Module State.Domain

val unique_id : unit -> int

val name : unit -> string

module Context : sig ... end

val root_context : unit -> Context.t

val context_pretty : Stdlib.Format.formatter -> Context.t -> unit

type boolean = Dba2CodexC.Domain.boolean

val assume : Context.t -> boolean -> Context.t option

val typed_nondet2 : Context.t -> Context.t -> 'a Context.in_tuple -> Context.t * 'a Context.out_tuple

val nondet_same_context : Context.t -> 'a Context.in_tuple -> 'a Context.out_tuple

val mu_context_open : Context.t -> Context.t

val typed_fixpoint_step : iteration:int -> init:Context.t -> arg:Context.t -> body:Context.t -> (bool * 'a Context.in_tuple) -> bool * (close:bool -> 'a Context.out_tuple * Context.t)

val widened_fixpoint_step : widening_id:int -> previous:Context.t -> next:Context.t -> (bool * 'a Context.in_tuple) -> Context.t * bool * 'a Context.out_tuple

module Boolean : sig ... end

val boolean_pretty : Context.t -> Stdlib.Format.formatter -> boolean -> unit

val serialize_boolean : Context.t -> boolean -> Context.t -> boolean -> 'a Context.in_acc -> (boolean, 'a) Context.result

val boolean_empty : Context.t -> boolean

val boolean_unknown : Context.t -> boolean

module Boolean_Forward : sig ... end

val query_boolean : Context.t -> boolean -> Lattices.Quadrivalent.t

type binary = Dba2CodexC.Domain.binary

type enum = Dba2CodexC.Domain.enum

val binary_unknown_typed : size:Units.In_bits.t -> Context.t -> Types.TypedC.typ -> binary

module Binary : sig ... end

val binary_pretty : size:Units.In_bits.t -> Context.t -> Stdlib.Format.formatter -> binary -> unit

val serialize_binary : widens:bool -> size:Units.In_bits.t -> Context.t -> binary -> Context.t -> binary -> 'a Context.in_acc -> (binary, 'a) Context.result

val binary_empty : size:Units.In_bits.t -> Context.t -> binary

val binary_unknown : size:Units.In_bits.t -> Context.t -> binary

module Binary_Forward : sig ... end

module Enum : sig ... end

val enum_pretty : Context.t -> Stdlib.Format.formatter -> enum -> unit

val serialize_enum : Context.t -> enum -> Context.t -> enum -> 'a Context.in_acc -> (enum, 'a) Context.result

val enum_empty : Context.t -> enum

val enum_unknown : enumsize:int -> Context.t -> enum

module Enum_Forward : sig ... end

val union : Operator.Condition.t -> Context.t -> 'a Context.in_tuple -> 'a Context.out_tuple

val satisfiable : Context.t -> boolean -> Smtbackend.Smtlib_sig.sat

type block = Dba2CodexC.Domain.block

type offset = Dba2CodexC.Domain.offset

type memory = Dba2CodexC.Domain.memory

module Query : sig ... end

val should_focus : size:Units.In_bits.t -> Context.t -> memory -> binary -> (binary * offset) option

val may_alias : ptr_size:Units.In_bits.t -> Context.t -> size1:offset -> size2:offset -> binary -> binary -> bool

val is_weak : size:Units.In_bits.t -> Context.t -> binary -> bool

val offset_zero : max:int option -> Context.t -> offset

val offset_shift : offset:int -> max:int option -> Context.t -> offset -> offset

val offset_le : Context.t -> offset -> offset -> boolean

val offset_eq : Context.t -> offset -> offset -> boolean

val block_empty : Context.t -> block

val block_unknown : Context.t -> block

val block_pretty : Context.t -> Stdlib.Format.formatter -> block -> unit

val serialize_block : widens:bool -> Context.t -> block -> Context.t -> block -> 'a Context.in_acc -> (block, 'a) Context.result

val addresses_in_block : Context.t -> block -> Context.t -> block -> (binary * binary) list

module Block_Forward : sig ... end

val offset_pretty : Context.t -> Stdlib.Format.formatter -> offset -> unit

val serialize_memory : widens:bool -> Context.t -> memory -> Context.t -> memory -> 'a Context.in_acc -> (memory, 'a) Context.result

val memory_pretty : Context.t -> Stdlib.Format.formatter -> memory -> unit

val addresses_in_memory : Context.t -> memory -> Context.t -> memory -> (binary * binary) list

module Memory_Forward : sig ... end

val reachable : Context.t -> memory -> Smtbackend.Smtlib_sig.sat

val global_symbol : Context.t -> string -> Units.In_bits.t * binary

val add_global_symbol : size:Units.In_bits.t -> Context.t -> string -> binary -> unit

val check_type : size:Units.In_bits.t -> Context.t -> Types.TypedC.typ -> binary -> binary Types.Type_check_tree.t

val type_of : size:Units.In_bits.t -> Context.t -> binary -> Types.TypedC.typ option

val flush_cache : Context.t -> memory -> memory

val analyze_summary : Context.t -> Types.TypedC.typ -> (Units.In_bits.t * binary) list -> memory -> bool * (Units.In_bits.t * binary) option * memory

val serialize_memory_and_cache : widens:bool -> Context.t -> memory -> Context.t -> memory -> (binary * binary) list -> 'a Context.in_acc -> (memory, 'a) Context.result