module Computer: functor (
AnalysisParam
:
Arg
) ->
sig
.. end
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 = {
}
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 ; |
|
mutable widening_state : Cvalue.Model.t ; |
|
mutable widening : int ; |
|
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