Predefined exceptions

Assertion error.

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

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 ())}

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 ())}