functor
  (AnalysisParam : sig
                     val kf : Cil_types.kernel_function
                     val initial_states : State_set.t
                     val active_behaviors : Eval_annots.ActiveBehaviors.t
                   end->
  sig
    val debug : bool
    val name : string
    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 slevel_merge_after_loop : Value_parameters.SlevelMergeAfterLoop.t
    val obviously_terminates : Value_parameters.ObviouslyTerminatesAll.t
    val slevel : Per_stmt_slevel.slevel
    val slevel : Cil_types.stmt -> int
    val initial_state : Cvalue.Model.t
    val current_table : Current_table.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 merge_after :
      Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
      Db.Value.callstack -> unit
    val conditions_table : int Cil_datatype.Stmt.Hashtbl.t
    val merge_results : unit -> Db.Value.Record_Value_After_Callbacks.result
    type u = { mutable to_propagate : State_set.t; }
    module StmtStartData :
      sig
        type data = u
        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
    val mark_degeneration : unit -> unit
    type t = Eval_slevel.Computer.u
    val copy : Eval_slevel.Computer.t -> Eval_slevel.Computer.t
    val display_one : Format.formatter -> Eval_slevel.Computer.u -> unit
    val pretty : Format.formatter -> Eval_slevel.Computer.t -> unit
    val computeFirstPredecessor :
      Cil_types.stmt -> Eval_slevel.Computer.u -> Eval_slevel.Computer.u
    val counter_unroll_target : Value_parameters.ShowSlevel.t Pervasives.ref
    val is_return : Cil_types.stmt -> bool
    val combinePredecessors :
      Cil_types.stmt ->
      old:Eval_slevel.Computer.u ->
      Eval_slevel.Computer.u -> Eval_slevel.Computer.u option
    val clob : Locals_scoping.clobbered_set
    val cacheable : Value_types.cacheable Pervasives.ref
    val interp_call :
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil_types.exp -> Cil_types.exp list -> State_set.t -> State_set.t
    val doInstr :
      Cil_types.stmt ->
      Cil_types.instr -> Eval_slevel.Computer.t -> Eval_slevel.Computer.t
    val doStmtSpecific : Cil_types.stmt -> '-> State_set.t -> State_set.t
    val merge_if_loop : Cil_types.stmt -> Eval_slevel.Computer.t -> unit
    val doStmt :
      Cil_types.stmt ->
      Eval_slevel.Computer.t -> Eval_slevel.Computer.u Dataflow2.stmtaction
    val doEdge :
      Cil_datatype.Stmt.Hashtbl.key ->
      Cil_types.stmt -> Eval_slevel.Computer.u -> Eval_slevel.Computer.u
    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 doGuardOneCond :
      Cil_types.stmt ->
      CilE.syntactic_context ->
      Cil_types.exp ->
      Eval_slevel.Computer.u -> Eval_slevel.Computer.u Dataflow2.guardaction
    val mask_then : int
    val mask_else : int
    val mask_both : int
    val doGuard :
      Cil_datatype.Stmt.Hashtbl.key ->
      Cil_types.exp ->
      Eval_slevel.Computer.u ->
      Eval_slevel.Computer.u Dataflow2.guardaction *
      Eval_slevel.Computer.u Dataflow2.guardaction
  end