module From:From_compute.Make
(
Value_local
)
(
Functionwise_From_to_use
)
(
Recording_To_Do
)
type
t' = {
|
additional_deps_table : |
(* | 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. | *) |
|
additional_deps : |
(* | Union of the sets in additional_deps_table | *) |
|
deps_table : |
(* | dependency table | *) |
val call_stack : Kernel_function.t Stack.t
val rebuild_additional_deps : From_compute.ZoneStmtMap.t -> Locations.Zone.t
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
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 -> indirectval 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
val compute : Kernel_function.t -> unit