module Function_Froms:sig
..end
A From table is internally represented as a Lmap of DepsOrUnassigned
.
However, the API mostly hides this fact, and exports access functions
that take or return Deps.t
values. This way, the user needs not
understand the subtleties of DepsBottom/Unassigned/MaybeAssigned.
module Deps:sig
..end
module DepsOrUnassigned:sig
..end
module Memory:sig
..end
type
froms = {
|
deps_return : |
(* |
Dependencies for the returned value
| *) |
|
deps_table : |
(* |
Dependencies on all the zones modified by the function
| *) |
include Datatype.S
val join : froms -> froms -> froms
val top : froms
val pretty_with_type : Cil_types.typ -> froms Pretty_utils.formatter
val pretty_with_type_indirect : Cil_types.typ -> froms Pretty_utils.formatter
val outputs : froms -> Locations.Zone.t
val inputs : ?include_self:bool -> froms -> Locations.Zone.t
include_self
is true, and the from is
of the form x FROM y (and SELF)
, x
is added to the result;
default value is false
.