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 reduce_by_cond :
        (Db.Value.state -> Cil_types.exp -> bool -> Db.Value.state)
        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 ->
         ?with_alarms:CilE.warn_mode ->
         Cil_types.lval -> 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_state :
        (?with_alarms:CilE.warn_mode ->
         Db.Value.state ->
         Cil_types.lval ->
         Db.Value.state * Precise_locs.precise_location * Cil_types.typ)
        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.assigns -> Locations.Zone.t)
        Pervasives.ref
      val assigns_outputs_to_zone :
        (Db.Value.state ->
         result:Cil_types.varinfo option ->
         Cil_types.assigns -> Locations.Zone.t)
        Pervasives.ref
      val assigns_outputs_to_locations :
        (Db.Value.state ->
         result:Cil_types.varinfo option ->
         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 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) Pervasives.ref
      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 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
      val self : State.t 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_initialized_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
      val get_float_to_int_status :
        (unit -> Db.RteGen.status_accessor) Pervasives.ref
      val get_finite_float_status :
        (unit -> Db.RteGen.status_accessor) 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 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 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