module Make:
Functor computing the functional dependencies, according to the three
modules above.
type
t' = {
|
additional_deps_table : From_compute.ZoneStmtMap.t ; |
|
additional_deps : Locations.Zone.t ; |
|
deps_table : Function_Froms.Memory.t ; |
}
val call_stack : Kernel_function.t Stack.t
Stack of function being processed
val rebuild_additional_deps : From_compute.ZoneStmtMap.t -> Locations.Zone.t
Recreate the additional_deps
field from additional_deps_table
val merge_deps : (Locations.Zone.t -> Function_Froms.Deps.t) ->
Function_Froms.Deps.from_deps -> Function_Froms.Deps.from_deps
given a Function_Froms.Deps.t
, apply f
on both components and merge
the result:
depending directly on an indirect dependency -> indirect,
depending indirectly on a direct dependency -> indirect
val find : Cil_types.stmt ->
Function_Froms.Memory.t -> Cil_types.exp -> Function_Froms.Deps.from_deps
val empty_from : t'
val bottom_from : t'
module Computer: sig
.. end
val externalize : Cil_types.stmt ->
Cil_types.kernel_function -> t' -> Function_Froms.froms
val compute_using_cfg : Kernel_function.t -> Function_Froms.froms
val compute_using_prototype : Kernel_function.t -> Function_Froms.froms
val compute_and_return : Kernel_function.t -> Function_Froms.t
Compute the dependencies of the given function, and return them
Compute the dependencies of the given function
val compute : Kernel_function.t -> unit