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