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