jon.recoil.org

Module Assume_info.VSource

Sourcetype t : immutable_data = Make_component(Witnesses).t =
  1. | Top of Witnesses.t
  2. | Safe
  3. | Bot
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