Module Dba2CState.State

module Domain : sig ... end
type t = Dba2CodexC.Make(Arch.Registers).State.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