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

module Below : S
module Val : S
module Above : S

Signature

include Comparable with type t = (Below.t, Val.t, Above.t) Types.below_above
include IStdlib.PrettyPrintable.PrintableType with type t = (Below.t, Val.t, Above.t) Types.below_above
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