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

SEq AssertionError

Defined in Grisette.Core.Control.Exception

Methods

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

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

EvaluateSym AssertionError

Defined in Grisette.Core.Control.Exception

Methods

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

ExtractSymbolics AssertionError

Defined in Grisette.Core.Control.Exception

Methods

extractSymbolics :: AssertionError -> SymbolSet

Mergeable AssertionError

Defined in Grisette.Core.Control.Exception

Methods

rootStrategy :: MergingStrategy AssertionError

SOrd AssertionError

Defined in Grisette.Core.Control.Exception

Methods

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

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

(>~) :: AssertionError -> AssertionError -> SymBool

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

symCompare :: AssertionError -> AssertionError -> UnionM Ordering

SimpleMergeable AssertionError

Defined in Grisette.Core.Control.Exception

Methods

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

TransformError ArithException AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: ArithException -> AssertionError

TransformError ArrayException AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: ArrayException -> AssertionError

TransformError AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: AssertionError -> AssertionError

TransformError AssertionError VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

transformError :: AssertionError -> VerificationConditions

ToCon AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

Methods

toCon :: AssertionError -> Maybe AssertionError

ToSym AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

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.1.0.0-6BNF0pL4m6OHMsp5yKPRPi" '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

SEq VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

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

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

EvaluateSym VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

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

ExtractSymbolics VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

extractSymbolics :: VerificationConditions -> SymbolSet

Mergeable VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

rootStrategy :: MergingStrategy VerificationConditions

SOrd VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

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

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

(>~) :: VerificationConditions -> VerificationConditions -> SymBool

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

symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering

TransformError AssertionError VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

transformError :: AssertionError -> VerificationConditions

TransformError VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

transformError :: VerificationConditions -> VerificationConditions

ToCon VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

toCon :: VerificationConditions -> Maybe VerificationConditions

ToSym VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

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.1.0.0-6BNF0pL4m6OHMsp5yKPRPi" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))

symAssert :: (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()

Used within a monadic multi path computation to begin exception processing.

Checks the condition passed to the function. The current execution path will be terminated with assertion error if the condition is false.

If the condition is symbolic, Grisette will split the execution into two paths based on the condition. The symbolic execution will continue on the then-branch, where the condition is true. For the else branch, where the condition is false, the execution will be terminated.

The resulting monadic environment should be compatible with the AssertionError error type. See TransformError type class for details.

Examples:

Terminates the execution if the condition is false. Note that we may lose the Mergeable knowledge here if no possible execution path is viable. This may affect the efficiency in theory, but in practice this should not be a problem as all paths are terminated and no further evaluation would be performed.

>>> symAssert (con False) :: ExceptT AssertionError UnionM ()
ExceptT {Left AssertionError}
>>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT <Left AssertionError>

No effect if the condition is true:

>>> symAssert (con True) :: ExceptT AssertionError UnionM ()
ExceptT {Right ()}
>>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT {Right 1}

Splitting the path and terminate one of them when the condition is symbolic.

>>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()
ExceptT {If (! a) (Left AssertionError) (Right ())}
>>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT {If (! a) (Left AssertionError) (Right 1)}

AssertionError is compatible with VerificationConditions:

>>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()
ExceptT {If (! a) (Left AssertionViolation) (Right ())}

symAssume :: (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()

Used within a monadic multi path computation to begin exception processing.

Similar to symAssert, but terminates the execution path with AssumptionViolation error.

Examples:

>>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()
ExceptT {If (! a) (Left AssumptionViolation) (Right ())}