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.