Module AbstractDomain.PairDisjunct

Parameters

module Domain1 : Disjunct
module Domain2 : Disjunct

Signature

include Comparable with type t = Domain1.t * Domain2.t
include IStdlib.PrettyPrintable.PrintableType with type t = Domain1.t * Domain2.t
type t = Domain1.t * Domain2.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)