Parameter Make_value.V

type t

Abstract value for each component of the domain.

val top : Witnesses.t -> t

Property may not hold on some paths.

val safe : t

Property holds on all paths.

val bot : t

Not reachable.

val lessequal : t -> t -> bool

Order of the abstract domain

val join : t -> t -> t
val meet : t -> t -> t
val compare : t -> t -> int

Use compare for structural comparison of terms, for example to store them in a set. Use lessequal for checking fixed point of the abstract domain.

val print : witnesses:bool -> Format.formatter -> t -> unit