jon.recoil.org

Parameter Make_value.V

type t

Abstract value for each component of the domain.

val top : Witnesses.t -> V.t

Property may not hold on some paths.

val safe : V.t

Property holds on all paths.

val bot : V.t

Not reachable.

val lessequal : V.t -> V.t -> bool

Order of the abstract domain

val join : V.t -> V.t -> V.t
val meet : V.t -> V.t -> V.t
val compare : V.t -> V.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 -> Stdlib.Format.formatter -> V.t -> unit