Parameter Make.X

type t

Type of abstract values

val bot : t

The bottom element \bot (most precise element)

val is_bot : t -> bool

Tests whether an element is \bot

val top : t

The top element \top (less precise element)

val leq : t -> t -> bool

Inclusion test between abstract values. Smaller elements are more precise; larger elements are less precise. This might not be a total order, and might not be anti-symmetric either.

val join : t -> t -> t

Abstract union of abstract values. This need not be the least upper bound for leq, nor an upper bound at all.

val widen : t -> t -> t

Widening operator, i.e., an approximation of the concrete union, that is used the ensure the convergence of Kleene-based iterations.

val meet : t -> t -> t

Abstract intersection of abstract values. This need not be the greatest lower bound for leq, nor a lower bound at all.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for abstract values