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.6.3.tbz
sha256=108b575f2b5405814cab41e34d15602045cc708c4b11ebb662a49ca759b3a37c
sha512=3c17273fc1deb160bc1bccf827e9afaec50715ee46d0b8e232be7599a0cd7c91f8422d59ea4d18f72c6133d9d026e21786b0d7c7ce8f394784f2cc350d9ada07

doc/binsec.sse/Se/Sse_symbolic/State/index.html

Module Sse_symbolic.State

Parameters

Signature

type t

Symbolic state

val empty : unit -> t
val assume : Binsec.Dba.Expr.t -> t -> t option
val split_on : Binsec.Dba.Expr.t -> ?n:int -> ?except:Binsec.Bitvector.t list -> t -> (Binsec.Bitvector.t * t) list
val fresh : string -> int -> t -> t
val assign : string -> Binsec.Dba.Expr.t -> t -> t
val memcpy : addr:Binsec.Bitvector.t -> int -> Binsec.Loader_buf.t -> t -> t
val pp : Format.formatter -> t -> unit
val pp_smt : ?slice:(Binsec.Dba.Expr.t * string) list -> Format.formatter -> t -> unit
val as_ascii : string -> t -> string
val to_formula : t -> Binsec.Formula.formula