module Callwise:sig
..end
Computation of callwise functional dependencies. The results are computed while the value analysis runs, and the results are usually much more precise than the functionwise results.
Nothing is exported here, the API can be found in the
Db.From.Callwise module
module Tbl:Cil_state_builder.Kinstr_hashtbl
(
Function_Froms
)
(
sig
val name :string
val size :int
val dependencies :State.t list
end
)
val merge_call_froms : Function_Froms.froms Cil_datatype.Kinstr.Hashtbl.t ->
Cil_datatype.Kinstr.Hashtbl.key -> Function_Froms.froms -> unit
type
from_state = {
|
current_function : |
(* |
Function being analyzed
| *) |
|
value_initial_state : |
(* |
State of Value at the beginning of
the call
| *) |
|
table_for_calls : |
(* |
State of the From plugin for each statement containing a function call
in the body of
current_function . Updated incrementally each time
Value analyses such a statement | *) |
val call_froms_stack : from_state list Pervasives.ref
val record_callwise_dependencies_in_db : Tbl.key -> Tbl.data -> unit
val call_for_individual_froms : Db.Value.state * (Kernel_function.t * Cil_datatype.Kinstr.Hashtbl.key) list ->
unit
val end_record : (Kernel_function.t * Tbl.key) list -> Tbl.data -> unit
module MemExec:State_builder.Hashtbl
(
Datatype.Int.Hashtbl
)
(
Function_Froms
)
(
sig
val size :int
val dependencies :State.t list
val name :string
end
)
val compute_call_from_value_states : Kernel_function.t ->
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t -> Function_Froms.t
val record_for_individual_froms : (Kernel_function.t * Tbl.key) list *
(Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t * 'a)
Value_types.callback_result -> unit
val force_compute_all_calldeps : unit -> unit