Module Eva_results

module Eva_results: sig .. end

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.

Results

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