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 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 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.
val print_summary : unit -> unit
Prints a summary of the analysis.