package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (18)

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Manh-Dung Nguyen
  10. M
    Mathéo Vergnolle
  11. M
    Mathilde Ollivier
  12. M
    Matthieu Lemerre
  13. O
    Olivier Nicole
  14. R
    Richard Bonichon
  15. R
    Robin David
  16. S
    Sébastien Bardin
  17. S
    Soline Ducousso
  18. T
    Ta Thanh Dinh
  19. Y
    Yaëlle Vinçont

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.8.1.tbz
sha256=94090e05906c7a0559f60d2c65dbe167eb5953a2338b958b71911c1c81dd9ffd
sha512=6f52f8918c3c242f1346ebdc244f80744966112b935e00519e5d4d5acc040f8e2d2c54ff6b172cf5eb34b9bf7366de085605de88fcc15c43f34abce39ed34220

doc/binsec.sse/Libsse/Eval/Make/argument-2-State/index.html

Parameter Make.State

include Types.RAW_STATE
type t

Symbolic state

module Uid : Types.UID
module Value : Types.VALUE with type id := Uid.t and type state := t
val lookup : Libsse.Types.Var.t -> t -> Value.t
val read : addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t
val select : string -> addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t
val empty : unit -> t
val assume : Value.t -> t -> t option
val test : Value.t -> t -> t Types.test
val get_value : Value.t -> t -> Binsec.Bitvector.t
val get_a_value : Value.t -> t -> Binsec.Bitvector.t
val enumerate : Value.t -> ?n:int -> ?except:Binsec.Bitvector.t list -> t -> (Binsec.Bitvector.t * t) list
val alloc : array:string -> t -> t
val assign : Libsse.Types.Var.t -> Value.t -> t -> t
val write : addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t
val store : string -> addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t
val memcpy : addr:Binsec.Bitvector.t -> int -> Binsec.Loader_buf.t -> t -> t
val merge : parent:t -> t -> t -> t
val assertions : t -> Value.t list
val pp : Format.formatter -> t -> unit
val pp_smt : Value.t Types.target -> Format.formatter -> t -> unit
val to_formula : t -> Binsec.Formula.formula
val downcast : 'a Types.feature -> (t -> 'a) option

downcast feature returns a cast function from a state to an extended state. It returns None if the current implementation does not support the queried feature.

val id : Uid.t Types.key