11.1. Exception Declarations¶
No additions or restrictions
11.2. Exception Handlers¶
Exception handlers are not permitted in SPARK.
11.3. Raise Statements¶
Raise statements are in SPARK, but must (as described below) be provably never executed.
raise_statementintroduces an obligation to prove that the statement will not be executed, much like the verification condition associated with
pragma Assert (False);
[In other words, the verification conditions introduced for a raise statement are the same as those introduced for a run-time check which fails unconditionally.]
11.4. Exception Handling¶
No additions or restrictions but exception handlers are not permitted in SPARK.
11.4.1. The Package Exceptions¶
11.4.2. Pragmas Assert and Assertion_Policy¶
Unsuppressare allowed in SPARK, but have no effect on the generation of verification conditions. [For example, an array index value must be shown to be in bounds regardless of whether Index_Check is suppressed at the point of the array indexing.]
The following SPARK defined aspects and pragmas are assertions and their Boolean_
expressionsare assertion expressions:
There is an assertion_
aspect_markfor each of these aspects and pragmas with the same identifier as the corresponding aspect or pragma. In addition, Ghost is a SPARK defined assertion_
An implementation may introduce further implementation defined assertion_
aspect_markssome of which may apply to groups of these assertions.