sig
  type state = Cvalue.Model.t
  type t = Cvalue.V.t
  val emitter : Emitter.t Stdlib.ref
  val proxy : State_builder.Proxy.t
  val self : State.t
  val mark_as_computed : unit -> unit
  val compute : (unit -> unit) Stdlib.ref
  val is_computed : unit -> bool
  module Table_By_Callstack :
    sig
      val self : State.t
      val name : string
      val mark_as_computed : ?project:Project.t -> unit -> unit
      val is_computed : ?project:Project.t -> unit -> bool
      module Datatype : Datatype.S
      val add_hook_on_update : (Datatype.t -> unit) -> unit
      val howto_marshal : (Datatype.t -> 'a) -> ('-> Datatype.t) -> unit
      type key = Cil_types.stmt
      type data = state Value_types.Callstack.Hashtbl.t
      val replace : key -> data -> unit
      val add : key -> data -> unit
      val clear : unit -> unit
      val length : unit -> int
      val iter : (key -> data -> unit) -> unit
      val iter_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
      val fold : (key -> data -> '-> 'a) -> '-> 'a
      val fold_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> '-> 'a) -> '-> 'a
      val memo : ?change:(data -> data) -> (key -> data) -> key -> data
      val find : key -> data
      val find_all : key -> data list
      val mem : key -> bool
      val remove : key -> unit
    end
  module AfterTable_By_Callstack :
    sig
      val self : State.t
      val name : string
      val mark_as_computed : ?project:Project.t -> unit -> unit
      val is_computed : ?project:Project.t -> unit -> bool
      module Datatype : Datatype.S
      val add_hook_on_update : (Datatype.t -> unit) -> unit
      val howto_marshal : (Datatype.t -> 'a) -> ('-> Datatype.t) -> unit
      type key = Cil_types.stmt
      type data = state Value_types.Callstack.Hashtbl.t
      val replace : key -> data -> unit
      val add : key -> data -> unit
      val clear : unit -> unit
      val length : unit -> int
      val iter : (key -> data -> unit) -> unit
      val iter_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
      val fold : (key -> data -> '-> 'a) -> '-> 'a
      val fold_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> '-> 'a) -> '-> 'a
      val memo : ?change:(data -> data) -> (key -> data) -> key -> data
      val find : key -> data
      val find_all : key -> data list
      val mem : key -> bool
      val remove : key -> unit
    end
  val ignored_recursive_call : Cil_types.kernel_function -> bool
  val condition_truth_value : Cil_types.stmt -> bool * bool
  val use_spec_instead_of_definition :
    (Cil_types.kernel_function -> bool) Stdlib.ref
  val fun_set_args : Db.Value.t list -> unit
  val fun_use_default_args : unit -> unit
  val fun_get_args : unit -> Db.Value.t list option
  exception Incorrect_number_of_arguments
  val globals_set_initial_state : Db.Value.state -> unit
  val globals_use_default_initial_state : unit -> unit
  val globals_state : unit -> Db.Value.state
  val globals_use_supplied_state : unit -> bool
  val get_initial_state : Cil_types.kernel_function -> Db.Value.state
  val get_initial_state_callstack :
    Cil_types.kernel_function ->
    Db.Value.state Value_types.Callstack.Hashtbl.t option
  val get_state : ?after:bool -> Cil_types.kinstr -> Db.Value.state
  val get_stmt_state_callstack :
    after:bool ->
    Cil_types.stmt -> Db.Value.state Value_types.Callstack.Hashtbl.t option
  val get_stmt_state : ?after:bool -> Cil_types.stmt -> Db.Value.state
  val fold_stmt_state_callstack :
    (Db.Value.state -> '-> 'a) -> '-> after:bool -> Cil_types.stmt -> 'a
  val fold_state_callstack :
    (Db.Value.state -> '-> 'a) ->
    '-> after:bool -> Cil_types.kinstr -> 'a
  val find : Db.Value.state -> Locations.location -> Db.Value.t
  val eval_lval :
    (?with_alarms:CilE.warn_mode ->
     Locations.Zone.t option ->
     Db.Value.state -> Cil_types.lval -> Locations.Zone.t option * Db.Value.t)
    Stdlib.ref
  val eval_expr :
    (?with_alarms:CilE.warn_mode ->
     Db.Value.state -> Cil_types.exp -> Db.Value.t)
    Stdlib.ref
  val eval_expr_with_state :
    (?with_alarms:CilE.warn_mode ->
     Db.Value.state -> Cil_types.exp -> Db.Value.state * Db.Value.t)
    Stdlib.ref
  val reduce_by_cond :
    (Db.Value.state -> Cil_types.exp -> bool -> Db.Value.state) Stdlib.ref
  val find_lv_plus :
    (Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list)
    Stdlib.ref
  val expr_to_kernel_function :
    (Cil_types.kinstr ->
     ?with_alarms:CilE.warn_mode ->
     deps:Locations.Zone.t option ->
     Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
    Stdlib.ref
  val expr_to_kernel_function_state :
    (Db.Value.state ->
     deps:Locations.Zone.t option ->
     Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
    Stdlib.ref
  exception Not_a_call
  val call_to_kernel_function : Cil_types.stmt -> Kernel_function.Hptset.t
  val valid_behaviors :
    (Cil_types.kernel_function ->
     Db.Value.state -> Cil_types.funbehavior list)
    Stdlib.ref
  val add_formals_to_state :
    (Db.Value.state ->
     Cil_types.kernel_function -> Cil_types.exp list -> Db.Value.state)
    Stdlib.ref
  val is_accessible : Cil_types.kinstr -> bool
  val is_reachable : Db.Value.state -> bool
  val is_reachable_stmt : Cil_types.stmt -> bool
  exception Void_Function
  val find_return_loc : Cil_types.kernel_function -> Locations.location
  val is_called : (Cil_types.kernel_function -> bool) Stdlib.ref
  val callers :
    (Cil_types.kernel_function ->
     (Cil_types.kernel_function * Cil_types.stmt list) list)
    Stdlib.ref
  val access : (Cil_types.kinstr -> Cil_types.lval -> Db.Value.t) Stdlib.ref
  val access_expr :
    (Cil_types.kinstr -> Cil_types.exp -> Db.Value.t) Stdlib.ref
  val access_location :
    (Cil_types.kinstr -> Locations.location -> Db.Value.t) Stdlib.ref
  val lval_to_loc :
    (Cil_types.kinstr ->
     ?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location)
    Stdlib.ref
  val lval_to_loc_with_deps :
    (Cil_types.kinstr ->
     ?with_alarms:CilE.warn_mode ->
     deps:Locations.Zone.t ->
     Cil_types.lval -> Locations.Zone.t * Locations.location)
    Stdlib.ref
  val lval_to_loc_with_deps_state :
    (Db.Value.state ->
     deps:Locations.Zone.t ->
     Cil_types.lval -> Locations.Zone.t * Locations.location)
    Stdlib.ref
  val lval_to_loc_state :
    (Db.Value.state -> Cil_types.lval -> Locations.location) Stdlib.ref
  val lval_to_offsetmap :
    (Cil_types.kinstr ->
     ?with_alarms:CilE.warn_mode ->
     Cil_types.lval -> Cvalue.V_Offsetmap.t option)
    Stdlib.ref
  val lval_to_offsetmap_state :
    (Db.Value.state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)
    Stdlib.ref
  val lval_to_zone :
    (Cil_types.kinstr ->
     ?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t)
    Stdlib.ref
  val lval_to_zone_state :
    (Db.Value.state -> Cil_types.lval -> Locations.Zone.t) Stdlib.ref
  val lval_to_zone_with_deps_state :
    (Db.Value.state ->
     for_writing:bool ->
     deps:Locations.Zone.t option ->
     Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool)
    Stdlib.ref
  val lval_to_precise_loc_state :
    (?with_alarms:CilE.warn_mode ->
     Db.Value.state ->
     Cil_types.lval ->
     Db.Value.state * Precise_locs.precise_location * Cil_types.typ)
    Stdlib.ref
  val lval_to_precise_loc_with_deps_state :
    (Db.Value.state ->
     deps:Locations.Zone.t option ->
     Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location)
    Stdlib.ref
  val assigns_inputs_to_zone :
    (Db.Value.state -> Cil_types.assigns -> Locations.Zone.t) Stdlib.ref
  val assigns_outputs_to_zone :
    (Db.Value.state ->
     result:Cil_types.varinfo option -> Cil_types.assigns -> Locations.Zone.t)
    Stdlib.ref
  val assigns_outputs_to_locations :
    (Db.Value.state ->
     result:Cil_types.varinfo option ->
     Cil_types.assigns -> Locations.location list)
    Stdlib.ref
  val verify_assigns_froms :
    (Kernel_function.t -> pre:Db.Value.state -> Function_Froms.t -> unit)
    Stdlib.ref
  module Logic :
    sig
      val eval_predicate :
        (pre:Db.Value.state ->
         here:Db.Value.state ->
         Cil_types.predicate -> Property_status.emitted_status)
        Stdlib.ref
    end
  type callstack = Value_types.callstack
  module Record_Value_Callbacks :
    sig
      type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  module Record_Value_Superposition_Callbacks :
    sig
      type param = callstack * state list Cil_datatype.Stmt.Hashtbl.t Lazy.t
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  module Record_Value_After_Callbacks :
    sig
      type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  module Record_Value_Callbacks_New :
    sig
      type param =
          callstack *
          (state Cil_datatype.Stmt.Hashtbl.t Lazy.t *
           state Cil_datatype.Stmt.Hashtbl.t Lazy.t)
          Value_types.callback_result
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  val no_results : (Cil_types.fundec -> bool) Stdlib.ref
  module Call_Value_Callbacks :
    sig
      type param = state * callstack
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  module Call_Type_Value_Callbacks :
    sig
      type param =
          [ `Builtin of Value_types.call_froms
          | `Def
          | `Memexec
          | `Spec of Cil_types.funspec ] * state * callstack
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  module Compute_Statement_Callbacks :
    sig
      type param = Cil_types.stmt * callstack * state list
      type result = unit
      val extend : (param -> result) -> unit
      val extend_once : (param -> result) -> unit
      val apply : param -> result
      val is_empty : unit -> bool
      val clear : unit -> unit
      val length : unit -> int
    end
  val rm_asserts : (unit -> unit) Stdlib.ref
  val pretty : Stdlib.Format.formatter -> Db.Value.t -> unit
  val pretty_state : Stdlib.Format.formatter -> Db.Value.state -> unit
  val display :
    (Stdlib.Format.formatter -> Cil_types.kernel_function -> unit) Stdlib.ref
  val noassert_get_state : ?after:bool -> Cil_types.kinstr -> Db.Value.state
  val recursive_call_occurred : Cil_types.kernel_function -> unit
  val merge_conditions : int Cil_datatype.Stmt.Hashtbl.t -> unit
  val mask_then : int
  val mask_else : int
  val initial_state_only_globals : (unit -> Db.Value.state) Stdlib.ref
  val update_callstack_table :
    after:bool ->
    Cil_types.stmt -> Db.Value.callstack -> Db.Value.state -> unit
  val memoize : (Cil_types.kernel_function -> unit) Stdlib.ref
  val merge_initial_state : Db.Value.callstack -> Db.Value.state -> unit
  val initial_state_changed : (unit -> unit) Stdlib.ref
end