jon.recoil.org

Module type Zero_alloc_utils.Component

type t

Abstract value for each component of the domain.

type witnesses
val top : witnesses -> 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 -> Stdlib.Format.formatter -> t -> unit