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