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