Parameter With_Cardinality._

include Lattice_type.AI_Lattice_with_cardinal_one with type t := Value.t
include Lattice_type.Bottom_Bounded_Join_Semi_Lattice with type t := Value.t
include Lattice_type.Join_Semi_Lattice with type t := Value.t

datatype of element of the lattice

include Datatype.S with type t := Value.t
include Datatype.S_no_copy with type t := Value.t
include Datatype.Ty with type t := Value.t
val ty : Value.t Type.t
val datatype_name : string

Unique name of the datatype.

val datatype_descr : Value.t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : Value.t list

List of representants of the descriptor.

val equal : Value.t -> Value.t -> bool

Equality: same spec than Stdlib.(=).

val compare : Value.t -> Value.t -> int

Comparison: same spec than Stdlib.compare.

val hash : Value.t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Stdlib.Format.formatter -> Value.t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> Value.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 copy : Value.t -> Value.t

Deep copy: no possible sharing between x and copy x.

val join : Value.t -> Value.t -> Value.t

over-approximation of union

val is_included : Value.t -> Value.t -> bool

is first argument included in the second?

val bottom : Value.t

smallest element

include Lattice_type.With_Top with type t := Value.t
val top : Value.t

largest element

include Lattice_type.With_Cardinal_One with type t := Value.t
val cardinal_zero_or_one : Value.t -> bool
include Lattice_type.With_Narrow with type t := Value.t
val narrow : Value.t -> Value.t -> Value.t

over-approximation of intersection

include Lattice_type.With_Under_Approximation with type t := Value.t

under-approximation of union

val meet : Value.t -> Value.t -> Value.t

under-approximation of intersection

include Lattice_type.With_Intersects with type t := Value.t
val intersects : Value.t -> Value.t -> bool

intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.

include Lattice_type.With_Diff with type t := Value.t
val diff : Value.t -> Value.t -> Value.t

diff t1 t2 is an over-approximation of t1-t2. t2 must be an under-approximation or exact.

include Lattice_type.With_Diff_One with type t := Value.t
val diff_if_one : Value.t -> Value.t -> Value.t

diff_if_one t1 t2 is an over-approximation of t1-t2.

  • returns

    t1 if t2 is not a singleton.

include Lattice_type.With_Enumeration with type t := Value.t
val fold_enum : (Value.t -> 'a -> 'a) -> Value.t -> 'a -> 'a

Fold on the elements of the value one by one if possible. Raises Abstract_interp.Not_less_than when there is an infinite number of elements to enumerate.

val cardinal_less_than : Value.t -> int -> int

Raises Abstract_interp.Not_less_than whenever the cardinal of the given lattice is strictly higher than the given integer.