11.4.2 Pragmas Assert and Assertion_Policy

Pragma Assert is used to assert the truth of a boolean expression at a point within a sequence of declarations or statements.

 Assert pragmas, subtype predicates (see 3.2.4), preconditions and postconditions (see 6.1.1), type invariants (see 7.3.2), and default initial conditions (see 7.3.3) are collectively referred to as assertions; their boolean expressions are referred to as assertion expressions.

 Pragma Assertion_Policy is used to control whether assertions are to be ignored by the implementation, checked at run time, or handled in some implementation-defined manner. 

The expected type for the boolean_expression of a pragma Assert is any boolean type. The expected type for the string_expression of a pragma Assert is type String. 

The assertion_aspect_mark of a pragma Assertion_Policy shall identify an assertion aspect, namely one of Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class, Default_Initial_Condition, or some implementation-defined (assertion) aspect_mark. The policy_identifier shall be either Check, Ignore, or some implementation-defined identifier.

A pragma Assertion_Policy determines for each assertion aspect named in the pragma_argument_associations whether assertions of the given aspect are to be enforced by a runtime check. The policy_identifier Check requires that assertion expressions of the given aspect be checked that they evaluate to True at the points specified for the given aspect; the policy_identifier Ignore requires that the assertion expression not be evaluated at these points, and the runtime checks not be performed. Note that for subtype predicate aspects (see 3.2.4), even when the applicable Assertion_Policy is Ignore, the predicate will still be evaluated as part of membership tests and Valid attribute_references, and if static, will still have an effect on loop iteration over the subtype, and the selection of case_statement_alternatives and variants.

  If no assertion_aspect_marks are specified in the pragma, the specified policy applies to all assertion aspects.

  A pragma Assertion_Policy applies to the named assertion aspects in a specific region, and applies to all assertion expressions associated with those aspects specified in that region. A pragma Assertion_Policy given in a declarative_part or immediately within a package_specification applies from the place of the pragma to the end of the innermost enclosing declarative region. The region for a pragma Assertion_Policy given as a configuration pragma is the declarative region for the entire compilation unit (or units) to which it applies.

  If a pragma Assertion_Policy applies to a generic_instantiation, then the pragma Assertion_Policy applies to the entire instance.

  If multiple Assertion_Policy pragmas apply to a given construct for a given assertion aspect, the assertion policy is determined by the one in the innermost enclosing region of a pragma Assertion_Policy specifying a policy for the assertion aspect. If no such Assertion_Policy pragma exists, the policy is implementation defined.

The following language-defined library package exists:

A compilation unit containing a check for an assertion (including a pragma Assert) has a semantic dependence on the Assertions library unit.

If performing checks is required by the Assert assertion policy in effect at the place of a pragma Assert, the elaboration of the pragma consists of evaluating the boolean expression, and if the result is False, evaluating the Message argument, if any, and raising the exception Assertions.Assertion_Error, with a message if the Message argument is provided.

Calling the procedure Assertions.Assert without a Message parameter is equivalent to:

Calling the procedure Assertions.Assert with a Message parameter is equivalent to:

The procedures Assertions.Assert have these effects independently of the assertion policy in effect.

  It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of an assertion expression associated with a call on, or return from, a protected operation. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it can result in deadlock or a (nested) protected action. 

  Any postcondition expression, type invariant expression, or default initial condition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1, 7.3.2, and 7.3.3).

  The evaluation of any such postcondition, type invariant, or default initial condition expression shall either yield True or propagate an exception from a raise_expression that appears within the assertion expression.

  Any precondition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5). Similarly, any predicate checks for a subtype occurring in the specification of a language-defined unit are enabled (see 3.2.4) unless suppressed.

Assertion_Error may be declared by renaming an implementation-defined exception from another package. 

Implementations may define their own assertion policies.

If the result of a function call in an assertion is not used to determine the value of the assertion expression, an implementation is permitted to omit the function call. This permission applies even if the function has side effects.

An implementation may disallow the specification of an assertion expression if the evaluation of the expression has a side effect such that an immediate reevaluation of the expression can produce a different value. Similarly, an implementation may disallow the specification of an assertion expression that is checked as part of a call on or return from a callable entity C, if the evaluation of the expression has a side effect such that the evaluation of some other assertion expression associated with the same call of (or return from) C can produce a different value than in the case when the first expression had not been evaluated.