package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

Dune Dependency

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

Authors

Maintainers

B

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

Sources

binsec-0.10.1.tbz

sha256=87d4048c9a90c8a14ee029e77d31032a15427f06416a31938cec8a68394234c4

sha512=6a023d2a5c87c56b0aac489874431d8dcccee1451a072a826190be3a7f75a961688bab95f193f494231744abc3bc9733ab5c809057d36a5e4d24c6c29c369144

doc/shadow_stack/Shadow_stack/Inline/argument-2-S/index.html

Parameter `Inline.S`

include Libsse.Types.RAW_STATE

type t

Symbolic state

module Uid : Libsse.Types.UID

module Value : Libsse.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 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 getter : 'a Libsse.Types.feature -> (t -> 'a) option

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

val setter : 'a Libsse.Types.feature -> ('a -> t -> t) option

setter feature returns a setter function to update an extended feature. It returns None if the current implementation does not support the queried feature.

val id : Uid.t Libsse.Types.key

val symbols : Value.t list Libsse.Types.S.Map.t Libsse.Types.key