Parameter Make.State

type t = {
  1. ctx : Domain.Context.t;
  2. vars : Domain.binary Binsec_codex_lib.Dba2Codex.VarMap.t;
  3. memory : Domain.memory;
  4. instruction_count : int;
  5. is_bottom : bool;
  6. never_went_to_user_code : bool;
}
val initial : (Binsec.Loader_elf.Img.t, 'a, 'b, 'c) Binsec.Loader.t_pack -> Domain.Context.t -> t
val initial_concrete : (Binsec.Loader_elf.Img.t, 'a, 'b, 'c) Binsec.Loader.t_pack -> Domain.Context.t -> t
val reset : (Binsec.Loader_elf.Img.t, 'a, 'b, 'c) Binsec.Loader.t_pack -> Domain.Context.t -> t
val get : size:Units.In_bits.t -> t -> string -> Domain.binary
val set : t -> string -> Domain.binary -> t
val assume : Domain.boolean -> t -> t
val bottom : Domain.Context.t -> t
val dump_state : Stdlib.Format.formatter -> t -> unit
val dump_state_diff : Stdlib.Format.formatter -> t -> t -> Binsec.Virtual_address.t -> (string, string) Stdlib.Hashtbl.t -> unit
val join : t -> t -> t
val is_included : t -> t -> bool
val serialize : widens:bool -> t -> t -> 'a Domain.Context.in_acc -> (t, 'a) Domain.Context.result

Serialize a state's variables and memory into a tuple. to_tuple ctx state returns the result of serialization, along with an inversion function, to turn a tuple back into a state. This function takes the original state and a tuple as arguments, and update the state's vars and memory fields with the tuple's contents.