Assigns.DepsOrUnassigned
type t =
| 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 Deps.t
Location guaranteed to have been overwritten, its contents depend on the Deps.t
value
| MaybeAssignedFrom of Deps.t
Location may or may not have been overwritten
*)The lattice is DepsBottom <= Unassigned
, DepsBottom <= AssignedFrom z
, Unassigned <= MaybeAssignedFrom
and AssignedFrom z <= MaybeAssignedFrom z
.
val top : t
val may_be_unassigned : t -> bool
val to_zone : t -> Frama_c_kernel.Locations.Zone.t