jon.recoil.org

Module Zero_alloc_utils.Make_componentSource

Parameters

module Witnesses : WS

Signature

Sourcetype t =
  1. | Top of Witnesses.t
  2. | Safe
  3. | Bot
include Component with type witnesses := Witnesses.t and type t := t
Sourceval top : Witnesses.t -> t

Property may not hold on some paths.

Sourceval safe : t

Property holds on all paths.

Sourceval bot : t

Not reachable.

Sourceval lessequal : t -> t -> bool

Order of the abstract domain

Sourceval join : t -> t -> t
Sourceval meet : t -> t -> t
Sourceval 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.

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