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 : Stdlib.Format.formatter -> t -> unit
val to_zone : t -> Locations.Zone.t
val to_deps : t -> Function_Froms.Deps.deps