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 | *) |
| |
MaybeAssignedFrom of |
(* | Location may or may not have been overwritten | *) |
The lattice is 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