ExplicitTrace.FiniteSet
A powerset domain of traces, with bottom = empty and join = union
include AbstractDomain.FiniteSetS
include IStdlib.PrettyPrintable.PPSet
val is_singleton_or_more : t -> elt IStdlib.IContainer.singleton_or_more
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp_element : IStdlib.PrettyPrintable.F.formatter -> elt -> unit
include AbstractDomain.WithBottom with type t := t
include AbstractDomain.S with type t := t
include AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val bottom : t
The bottom value of the domain.
val is_bottom : t -> bool
Return true if this is the bottom value
val with_callsite : t -> CallSite.t -> t
Push given callsite onto all traces in set. Cf TraceElem.with_callsite