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.


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.