Module Value_results

module Value_results: sig .. end
This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally.

Is called



val mark_kf_as_called : Cil_types.kernel_function -> unit
val add_kf_caller : caller:Cil_types.kernel_function * Cil_types.stmt ->
Cil_types.kernel_function -> unit
val partition_terminating_instr : Cil_types.stmt -> Db.Value.callstack list * Db.Value.callstack list
Returns the list of terminating callstacks and the list of non-terminating callstacks. Must be called *only* on statements that are instructions.
val is_non_terminating_instr : Cil_types.stmt -> bool
Returns true iff there exists executions of the statement that does not always fail/loop (for function calls). Must be called *only* on statements that are instructions.
type state_per_stmt = Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t 
val merge_states_in_db : state_per_stmt Lazy.t -> Db.Value.callstack -> unit
val merge_after_states_in_db : state_per_stmt Lazy.t -> Db.Value.callstack -> unit