Module Callwise

module Callwise: sig .. end
State for the analysis of one function call

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 : Kernel_function.t; (*
Function being analyzed
*)
   value_initial_state : Db.Value.state; (*
State of Value at the beginning of the call
*)
   table_for_calls : Function_Froms.t Cil_datatype.Kinstr.Hashtbl.t; (*
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
*)
}
State for the analysis of one function call
val call_froms_stack : from_state list Pervasives.ref
The state of the callwise From analysis. Only the top of this callstack is accessed. New calls are pushed on the stack when Value starts the analysis of a function, and popped when the analysis finisheds. This stack is manually synchronized with Value's callstack.
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