module From:From_compute.Make
(
To_Use
)
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.deps) ->
Function_Froms.Deps.deps -> Function_Froms.Deps.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 bind_locals : Cil_types.varinfo list -> Function_Froms.Memory.t -> Function_Froms.Memory.t
Assigned \from \nothing
. This function
is always called on local variables. We do *not* want to bind a local
variable v
to Unassigned, as otherwise we could get some dependencies
that refer to v
(when v
is not guaranteed to be always assigned, or
for padding in local structs), and that would need to be removed when v
goes out of scope. Moreover, semantically, v
*is* assigned (albeit to
"uninitalized", which represents an indefinite part of the stack). We
do not attemps to track this "uninitalized" information in From, as this
is redundant with the work done by Value -- hence the use of \nothing
.val find : Cil_types.stmt ->
Function_Froms.Memory.t -> Cil_types.exp -> Function_Froms.Deps.deps
val lval_to_zone_with_deps : Cil_types.stmt ->
for_writing:bool ->
Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool
val lval_to_precise_loc_with_deps : Cil_types.stmt ->
for_writing:bool ->
Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location * bool
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