functor (AnalysisParam : Arg->
  sig
    val current_kf : Cil_types.kernel_function
    val current_fundec : Cil_types.fundec
    val return : Cil_types.stmt
    val return_lv : Cil_types.lval option
    val is_natural_loop : Cil_datatype.Stmt.Set.elt -> bool
    val is_basic_loop : Cil_types.stmt -> bool
    val is_loop : Cil_datatype.Stmt.Set.elt -> bool
    val obviously_terminates : Value_parameters.ObviouslyTerminatesAll.t
    val slevel : Cil_types.stmt -> int
    val initial_state : Cvalue.Model.t
    type diff = { mutable to_propagate : State_set.t; }
    type stmt_state = {
      superposition : State_imp.t;
      mutable widening_state : Cvalue.Model.t;
      mutable widening : int;
      mutable counter_unroll : int;
    }
    val empty_record : unit -> Eval_slevel.Computer.stmt_state
    type t = Eval_slevel.Computer.stmt_state Cil_datatype.Stmt.Hashtbl.t
    val current_table : Eval_slevel.Computer.t
    val stmt_state :
      Cil_datatype.Stmt.Hashtbl.key -> Eval_slevel.Computer.stmt_state
    val stmt_widening_info :
      Cil_datatype.Stmt.Hashtbl.key -> int * Cvalue.Model.t
    val update_stmt_states :
      Cil_datatype.Stmt.Hashtbl.key -> State_set.t -> State_set.t
    val update_stmt_widening_info :
      Cil_datatype.Stmt.Hashtbl.key -> int -> Cvalue.Model.t -> unit
    val states_unmerged_for_callbacks :
      unit -> Cvalue.Model.t list Cil_datatype.Stmt.Hashtbl.t
    val states_for_callbacks :
      unit -> Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t
    val states_unmerged : Cil_datatype.Stmt.Hashtbl.key -> State_set.t
    val states_after : Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t
    val store_state_after_during_dataflow :
      Cil_types.stmt -> Cil_types.stmt -> bool
    val local_after_states :
      Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
      Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t lazy_t
    val conditions_table : int Cil_datatype.Stmt.Hashtbl.t
    val merge_results : unit -> Db.Value.Record_Value_After_Callbacks.result
    val clob : Locals_scoping.clobbered_set
    val cacheable : Value_types.cacheable Pervasives.ref
    module DataflowArg :
      sig
        val name : string
        val debug : bool
        type t = diff
        val copy : t -> t
        val pretty : Format.formatter -> t -> unit
        val computeFirstPredecessor : Cil_types.stmt -> t -> t
        val combinePredecessors : Cil_types.stmt -> old:t -> t -> t option
        val doInstr : Cil_types.stmt -> Cil_types.instr -> t -> t
        val doGuard :
          Cil_types.stmt ->
          Cil_types.exp ->
          t -> t Dataflow2.guardaction * t Dataflow2.guardaction
        val doStmt : Cil_types.stmt -> t -> t Dataflow2.stmtaction
        val doEdge : Cil_types.stmt -> Cil_types.stmt -> t -> t
        module StmtStartData :
          sig
            type data = t
            val clear : unit -> unit
            val mem : Cil_types.stmt -> bool
            val find : Cil_types.stmt -> data
            val replace : Cil_types.stmt -> data -> unit
            val add : Cil_types.stmt -> data -> unit
            val iter : (Cil_types.stmt -> data -> unit) -> unit
            val length : unit -> int
          end
      end
    module Dataflow : sig val compute : Cil_types.stmt list -> unit end
    val mark_degeneration : unit -> unit
    val checkConvergence : unit -> unit
    val final_states : unit -> State_set.t
    val externalize :
      State_set.t -> (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list
    val results : unit -> Value_types.call_result
    val compute : State_set.t -> unit
  end