Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Control.Exception

Contents

Predefined exceptions

Description

Synopsis

data AssertionError = AssertionError
data VerificationConditions
- = AssertionViolation
- | AssumptionViolation

Predefined exceptions

data AssertionError Source #

Assertion error.

Constructors

AssertionError

Instances

Instances details

Generic AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Associated Types type Rep AssertionError :: Type -> Type # Methods from :: AssertionError -> Rep AssertionError x # to :: Rep AssertionError x -> AssertionError #
Show AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods showsPrec :: Int -> AssertionError -> ShowS # show :: AssertionError -> String # showList :: [AssertionError] -> ShowS #
NFData AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods rnf :: AssertionError -> () #
Eq AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods (==) :: AssertionError -> AssertionError -> Bool # (/=) :: AssertionError -> AssertionError -> Bool #
Ord AssertionError Source #
Instance details Defined in Grisette.Internal.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 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> AssertionError -> AssertionError Source #
ExtractSymbolics AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: AssertionError -> SymbolSet Source #
Mergeable AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy AssertionError Source #
SEq AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: AssertionError -> AssertionError -> SymBool Source # (./=) :: AssertionError -> AssertionError -> SymBool Source #
SOrd AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: AssertionError -> AssertionError -> SymBool Source # (.<=) :: AssertionError -> AssertionError -> SymBool Source # (.>) :: AssertionError -> AssertionError -> SymBool Source # (.>=) :: AssertionError -> AssertionError -> SymBool Source # symCompare :: AssertionError -> AssertionError -> UnionM Ordering Source #
SimpleMergeable AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> AssertionError -> AssertionError -> AssertionError Source #
AllSyms AssertionError Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: AssertionError -> [SomeSym] -> [SomeSym] Source # allSyms :: AssertionError -> [SomeSym] Source #
TransformError ArithException AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: ArithException -> AssertionError Source #
TransformError ArrayException AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: ArrayException -> AssertionError Source #
TransformError AssertionError AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: AssertionError -> AssertionError Source #
TransformError AssertionError VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: AssertionError -> VerificationConditions Source #
ToCon AssertionError AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: AssertionError -> Maybe AssertionError Source #
ToSym AssertionError AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: AssertionError -> AssertionError Source #
type Rep AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception type Rep AssertionError = D1 ('MetaData "AssertionError" "Grisette.Internal.Core.Control.Exception" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'False) (C1 ('MetaCons "AssertionError" 'PrefixI 'False) (U1 :: Type -> Type))

data VerificationConditions Source #

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

Constructors

AssertionViolation
AssumptionViolation

Instances

Instances details

Generic VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Associated Types type Rep VerificationConditions :: Type -> Type # Methods from :: VerificationConditions -> Rep VerificationConditions x # to :: Rep VerificationConditions x -> VerificationConditions #
Show VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods showsPrec :: Int -> VerificationConditions -> ShowS # show :: VerificationConditions -> String # showList :: [VerificationConditions] -> ShowS #
NFData VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods rnf :: VerificationConditions -> () #
Eq VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception Methods (==) :: VerificationConditions -> VerificationConditions -> Bool # (/=) :: VerificationConditions -> VerificationConditions -> Bool #
Ord VerificationConditions Source #
Instance details Defined in Grisette.Internal.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 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> VerificationConditions -> VerificationConditions Source #
ExtractSymbolics VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: VerificationConditions -> SymbolSet Source #
Mergeable VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy VerificationConditions Source #
SEq VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: VerificationConditions -> VerificationConditions -> SymBool Source # (./=) :: VerificationConditions -> VerificationConditions -> SymBool Source #
SOrd VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.<=) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>=) :: VerificationConditions -> VerificationConditions -> SymBool Source # symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering Source #
AllSyms VerificationConditions Source #
Instance details Defined in Grisette.Internal.SymPrim.AllSyms Methods allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym] Source # allSyms :: VerificationConditions -> [SomeSym] Source #
TransformError AssertionError VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: AssertionError -> VerificationConditions Source #
TransformError VerificationConditions VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: VerificationConditions -> VerificationConditions Source #
ToCon VerificationConditions VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: VerificationConditions -> Maybe VerificationConditions Source #
ToSym VerificationConditions VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: VerificationConditions -> VerificationConditions Source #
type Rep VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Control.Exception type Rep VerificationConditions = D1 ('MetaData "VerificationConditions" "Grisette.Internal.Core.Control.Exception" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))