Module From_compute

module From_compute: sig .. end
Additional control dependencies to add to all modified variables, coming from the control statements encountered so far (If, Switch). The statement information is used to remove the dependencies that are no longer useful, when we reach a statement that post-dominates the statement that gave rise to the dependency.

Module implementing the computation of functional dependencies


exception Call_did_not_take_place
Exception indicating that a given call statement was not evaluated.
module type Froms_To_Use_Sig = sig .. end
Signature of the module explaining how to find the Froms for a given call during the analysis.
module type Values_To_Use_Sig = sig .. end
Signature of the module explaining how to evaluatue some values during the analysis.
module type Recording_Sig = sig .. end
Module explaining how results should be recorded.
val find_deps_no_transitivity : Db.Value.state -> Cil_types.exp -> Function_Froms.Deps.t
Direct computation of the dependencies on expressions, offsets and lvals. The state at the statement is taken from Values_To_Use
val find_deps_lval_no_transitivity : Db.Value.state -> Cil_types.lval -> Function_Froms.Deps.t
val update : Locations.Zone.t ->
bool ->
Function_Froms.Memory.y -> Function_Froms.Memory.t -> Function_Froms.Memory.t
val compute_using_prototype_for_state : Db.Value.state -> Kernel_function.t -> Function_Froms.froms
Function that compute the Froms from a given prototype, called in the given state
module ZoneStmtMap: sig .. end
module Make: 
functor (Values_To_Use : Values_To_Use_Sig) ->
functor (Froms_To_Use : Froms_To_Use_Sig) ->
functor (Recording_To_Do : Recording_Sig) -> sig .. end
Functor computing the functional dependencies, according to the three modules above.