package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module D : Domains.S

Signature

type t

Symbolic state

module Value : Libsse.Types.VALUE with type id := Uid.t and type state := t with type t = 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.