Module Senv.StateSource

Parameters

module D : Domains.S

Signature

Sourcetype t

Symbolic state

Sourcemodule Value : Libsse.Types.VALUE with type id := Uid.t and type state := t with type t = Sexpr.Expr.t
Sourceval read : addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t
Sourceval select : string -> addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t
Sourceval empty : unit -> t
Sourceval assume : Value.t -> t -> t option
Sourceval get_value : Value.t -> t -> Binsec.Bitvector.t
Sourceval get_a_value : Value.t -> t -> Binsec.Bitvector.t
Sourceval enumerate : Value.t -> ?n:int -> ?except:Binsec.Bitvector.t list -> t -> (Binsec.Bitvector.t * t) list
Sourceval alloc : array:string -> t -> t
Sourceval assign : Libsse.Types.Var.t -> Value.t -> t -> t
Sourceval write : addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t
Sourceval store : string -> addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t
Sourceval memcpy : addr:Binsec.Bitvector.t -> int -> Binsec.Loader_buf.t -> t -> t
Sourceval merge : parent:t -> t -> t -> t
Sourceval assertions : t -> Value.t list
Sourceval pp : Format.formatter -> t -> unit
Sourceval to_formula : t -> Binsec.Formula.formula
Sourceval 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.

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