sig   type state = Cvalue.Model.t   type t = Cvalue.V.t   exception Aborted   val emitter : Emitter.t Pervasives.ref   val self : State.t   val mark_as_computed : unit -> unit   val compute : (unit -> unit) Pervasives.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   exception Outside_builtin_possibilities   type builtin_sig =       Db.Value.state ->       (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->       Value_types.call_result   val register_builtin :     (string -> ?replace:string -> Db.Value.builtin_sig -> unit)     Pervasives.ref   val registered_builtins :     (unit -> (string * Db.Value.builtin_sig) list) Pervasives.ref   val mem_builtin : (string -> bool) Pervasives.ref   val use_spec_instead_of_definition :     (Cil_types.kernel_function -> bool) Pervasives.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 : 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 : 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)     Pervasives.ref   val eval_expr :     (with_alarms:CilE.warn_mode ->      Db.Value.state -> Cil_types.exp -> Db.Value.t)     Pervasives.ref   val eval_expr_with_state :     (with_alarms:CilE.warn_mode ->      Db.Value.state -> Cil_types.exp -> Db.Value.state * Db.Value.t)     Pervasives.ref   val find_lv_plus :     (Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list)     Pervasives.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)     Pervasives.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)     Pervasives.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)     Pervasives.ref   val add_formals_to_state :     (Db.Value.state ->      Cil_types.kernel_function -> Cil_types.exp list -> Db.Value.state)     Pervasives.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) Pervasives.ref   val callers :     (Cil_types.kernel_function ->      (Cil_types.kernel_function * Cil_types.stmt list) list)     Pervasives.ref   val access :     (Cil_types.kinstr -> Cil_types.lval -> Db.Value.t) Pervasives.ref   val access_expr :     (Cil_types.kinstr -> Cil_types.exp -> Db.Value.t) Pervasives.ref   val access_location :     (Cil_types.kinstr -> Locations.location -> Db.Value.t) Pervasives.ref   val lval_to_loc :     (Cil_types.kinstr ->      with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location)     Pervasives.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)     Pervasives.ref   val lval_to_loc_with_deps_state :     (Db.Value.state ->      deps:Locations.Zone.t ->      Cil_types.lval -> Locations.Zone.t * Locations.location)     Pervasives.ref   val lval_to_loc_state :     (Db.Value.state -> Cil_types.lval -> Locations.location) Pervasives.ref   val lval_to_offsetmap :     (Cil_types.kinstr ->      Cil_types.lval ->      with_alarms:CilE.warn_mode -> Cvalue.V_Offsetmap.t option)     Pervasives.ref   val lval_to_offsetmap_state :     (Db.Value.state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)     Pervasives.ref   val lval_to_zone :     (Cil_types.kinstr ->      with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t)     Pervasives.ref   val lval_to_zone_state :     (Db.Value.state -> Cil_types.lval -> Locations.Zone.t) Pervasives.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)     Pervasives.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)     Pervasives.ref   val assigns_inputs_to_zone :     (Db.Value.state ->      Cil_types.identified_term Cil_types.assigns -> Locations.Zone.t)     Pervasives.ref   val assigns_outputs_to_zone :     (Db.Value.state ->      result:Cil_types.varinfo option ->      Cil_types.identified_term Cil_types.assigns -> Locations.Zone.t)     Pervasives.ref   val assigns_outputs_to_locations :     (Db.Value.state ->      result:Cil_types.varinfo option ->      Cil_types.identified_term Cil_types.assigns -> Locations.location list)     Pervasives.ref   val verify_assigns_froms :     (Kernel_function.t -> pre:Db.Value.state -> Function_Froms.t -> unit)     Pervasives.ref   module Logic :     sig       val eval_predicate :         (pre:Db.Value.state ->          here:Db.Value.state ->          Cil_types.predicate -> Property_status.emitted_status)         Pervasives.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) Pervasives.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_result | `Def | `Memexec | `Spec ] *           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 pretty : Format.formatter -> Db.Value.t -> unit   val pretty_state : Format.formatter -> Db.Value.state -> unit   val display :     (Format.formatter -> Cil_types.kernel_function -> unit) Pervasives.ref   val noassert_get_state : 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) Pervasives.ref   val update_callstack_table :     after:bool ->     Cil_types.stmt -> Db.Value.callstack -> Db.Value.state -> unit   val memoize : (Cil_types.kernel_function -> unit) Pervasives.ref   val merge_initial_state : Db.Value.callstack -> Db.Value.state -> unit   val initial_state_changed : (unit -> unit) Pervasives.ref end