module DepsOrUnassigned:sig
..end
type
deps_or_unassigned =
| |
DepsBottom |
(* |
Bottom of the lattice, never bound inside a memory state
at a valid location. (May appear for bases for which the
validity does not start at 0, currently only NULL.)
| *) |
| |
Unassigned |
(* |
Location has never been assigned
| *) |
| |
AssignedFrom of |
(* |
Location guaranteed to have been overwritten,
its contents depend on the
Deps.t value | *) |
| |
MaybeAssignedFrom of |
(* |
Location may or may not have been
overwritten
| *) |
DepsBottom <= Unassigned
, DepsBottom <= AssignedFrom z
,
Unassigned <= MaybeAssignedFrom
and
AssignedFrom z <= MaybeAssignedFrom z
.include Lmap_bitwise.With_default
val subst : (Function_Froms.Deps.t -> Function_Froms.Deps.t) -> t -> t
val extract_data : t -> Locations.Zone.t
val extract_indirect : t -> Locations.Zone.t
val may_be_unassigned : t -> bool
val compose : t -> t -> t
compose d1 d2
is the sequential composition of d1
after d2
, ie.
the dependencies needed to execute d1
after having executed d2
.
It is computed as d1
if d1 = AssignedFrom _
(as executing d1
completely overwrites what d2
wrote), and as a partial join between
d1
and d2
in the other cases.val pretty_precise : Format.formatter -> t -> unit
val to_zone : t -> Locations.Zone.t
val to_deps : t -> Function_Froms.Deps.deps