Parameter Make.State

type t

A mapping for variables (Binsec_kernel.Dba.Var.t -> value) and memory accesses (value -> value).

val lookup : Binsec_kernel.Dba.Var.t -> t -> Value.t

lookup var s returns the value assigned to var in s.

  • raises Undefined

    if var is not in s.

val read : addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

read ~addr len d s returns len bytes of the value stored at address addr in the main memory array @, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    None if there is no main memory in s (see S.declare).

val select : string -> addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

select m ~addr len d s returns len bytes of the value stored at address addr in the memory array m, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    Some m if m is not in s (see S.declare).