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.

None means multiple functions


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
type results 

Results


val get_results : unit -> results
val set_results : results -> unit
val merge : results -> results -> results
val change_callstacks : (Value_types.callstack -> Value_types.callstack) ->
results -> results
Change the callstacks for the results for which this is meaningful. For technical reasons, the top of the callstack must currently be preserved.