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 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.