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
    Mahmudul Faisal Al Ameen
  10. M
    Manh-Dung Nguyen
  11. M
    Mathéo Vergnolle
  12. M
    Mathilde Ollivier
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

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

Sources

binsec-0.9.0.tbz
sha256=d959c2351b6cac10ffbdaf112769a676c9ad84bf6bc7fefa5cb1daa8d086cc97
sha512=1a3951896f05fb3a4cb05e81830373c75409a69c49323dc82e97c94889927b5f9561e704565a22c2a608842f67063d6c89a330477165b197a40d6ac231c09a7e

doc/checkct/Checkct/Make/argument-4-State/index.html

Parameter Make.State

include Libsse.Types.RAW_STATE with type Value.t = Libterm.Sexpr.Expr.t
type t

Symbolic state

module Value : Libsse.Types.VALUE with type id := Uid.t and type state := t with type t = Libterm.Sexpr.Expr.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 Libsse.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 Libsse.Types.target -> Format.formatter -> t -> unit
val to_formula : t -> Binsec.Formula.formula
val downcast : 'a Libsse.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.