Function_Froms.DepsOrUnassigned
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 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
.
include Lmap_bitwise.With_default with type t = deps_or_unassigned
include Lattice_type.Bounded_Join_Semi_Lattice with type t = deps_or_unassigned
include Lattice_type.Join_Semi_Lattice with type t = deps_or_unassigned
datatype of element of the lattice
include Datatype.S with type t = deps_or_unassigned
include Datatype.S_no_copy with type t = deps_or_unassigned
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
val bottom : t
smallest element
include Lattice_type.With_Top with type t := t
val top : t
largest element
val default : t
val extract_data : t -> Locations.Zone.t
val extract_indirect : t -> Locations.Zone.t
val may_be_unassigned : t -> bool
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