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 computing the functional dependencies, according to the three
modules above.