sig   type 'a how_to_journalize =       Journalize of string * 'Type.t     | Journalization_not_required     | Journalization_must_not_happen of string   val register : 'Db.how_to_journalize -> 'Pervasives.ref -> '-> unit   val register_compute :     string ->     State.t list ->     (unit -> unit) Pervasives.ref -> (unit -> unit) -> State.t   val register_guarded_compute :     string ->     (unit -> bool) -> (unit -> unit) Pervasives.ref -> (unit -> unit) -> unit   module Main :     sig       val extend : (unit -> unit) -> unit       val play : (unit -> unit) Pervasives.ref       val apply : unit -> unit     end   module Toplevel : sig val run : ((unit -> unit) -> unit) Pervasives.ref end   module Value :     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   module From :     sig       exception Not_lval       val compute_all : (unit -> unit) Pervasives.ref       val compute_all_calldeps : (unit -> unit) Pervasives.ref       val compute : (Cil_types.kernel_function -> unit) Pervasives.ref       val is_computed : (Cil_types.kernel_function -> bool) Pervasives.ref       val get :         (Cil_types.kernel_function -> Function_Froms.t) Pervasives.ref       val access :         (Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t)         Pervasives.ref       val find_deps_no_transitivity :         (Cil_types.stmt -> Cil_types.exp -> Locations.Zone.t) Pervasives.ref       val find_deps_no_transitivity_state :         (Db.Value.state -> Cil_types.exp -> Locations.Zone.t) Pervasives.ref       val find_deps_term_no_transitivity_state :         (Db.Value.state -> Cil_types.term -> Value_types.logic_dependencies)         Pervasives.ref       val self : State.t Pervasives.ref       val pretty :         (Format.formatter -> Cil_types.kernel_function -> unit)         Pervasives.ref       val display : (Format.formatter -> unit) Pervasives.ref       module Record_From_Callbacks :         sig           type param =               Kernel_function.t Stack.t *               Function_Froms.Memory.t Cil_datatype.Stmt.Hashtbl.t *               (Kernel_function.t * Function_Froms.Memory.t) list               Cil_datatype.Stmt.Hashtbl.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 Callwise :         sig           val iter :             ((Cil_types.kinstr -> Function_Froms.t -> unit) -> unit)             Pervasives.ref           val find : (Cil_types.kinstr -> Function_Froms.t) Pervasives.ref         end     end   module Users :     sig       val get :         (Cil_types.kernel_function -> Kernel_function.Hptset.t)         Pervasives.ref     end   module Properties :     sig       module Interp :         sig           val term_lval :             (Cil_types.kernel_function ->              ?loc:Cil_types.location ->              ?env:Logic_typing.Lenv.t -> string -> Cil_types.term_lval)             Pervasives.ref           val term :             (Cil_types.kernel_function ->              ?loc:Cil_types.location ->              ?env:Logic_typing.Lenv.t -> string -> Cil_types.term)             Pervasives.ref           val predicate :             (Cil_types.kernel_function ->              ?loc:Cil_types.location ->              ?env:Logic_typing.Lenv.t -> string -> Cil_types.predicate)             Pervasives.ref           val code_annot :             (Cil_types.kernel_function ->              Cil_types.stmt -> string -> Cil_types.code_annotation)             Pervasives.ref           exception No_conversion           val term_lval_to_lval :             (result:Cil_types.varinfo option ->              Cil_types.term_lval -> Cil_types.lval)             Pervasives.ref           val term_to_lval :             (result:Cil_types.varinfo option ->              Cil_types.term -> Cil_types.lval)             Pervasives.ref           val term_to_exp :             (result:Cil_types.varinfo option ->              Cil_types.term -> Cil_types.exp)             Pervasives.ref           val loc_to_exp :             (result:Cil_types.varinfo option ->              Cil_types.term -> Cil_types.exp list)             Pervasives.ref           val loc_to_lval :             (result:Cil_types.varinfo option ->              Cil_types.term -> Cil_types.lval list)             Pervasives.ref           val term_offset_to_offset :             (result:Cil_types.varinfo option ->              Cil_types.term_offset -> Cil_types.offset)             Pervasives.ref           val loc_to_offset :             (result:Cil_types.varinfo option ->              Cil_types.term -> Cil_types.offset list)             Pervasives.ref           val loc_to_loc :             (result:Cil_types.varinfo option ->              Db.Value.state -> Cil_types.term -> Locations.location)             Pervasives.ref           val loc_to_loc_under_over :             (result:Cil_types.varinfo option ->              Db.Value.state ->              Cil_types.term ->              Locations.location * Locations.location * Locations.Zone.t)             Pervasives.ref           module To_zone :             sig               type t_ctx = {                 state_opt : bool option;                 ki_opt : (Cil_types.stmt * bool) option;                 kf : Kernel_function.t;               }               val mk_ctx_func_contrat :                 (Cil_types.kernel_function ->                  state_opt:bool option -> Db.Properties.Interp.To_zone.t_ctx)                 Pervasives.ref               val mk_ctx_stmt_contrat :                 (Cil_types.kernel_function ->                  Cil_types.stmt ->                  state_opt:bool option -> Db.Properties.Interp.To_zone.t_ctx)                 Pervasives.ref               val mk_ctx_stmt_annot :                 (Cil_types.kernel_function ->                  Cil_types.stmt -> Db.Properties.Interp.To_zone.t_ctx)                 Pervasives.ref               type t = {                 before : bool;                 ki : Cil_types.stmt;                 zone : Locations.Zone.t;               }               type t_zone_info = Db.Properties.Interp.To_zone.t list option               type t_decl = {                 var : Cil_datatype.Varinfo.Set.t;                 lbl : Cil_datatype.Logic_label.Set.t;               }               type t_pragmas = {                 ctrl : Cil_datatype.Stmt.Set.t;                 stmt : Cil_datatype.Stmt.Set.t;               }               val from_term :                 (Cil_types.term ->                  Db.Properties.Interp.To_zone.t_ctx ->                  Db.Properties.Interp.To_zone.t_zone_info *                  Db.Properties.Interp.To_zone.t_decl)                 Pervasives.ref               val from_terms :                 (Cil_types.term list ->                  Db.Properties.Interp.To_zone.t_ctx ->                  Db.Properties.Interp.To_zone.t_zone_info *                  Db.Properties.Interp.To_zone.t_decl)                 Pervasives.ref               val from_pred :                 (Cil_types.predicate ->                  Db.Properties.Interp.To_zone.t_ctx ->                  Db.Properties.Interp.To_zone.t_zone_info *                  Db.Properties.Interp.To_zone.t_decl)                 Pervasives.ref               val from_preds :                 (Cil_types.predicate list ->                  Db.Properties.Interp.To_zone.t_ctx ->                  Db.Properties.Interp.To_zone.t_zone_info *                  Db.Properties.Interp.To_zone.t_decl)                 Pervasives.ref               val from_zone :                 (Cil_types.identified_term ->                  Db.Properties.Interp.To_zone.t_ctx ->                  Db.Properties.Interp.To_zone.t_zone_info *                  Db.Properties.Interp.To_zone.t_decl)                 Pervasives.ref               val from_stmt_annot :                 (Cil_types.code_annotation ->                  Cil_types.stmt * Cil_types.kernel_function ->                  (Db.Properties.Interp.To_zone.t_zone_info *                   Db.Properties.Interp.To_zone.t_decl) *                  Db.Properties.Interp.To_zone.t_pragmas)                 Pervasives.ref               val from_stmt_annots :                 ((Cil_types.code_annotation -> bool) option ->                  Cil_types.stmt * Cil_types.kernel_function ->                  (Db.Properties.Interp.To_zone.t_zone_info *                   Db.Properties.Interp.To_zone.t_decl) *                  Db.Properties.Interp.To_zone.t_pragmas)                 Pervasives.ref               val from_func_annots :                 (((Cil_types.stmt -> unit) ->                   Cil_types.kernel_function -> unit) ->                  (Cil_types.code_annotation -> bool) option ->                  Cil_types.kernel_function ->                  (Db.Properties.Interp.To_zone.t_zone_info *                   Db.Properties.Interp.To_zone.t_decl) *                  Db.Properties.Interp.To_zone.t_pragmas)                 Pervasives.ref               val code_annot_filter :                 (Cil_types.code_annotation ->                  threat:bool ->                  user_assert:bool ->                  slicing_pragma:bool ->                  loop_inv:bool -> loop_var:bool -> others:bool -> bool)                 Pervasives.ref             end           val to_result_from_pred :             (Cil_types.predicate -> bool) Pervasives.ref         end       val add_assert :         Emitter.t ->         Cil_types.kernel_function -> Cil_types.stmt -> string -> unit     end   module PostdominatorsTypes :     sig       exception Top       module type Sig =         sig           val compute : (Cil_types.kernel_function -> unit) Pervasives.ref           val stmt_postdominators :             (Cil_types.kernel_function ->              Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t)             Pervasives.ref           val is_postdominator :             (Cil_types.kernel_function ->              opening:Cil_types.stmt -> closing:Cil_types.stmt -> bool)             Pervasives.ref           val display : (unit -> unit) Pervasives.ref           val print_dot :             (string -> Cil_types.kernel_function -> unit) Pervasives.ref         end     end   module Postdominators : PostdominatorsTypes.Sig   module PostdominatorsValue : PostdominatorsTypes.Sig   module RteGen :     sig       val compute : (unit -> unit) Pervasives.ref       val annotate_kf : (Cil_types.kernel_function -> unit) Pervasives.ref       val self : State.t Pervasives.ref       val do_precond : (Cil_types.kernel_function -> unit) Pervasives.ref       val do_all_rte : (Cil_types.kernel_function -> unit) Pervasives.ref       val do_rte : (Cil_types.kernel_function -> unit) Pervasives.ref       type status_accessor =           string * (Cil_types.kernel_function -> bool -> unit) *           (Cil_types.kernel_function -> bool)       val get_all_status :         (unit -> Db.RteGen.status_accessor list) Pervasives.ref       val get_precond_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_divMod_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_memAccess_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_pointerCall_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_signedOv_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_signed_downCast_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_unsignedOv_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref       val get_unsignedDownCast_status :         (unit -> Db.RteGen.status_accessor) Pervasives.ref     end   module Report : sig val print : (unit -> unit) Pervasives.ref end   module Constant_Propagation :     sig       val get :         (Cil_datatype.Fundec.Set.t -> cast_intro:bool -> Project.t)         Pervasives.ref       val compute : (unit -> unit) Pervasives.ref     end   module Impact :     sig       val compute_pragmas : (unit -> Cil_types.stmt list) Pervasives.ref       val from_stmt : (Cil_types.stmt -> Cil_types.stmt list) Pervasives.ref       val from_nodes :         (Cil_types.kernel_function ->          PdgTypes.Node.t list -> PdgTypes.NodeSet.t)         Pervasives.ref     end   module Security :     sig       val run_whole_analysis : (unit -> unit) Pervasives.ref       val run_ai_analysis : (unit -> unit) Pervasives.ref       val run_slicing_analysis : (unit -> Project.t) Pervasives.ref       val self : State.t Pervasives.ref     end   module Pdg :     sig       exception Bottom       exception Top       type t = PdgTypes.Pdg.t       type t_nodes_and_undef =           (PdgTypes.Node.t * Locations.Zone.t option) list *           Locations.Zone.t option       val self : State.t Pervasives.ref       val get : (Cil_types.kernel_function -> Db.Pdg.t) Pervasives.ref       val node_key : (PdgTypes.Node.t -> PdgIndex.Key.t) Pervasives.ref       val from_same_fun : Db.Pdg.t -> Db.Pdg.t -> bool       val find_decl_var_node :         (Db.Pdg.t -> Cil_types.varinfo -> PdgTypes.Node.t) Pervasives.ref       val find_ret_output_node : (Db.Pdg.t -> PdgTypes.Node.t) Pervasives.ref       val find_output_nodes :         (Db.Pdg.t -> PdgIndex.Signature.out_key -> Db.Pdg.t_nodes_and_undef)         Pervasives.ref       val find_input_node :         (Db.Pdg.t -> int -> PdgTypes.Node.t) Pervasives.ref       val find_all_inputs_nodes :         (Db.Pdg.t -> PdgTypes.Node.t list) Pervasives.ref       val find_stmt_node :         (Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref       val find_simple_stmt_nodes :         (Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list) Pervasives.ref       val find_label_node :         (Db.Pdg.t -> Cil_types.stmt -> Cil_types.label -> PdgTypes.Node.t)         Pervasives.ref       val find_stmt_and_blocks_nodes :         (Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list) Pervasives.ref       val find_top_input_node : (Db.Pdg.t -> PdgTypes.Node.t) Pervasives.ref       val find_entry_point_node :         (Db.Pdg.t -> PdgTypes.Node.t) Pervasives.ref       val find_location_nodes_at_stmt :         (Db.Pdg.t ->          Cil_types.stmt ->          before:bool -> Locations.Zone.t -> Db.Pdg.t_nodes_and_undef)         Pervasives.ref       val find_location_nodes_at_end :         (Db.Pdg.t -> Locations.Zone.t -> Db.Pdg.t_nodes_and_undef)         Pervasives.ref       val find_location_nodes_at_begin :         (Db.Pdg.t -> Locations.Zone.t -> Db.Pdg.t_nodes_and_undef)         Pervasives.ref       val find_call_stmts :         (Cil_types.kernel_function ->          caller:Cil_types.kernel_function -> Cil_types.stmt list)         Pervasives.ref       val find_call_ctrl_node :         (Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref       val find_call_input_node :         (Db.Pdg.t -> Cil_types.stmt -> int -> PdgTypes.Node.t) Pervasives.ref       val find_call_output_node :         (Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t) Pervasives.ref       val find_code_annot_nodes :         (Db.Pdg.t ->          Cil_types.stmt ->          Cil_types.code_annotation ->          PdgTypes.Node.t list * PdgTypes.Node.t list *          Db.Pdg.t_nodes_and_undef option)         Pervasives.ref       val find_fun_precond_nodes :         (Db.Pdg.t ->          Cil_types.predicate ->          PdgTypes.Node.t list * Db.Pdg.t_nodes_and_undef option)         Pervasives.ref       val find_fun_postcond_nodes :         (Db.Pdg.t ->          Cil_types.predicate ->          PdgTypes.Node.t list * Db.Pdg.t_nodes_and_undef option)         Pervasives.ref       val find_fun_variant_nodes :         (Db.Pdg.t ->          Cil_types.term ->          PdgTypes.Node.t list * Db.Pdg.t_nodes_and_undef option)         Pervasives.ref       val find_call_out_nodes_to_select :         (Db.Pdg.t ->          PdgTypes.NodeSet.t ->          Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list)         Pervasives.ref       val find_in_nodes_to_select_for_this_call :         (Db.Pdg.t ->          PdgTypes.NodeSet.t ->          Cil_types.stmt -> Db.Pdg.t -> PdgTypes.Node.t list)         Pervasives.ref       val direct_dpds :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_ctrl_dpds :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_data_dpds :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_addr_dpds :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val all_dpds :         (Db.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val all_data_dpds :         (Db.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val all_ctrl_dpds :         (Db.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val all_addr_dpds :         (Db.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val direct_uses :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_ctrl_uses :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_data_uses :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val direct_addr_uses :         (Db.Pdg.t -> PdgTypes.Node.t -> PdgTypes.Node.t list) Pervasives.ref       val all_uses :         (Db.Pdg.t -> PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val custom_related_nodes :         ((PdgTypes.Node.t -> PdgTypes.Node.t list) ->          PdgTypes.Node.t list -> PdgTypes.Node.t list)         Pervasives.ref       val iter_nodes :         ((PdgTypes.Node.t -> unit) -> Db.Pdg.t -> unit) Pervasives.ref       val extract : (Db.Pdg.t -> string -> unit) Pervasives.ref       val pretty_node :         (bool -> Format.formatter -> PdgTypes.Node.t -> unit) Pervasives.ref       val pretty_key :         (Format.formatter -> PdgIndex.Key.t -> unit) Pervasives.ref       val pretty :         (?bw:bool -> Format.formatter -> Db.Pdg.t -> unit) Pervasives.ref     end   module Scope :     sig       val get_data_scope_at_stmt :         (Cil_types.kernel_function ->          Cil_types.stmt ->          Cil_types.lval ->          Cil_datatype.Stmt.Hptset.t *          (Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t))         Pervasives.ref       val get_prop_scope_at_stmt :         (Cil_types.kernel_function ->          Cil_types.stmt ->          Cil_types.code_annotation ->          Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list)         Pervasives.ref       val check_asserts :         (unit -> Cil_types.code_annotation list) Pervasives.ref       val rm_asserts : (unit -> unit) Pervasives.ref       val get_defs :         (Cil_types.kernel_function ->          Cil_types.stmt ->          Cil_types.lval ->          (Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option)         Pervasives.ref       val get_defs_with_type :         (Cil_types.kernel_function ->          Cil_types.stmt ->          Cil_types.lval ->          ((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option)          option)         Pervasives.ref       type t_zones = Locations.Zone.t Cil_datatype.Stmt.Hashtbl.t       val build_zones :         (Cil_types.kernel_function ->          Cil_types.stmt ->          Cil_types.lval -> Cil_datatype.Stmt.Hptset.t * Db.Scope.t_zones)         Pervasives.ref       val pretty_zones :         (Format.formatter -> Db.Scope.t_zones -> unit) Pervasives.ref       val get_zones :         (Db.Scope.t_zones -> Cil_types.stmt -> Locations.Zone.t)         Pervasives.ref     end   module Sparecode :     sig       val get :         (select_annot:bool -> select_slice_pragma:bool -> Project.t)         Pervasives.ref       val rm_unused_globals :         (?new_proj_name:string -> ?project:Project.t -> unit -> Project.t)         Pervasives.ref     end   module Occurrence :     sig       type t =           (Cil_types.kernel_function option * Cil_types.kinstr *            Cil_types.lval)           list       val get : (Cil_types.varinfo -> Db.Occurrence.t) Pervasives.ref       val get_last_result :         (unit -> (Db.Occurrence.t * Cil_types.varinfo) option) Pervasives.ref       val print_all : (unit -> unit) Pervasives.ref       val self : State.t Pervasives.ref     end   module Slicing :     sig       exception No_Project       exception Existing_Project       val self : State.t Pervasives.ref       val set_modes :         (?calls:int ->          ?callers:bool ->          ?sliceUndef:bool ->          ?keepAnnotations:bool -> ?print:bool -> unit -> unit)         Pervasives.ref       module Project :         sig           type t = SlicingTypes.sl_project           val dyn_t : Db.Slicing.Project.t Type.t           val mk_project : (string -> Db.Slicing.Project.t) Pervasives.ref           val from_unique_name :             (string -> Db.Slicing.Project.t) Pervasives.ref           val get_all : (unit -> Db.Slicing.Project.t list) Pervasives.ref           val set_project :             (Db.Slicing.Project.t option -> unit) Pervasives.ref           val get_project :             (unit -> Db.Slicing.Project.t option) Pervasives.ref           val get_name : (Db.Slicing.Project.t -> string) Pervasives.ref           val is_called :             (Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)             Pervasives.ref           val has_persistent_selection :             (Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)             Pervasives.ref           val change_slicing_level :             (Db.Slicing.Project.t -> Cil_types.kernel_function -> int -> unit)             Pervasives.ref           val default_slice_names :             (Cil_types.kernel_function -> bool -> int -> string)             Pervasives.ref           val extract :             (string ->              ?f_slice_names:(Cil_types.kernel_function ->                              bool -> int -> string) ->              Db.Slicing.Project.t -> Project.t)             Pervasives.ref           val print_extracted_project :             (?fmt:Format.formatter -> extracted_prj:Project.t -> unit)             Pervasives.ref           val print_dot :             (filename:string -> title:string -> Db.Slicing.Project.t -> unit)             Pervasives.ref           val pretty :             (Format.formatter -> Db.Slicing.Project.t -> unit) Pervasives.ref           val is_directly_called_internal :             (Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)             Pervasives.ref         end       module Mark :         sig           type t = SlicingTypes.sl_mark           val dyn_t : Db.Slicing.Mark.t Type.t           val make :             (data:bool -> addr:bool -> ctrl:bool -> Db.Slicing.Mark.t)             Pervasives.ref           val compare :             (Db.Slicing.Mark.t -> Db.Slicing.Mark.t -> int) Pervasives.ref           val is_bottom : (Db.Slicing.Mark.t -> bool) Pervasives.ref           val is_spare : (Db.Slicing.Mark.t -> bool) Pervasives.ref           val is_data : (Db.Slicing.Mark.t -> bool) Pervasives.ref           val is_ctrl : (Db.Slicing.Mark.t -> bool) Pervasives.ref           val is_addr : (Db.Slicing.Mark.t -> bool) Pervasives.ref           val get_from_src_func :             (Db.Slicing.Project.t ->              Cil_types.kernel_function -> Db.Slicing.Mark.t)             Pervasives.ref           val pretty :             (Format.formatter -> Db.Slicing.Mark.t -> unit) Pervasives.ref         end       module Select :         sig           type t = SlicingTypes.sl_select           val dyn_t : Db.Slicing.Select.t Type.t           type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t           val dyn_set : Db.Slicing.Select.set Type.t           val empty_selects : Db.Slicing.Select.set           val select_stmt :             (Db.Slicing.Select.set ->              spare:bool ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_ctrl :             (Db.Slicing.Select.set ->              spare:bool ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_lval_rw :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              rd:Datatype.String.Set.t ->              wr:Datatype.String.Set.t ->              Cil_types.stmt ->              eval:Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_lval :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Datatype.String.Set.t ->              before:bool ->              Cil_types.stmt ->              eval:Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_zone :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Locations.Zone.t ->              before:bool ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_term :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Cil_types.term ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_pred :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Cil_types.predicate ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_annot :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              spare:bool ->              Cil_types.code_annotation ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_stmt_annots :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              spare:bool ->              threat:bool ->              user_assert:bool ->              slicing_pragma:bool ->              loop_inv:bool ->              loop_var:bool ->              Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_lval_rw :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              rd:Datatype.String.Set.t ->              wr:Datatype.String.Set.t ->              eval:Cil_types.stmt ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_lval :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Datatype.String.Set.t ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_zone :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              Locations.Zone.t ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_return :             (Db.Slicing.Select.set ->              spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_calls_to :             (Db.Slicing.Select.set ->              spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_calls_into :             (Db.Slicing.Select.set ->              spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val select_func_annots :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              spare:bool ->              threat:bool ->              user_assert:bool ->              slicing_pragma:bool ->              loop_inv:bool ->              loop_var:bool ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref           val pretty :             (Format.formatter -> Db.Slicing.Select.t -> unit) Pervasives.ref           val get_function :             (Db.Slicing.Select.t -> Cil_types.kernel_function) Pervasives.ref           val merge_internal :             (Db.Slicing.Select.t ->              Db.Slicing.Select.t -> Db.Slicing.Select.t)             Pervasives.ref           val add_to_selects_internal :             (Db.Slicing.Select.t ->              Db.Slicing.Select.set -> Db.Slicing.Select.set)             Pervasives.ref           val iter_selects_internal :             ((Db.Slicing.Select.t -> unit) -> Db.Slicing.Select.set -> unit)             Pervasives.ref           val fold_selects_internal :             ('-> Db.Slicing.Select.t -> 'a) ->             '-> Db.Slicing.Select.set -> 'a           val select_stmt_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_types.stmt -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_label_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_datatype.Logic_label.t ->              Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_min_call_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_types.stmt -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_stmt_zone_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_types.stmt ->              before:bool ->              Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_zone_at_entry_point_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_zone_at_end_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_modified_output_zone_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_stmt_ctrl_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_types.stmt -> Db.Slicing.Select.t)             Pervasives.ref           val select_pdg_nodes_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              PdgTypes.Node.t list -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_entry_point_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_return_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_decl_var_internal :             (Cil_types.kernel_function ->              ?select:Db.Slicing.Select.t ->              Cil_types.varinfo -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)             Pervasives.ref           val select_pdg_nodes :             (Db.Slicing.Select.set ->              Db.Slicing.Mark.t ->              PdgTypes.Node.t list ->              Cil_types.kernel_function -> Db.Slicing.Select.set)             Pervasives.ref         end       module Slice :         sig           type t = SlicingTypes.sl_fct_slice           val dyn_t : Db.Slicing.Slice.t Type.t           val create :             (Db.Slicing.Project.t ->              Cil_types.kernel_function -> Db.Slicing.Slice.t)             Pervasives.ref           val remove :             (Db.Slicing.Project.t -> Db.Slicing.Slice.t -> unit)             Pervasives.ref           val remove_uncalled : (Db.Slicing.Project.t -> unit) Pervasives.ref           val get_all :             (Db.Slicing.Project.t ->              Cil_types.kernel_function -> Db.Slicing.Slice.t list)             Pervasives.ref           val get_function :             (Db.Slicing.Slice.t -> Cil_types.kernel_function) Pervasives.ref           val get_callers :             (Db.Slicing.Slice.t -> Db.Slicing.Slice.t list) Pervasives.ref           val get_called_slice :             (Db.Slicing.Slice.t ->              Cil_types.stmt -> Db.Slicing.Slice.t option)             Pervasives.ref           val get_called_funcs :             (Db.Slicing.Slice.t ->              Cil_types.stmt -> Cil_types.kernel_function list)             Pervasives.ref           val get_mark_from_stmt :             (Db.Slicing.Slice.t -> Cil_types.stmt -> Db.Slicing.Mark.t)             Pervasives.ref           val get_mark_from_label :             (Db.Slicing.Slice.t ->              Cil_types.stmt -> Cil_types.label -> Db.Slicing.Mark.t)             Pervasives.ref           val get_mark_from_local_var :             (Db.Slicing.Slice.t -> Cil_types.varinfo -> Db.Slicing.Mark.t)             Pervasives.ref           val get_mark_from_formal :             (Db.Slicing.Slice.t -> Cil_types.varinfo -> Db.Slicing.Mark.t)             Pervasives.ref           val get_user_mark_from_inputs :             (Db.Slicing.Slice.t -> Db.Slicing.Mark.t) Pervasives.ref           val get_num_id : (Db.Slicing.Slice.t -> int) Pervasives.ref           val from_num_id :             (Db.Slicing.Project.t ->              Cil_types.kernel_function -> int -> Db.Slicing.Slice.t)             Pervasives.ref           val pretty :             (Format.formatter -> Db.Slicing.Slice.t -> unit) Pervasives.ref         end       module Request :         sig           val apply_all :             (Db.Slicing.Project.t -> propagate_to_callers:bool -> unit)             Pervasives.ref           val add_selection :             (Db.Slicing.Project.t -> Db.Slicing.Select.set -> unit)             Pervasives.ref           val add_persistent_selection :             (Db.Slicing.Project.t -> Db.Slicing.Select.set -> unit)             Pervasives.ref           val add_persistent_cmdline :             (Db.Slicing.Project.t -> unit) Pervasives.ref           val is_already_selected_internal :             (Db.Slicing.Slice.t -> Db.Slicing.Select.t -> bool)             Pervasives.ref           val add_slice_selection_internal :             (Db.Slicing.Project.t ->              Db.Slicing.Slice.t -> Db.Slicing.Select.t -> unit)             Pervasives.ref           val add_selection_internal :             (Db.Slicing.Project.t -> Db.Slicing.Select.t -> unit)             Pervasives.ref           val add_call_slice :             (Db.Slicing.Project.t ->              caller:Db.Slicing.Slice.t -> to_call:Db.Slicing.Slice.t -> unit)             Pervasives.ref           val add_call_fun :             (Db.Slicing.Project.t ->              caller:Db.Slicing.Slice.t ->              to_call:Cil_types.kernel_function -> unit)             Pervasives.ref           val add_call_min_fun :             (Db.Slicing.Project.t ->              caller:Db.Slicing.Slice.t ->              to_call:Cil_types.kernel_function -> unit)             Pervasives.ref           val apply_all_internal :             (Db.Slicing.Project.t -> unit) Pervasives.ref           val apply_next_internal :             (Db.Slicing.Project.t -> unit) Pervasives.ref           val is_request_empty_internal :             (Db.Slicing.Project.t -> bool) Pervasives.ref           val merge_slices :             (Db.Slicing.Project.t ->              Db.Slicing.Slice.t ->              Db.Slicing.Slice.t -> replace:bool -> Db.Slicing.Slice.t)             Pervasives.ref           val copy_slice :             (Db.Slicing.Project.t -> Db.Slicing.Slice.t -> Db.Slicing.Slice.t)             Pervasives.ref           val split_slice :             (Db.Slicing.Project.t ->              Db.Slicing.Slice.t -> Db.Slicing.Slice.t list)             Pervasives.ref           val propagate_user_marks :             (Db.Slicing.Project.t -> unit) Pervasives.ref           val pretty :             (Format.formatter -> Db.Slicing.Project.t -> unit) Pervasives.ref         end     end   module type INOUTKF =     sig       type t       val self_internal : State.t Pervasives.ref       val self_external : State.t Pervasives.ref       val compute : (Cil_types.kernel_function -> unit) Pervasives.ref       val get_internal :         (Cil_types.kernel_function -> Db.INOUTKF.t) Pervasives.ref       val get_external :         (Cil_types.kernel_function -> Db.INOUTKF.t) Pervasives.ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit)         Pervasives.ref       val pretty : Format.formatter -> Db.INOUTKF.t -> unit     end   module type INOUT =     sig       type t       val self_internal : State.t ref       val self_external : State.t ref       val compute : (Cil_types.kernel_function -> unit) ref       val get_internal : (Cil_types.kernel_function -> t) ref       val get_external : (Cil_types.kernel_function -> t) ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit) ref       val pretty : Format.formatter -> t -> unit       val statement : (Cil_types.stmt -> t) Pervasives.ref       val kinstr : Cil_types.kinstr -> t option     end   module Inputs :     sig       type t = Locations.Zone.t       val self_internal : State.t ref       val self_external : State.t ref       val compute : (Cil_types.kernel_function -> unit) ref       val get_internal : (Cil_types.kernel_function -> t) ref       val get_external : (Cil_types.kernel_function -> t) ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit) ref       val pretty : Format.formatter -> t -> unit       val statement : (Cil_types.stmt -> t) ref       val kinstr : Cil_types.kinstr -> t option       val expr : (Cil_types.stmt -> Cil_types.exp -> t) Pervasives.ref       val self_with_formals : State.t Pervasives.ref       val get_with_formals : (Cil_types.kernel_function -> t) Pervasives.ref       val display_with_formals :         (Format.formatter -> Cil_types.kernel_function -> unit)         Pervasives.ref     end   module Outputs :     sig       type t = Locations.Zone.t       val self_internal : State.t ref       val self_external : State.t ref       val compute : (Cil_types.kernel_function -> unit) ref       val get_internal : (Cil_types.kernel_function -> t) ref       val get_external : (Cil_types.kernel_function -> t) ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit) ref       val pretty : Format.formatter -> t -> unit       val statement : (Cil_types.stmt -> t) ref       val kinstr : Cil_types.kinstr -> t option       val display_external :         (Format.formatter -> Cil_types.kernel_function -> unit)         Pervasives.ref     end   module Operational_inputs :     sig       type t = Inout_type.t       val self_internal : State.t ref       val self_external : State.t ref       val compute : (Cil_types.kernel_function -> unit) ref       val get_internal : (Cil_types.kernel_function -> t) ref       val get_external : (Cil_types.kernel_function -> t) ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit) ref       val pretty : Format.formatter -> t -> unit       val get_internal_precise :         (?stmt:Cil_types.stmt -> Cil_types.kernel_function -> Inout_type.t)         Pervasives.ref       module Record_Inout_Callbacks :         sig           type param = Value_types.callstack * Inout_type.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     end   module Derefs :     sig       type t = Locations.Zone.t       val self_internal : State.t ref       val self_external : State.t ref       val compute : (Cil_types.kernel_function -> unit) ref       val get_internal : (Cil_types.kernel_function -> t) ref       val get_external : (Cil_types.kernel_function -> t) ref       val display :         (Format.formatter -> Cil_types.kernel_function -> unit) ref       val pretty : Format.formatter -> t -> unit       val statement : (Cil_types.stmt -> t) ref       val kinstr : Cil_types.kinstr -> t option     end   val progress : (unit -> unit) Pervasives.ref   exception Cancel end