Grisette.Core.Control.Exception

Predefined exceptions

data AssertionError

Assertion error.

Constructors

AssertionError

Instances

Generic AssertionError

Defined in Grisette.Core.Control.Exception

Associated Types

type Rep AssertionError :: Type -> Type

Methods

from :: AssertionError -> Rep AssertionError x

to :: Rep AssertionError x -> AssertionError

Show AssertionError

Defined in Grisette.Core.Control.Exception

Methods

showsPrec :: Int -> AssertionError -> ShowS

show :: AssertionError -> String

showList :: [AssertionError] -> ShowS

NFData AssertionError

Defined in Grisette.Core.Control.Exception

Methods

rnf :: AssertionError -> ()

Eq AssertionError

Defined in Grisette.Core.Control.Exception

Methods

(==) :: AssertionError -> AssertionError -> Bool

(/=) :: AssertionError -> AssertionError -> Bool

Ord AssertionError

Defined in Grisette.Core.Control.Exception

Methods

compare :: AssertionError -> AssertionError -> Ordering

(<) :: AssertionError -> AssertionError -> Bool

(<=) :: AssertionError -> AssertionError -> Bool

(>) :: AssertionError -> AssertionError -> Bool

(>=) :: AssertionError -> AssertionError -> Bool

max :: AssertionError -> AssertionError -> AssertionError

min :: AssertionError -> AssertionError -> AssertionError

EvaluateSym AssertionError

Defined in Grisette.Core.Data.Class.EvaluateSym

Methods

evaluateSym :: Bool -> Model -> AssertionError -> AssertionError

ExtractSymbolics AssertionError

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: AssertionError -> SymbolSet

Mergeable AssertionError

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy AssertionError

SEq AssertionError

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: AssertionError -> AssertionError -> SymBool

(./=) :: AssertionError -> AssertionError -> SymBool

SOrd AssertionError

Defined in Grisette.Core.Data.Class.SOrd

Methods

(.<) :: AssertionError -> AssertionError -> SymBool

(.<=) :: AssertionError -> AssertionError -> SymBool

(.>) :: AssertionError -> AssertionError -> SymBool

(.>=) :: AssertionError -> AssertionError -> SymBool

symCompare :: AssertionError -> AssertionError -> UnionM Ordering

SimpleMergeable AssertionError

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> AssertionError -> AssertionError -> AssertionError

AllSyms AssertionError

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

allSymsS :: AssertionError -> [SomeSym] -> [SomeSym]

allSyms :: AssertionError -> [SomeSym]

TransformError ArithException AssertionError

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: ArithException -> AssertionError

TransformError ArrayException AssertionError

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: ArrayException -> AssertionError

TransformError AssertionError AssertionError

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: AssertionError -> AssertionError

TransformError AssertionError VerificationConditions

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: AssertionError -> VerificationConditions

ToCon AssertionError AssertionError

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: AssertionError -> Maybe AssertionError

ToSym AssertionError AssertionError

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: AssertionError -> AssertionError

type Rep AssertionError

Defined in Grisette.Core.Control.Exception

type Rep AssertionError = D1 ('MetaData "AssertionError" "Grisette.Core.Control.Exception" "grisette-0.4.1.0-9jHs6dkH5tjGix4ciXfUxj" 'False) (C1 ('MetaCons "AssertionError" 'PrefixI 'False) (U1 :: Type -> Type))

data VerificationConditions

Verification conditions. A crashed program path can terminate with either assertion violation errors or assumption violation errors.

Constructors

AssertionViolation

AssumptionViolation

Instances

Generic VerificationConditions

Defined in Grisette.Core.Control.Exception

Associated Types

type Rep VerificationConditions :: Type -> Type

Methods

from :: VerificationConditions -> Rep VerificationConditions x

to :: Rep VerificationConditions x -> VerificationConditions

Show VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

showsPrec :: Int -> VerificationConditions -> ShowS

show :: VerificationConditions -> String

showList :: [VerificationConditions] -> ShowS

NFData VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

rnf :: VerificationConditions -> ()

Eq VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

(==) :: VerificationConditions -> VerificationConditions -> Bool

(/=) :: VerificationConditions -> VerificationConditions -> Bool

Ord VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

compare :: VerificationConditions -> VerificationConditions -> Ordering

(<) :: VerificationConditions -> VerificationConditions -> Bool

(<=) :: VerificationConditions -> VerificationConditions -> Bool

(>) :: VerificationConditions -> VerificationConditions -> Bool

(>=) :: VerificationConditions -> VerificationConditions -> Bool

max :: VerificationConditions -> VerificationConditions -> VerificationConditions

min :: VerificationConditions -> VerificationConditions -> VerificationConditions

EvaluateSym VerificationConditions

Defined in Grisette.Core.Data.Class.EvaluateSym

Methods

evaluateSym :: Bool -> Model -> VerificationConditions -> VerificationConditions

ExtractSymbolics VerificationConditions

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Methods

extractSymbolics :: VerificationConditions -> SymbolSet

Mergeable VerificationConditions

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy VerificationConditions

SEq VerificationConditions

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: VerificationConditions -> VerificationConditions -> SymBool

(./=) :: VerificationConditions -> VerificationConditions -> SymBool

SOrd VerificationConditions

Defined in Grisette.Core.Data.Class.SOrd

Methods

(.<) :: VerificationConditions -> VerificationConditions -> SymBool

(.<=) :: VerificationConditions -> VerificationConditions -> SymBool

(.>) :: VerificationConditions -> VerificationConditions -> SymBool

(.>=) :: VerificationConditions -> VerificationConditions -> SymBool

symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering

AllSyms VerificationConditions

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym]

allSyms :: VerificationConditions -> [SomeSym]

TransformError AssertionError VerificationConditions

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: AssertionError -> VerificationConditions

TransformError VerificationConditions VerificationConditions

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: VerificationConditions -> VerificationConditions

ToCon VerificationConditions VerificationConditions

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: VerificationConditions -> Maybe VerificationConditions

ToSym VerificationConditions VerificationConditions

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: VerificationConditions -> VerificationConditions

type Rep VerificationConditions

Defined in Grisette.Core.Control.Exception

type Rep VerificationConditions = D1 ('MetaData "VerificationConditions" "Grisette.Core.Control.Exception" "grisette-0.4.1.0-9jHs6dkH5tjGix4ciXfUxj" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))