Module Value_results

module Value_results: sig .. end

Is called

This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally.



Is called


module Is_Called: Kernel_function.Make_Table(Datatype.Bool)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val is_called : Is_Called.key -> Is_Called.data
val mark_kf_as_called : Is_Called.key -> unit

Callers


module Callers: Kernel_function.Make_Table(Kernel_function.Map.Make(Cil_datatype.Stmt.Set))(sig
val name : string
val dependencies : State.t list
val size : int
end)
val add_kf_caller : caller:Kernel_function.Map.key * Cil_datatype.Stmt.Set.elt ->
Callers.key -> unit
val callers : Callers.key ->
(Kernel_function.Map.key * Cil_datatype.Stmt.Set.elt list) list

Termination.


val partition_terminating_instr : Db.Value.AfterTable_By_Callstack.key ->
Value_types.Callstack.Hashtbl.key list *
Value_types.Callstack.Hashtbl.key 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 : Db.Value.AfterTable_By_Callstack.key -> 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.

Merging results.


type state_per_stmt = Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t 
val merge_states_in_db : Db.Value.state Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
Db.Value.callstack -> unit
val merge_after_states_in_db : Db.Value.state Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
Db.Value.callstack -> unit

Registration.