Module `AbstractDomain.Stacked`

Stacked abstract domain: tagged union of Below, Val, and Above domains where all elements of Below are strictly smaller than all elements of Val which are strictly smaller than all elements of Above

Parameters

Below : S
Val : S
Above : S

Signature

include NoJoin

include IStdlib.PrettyPrintable.PrintableType

type t

val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit

val leq : lhs:t -> rhs:t -> bool: the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t