Parameter PairDisjunct.Domain2

include Comparable
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 equal_fast : t -> t -> bool

equal_fast x y must imply x <=> y; it's a good idea for this function to be "fast", e.g. not depend on the size of its input

val is_normal : t -> bool

test if the abstract state represents exactly concrete states

val is_exceptional : t -> bool

test if the abstract state represents exactly exceptional concrete states

val is_executable : t -> bool

test if the abstract state represents executable states, e.g. ContinueProgram or ExceptionRaised.

val exceptional_to_normal : t -> t

convert all exceptional states into normal states (used when reaching a handler)

val is_active_loop : t -> IR.Procdesc.Node.id option

test if the abstract state is a loop invariant under inference and return the corresponding loop header id