Module Function_Froms.DepsOrUnassigned

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 Function_Froms.Deps.t (*
Location guaranteed to have been overwritten, its contents depend on the Deps.t value
*)
| MaybeAssignedFrom of Function_Froms.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.
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