Module Current_table

module Current_table: sig .. end
Internal state of the Value Analysis during analysis.

type state_imp = State_imp.t 
The array of all the states associated to a statement. It uses a different (imperative) structure than the functional State_set, but this is hidden by this interface where all the functions only use State_set.
type record = {
   superposition : State_imp.t;
   mutable widening : int;
   mutable widening_state : Cvalue.Model.t;
   mutable counter_unroll : int;
}
State on one statement
val empty_record : unit -> record
type t = record Cil_datatype.Stmt.Hashtbl.t 
State for an entire function
val create : unit -> 'a Cil_datatype.Stmt.Hashtbl.t
val clear : 'a Cil_datatype.Stmt.Hashtbl.t -> unit
val find_current : record Cil_datatype.Stmt.Hashtbl.t ->
Cil_datatype.Stmt.Hashtbl.key -> record
val find_widening_info : record Cil_datatype.Stmt.Hashtbl.t ->
Cil_datatype.Stmt.Hashtbl.key -> int * Cvalue.Model.t
Extraction
val update_and_tell_if_changed : record Cil_datatype.Stmt.Hashtbl.t ->
Cil_datatype.Stmt.Hashtbl.key -> State_set.t -> State_set.t
Updating
val update_widening_info : record Cil_datatype.Stmt.Hashtbl.t ->
Cil_datatype.Stmt.Hashtbl.key -> int -> Cvalue.Model.t -> unit
val merge_db_table : Db.Value.state Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
Db.Value.callstack -> unit
Merge the results of the current analysis with the global results. Honor -no-results* options
val superpositions : record Cil_datatype.Stmt.Hashtbl.t ->
Cvalue.Model.t list Cil_datatype.Stmt.Hashtbl.t
Export
val states : record Cil_datatype.Stmt.Hashtbl.t ->
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t
val find_superposition : record Cil_datatype.Stmt.Hashtbl.t ->
Cil_datatype.Stmt.Hashtbl.key -> State_set.t