module Value_results:sig
..end
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
val is_non_terminating_instr : Cil_types.stmt -> bool
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.typestate_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
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