Functor Eval_slevel.Computer

module Computer: 
functor (AnalysisParam : Arg) -> sig .. end
Parameters:
AnalysisParam : Arg

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 slevel : Cil_types.stmt -> int
type diff = {
   mutable to_propagate : State_set.t;
}
State propagated by the dataflow, that contains only 'new' states (i.e. not propagated before). All the states that have been seen so far are stored in an object of type
type stmt_state = {
   superposition : State_imp.t; (*
Bottom if we have never consumed all the slevel allocated. If no more slevel is available, the state that is being propgated. This state is *not* present in superposition.
*)
   mutable widening_state : Cvalue.Model.t; (*
should we widen the statement at the current iteration. widening_state is decremented each time we visit the statement, unless it is equal to zero. (In which case we widen, and set widening_state to a non-zero value, currently 1.)
*)
   mutable widening : int; (*
Number of states that were put in superposition; i.e. the sum of the cardinals of the state sets that were added with update_and_tell_if_changed. It may be different (i.e. larger) from the cardinal of state_imp, that merge states that are equal.
*)
   mutable counter_unroll : int;
}
The real state for a given statement, used in particular to detect convergence. Stored by us, not by the dataflow itself.
val empty_record : unit -> stmt_state
type t = stmt_state Cil_datatype.Stmt.Hashtbl.t 
val current_table : t
val stmt_state : Cil_datatype.Stmt.Hashtbl.key -> 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
Clobbered list for bases containing addresses of local variables.
val cacheable : Value_types.cacheable Pervasives.ref
module DataflowArg: sig .. end
module Dataflow: Dataflow2.Forwards(DataflowArg)
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