2.14 Pragma Assertion_Policy ¶

Syntax:

pragma Assertion_Policy (CHECK | DISABLE | IGNORE | SUPPRESSIBLE);

pragma Assertion_Policy (
    ASSERTION_KIND => POLICY_IDENTIFIER
 {, ASSERTION_KIND => POLICY_IDENTIFIER});

ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND

RM_ASSERTION_KIND ::= Assert                    |
                      Static_Predicate          |
                      Dynamic_Predicate         |
                      Pre                       |
                      Pre'Class                 |
                      Post                      |
                      Post'Class                |
                      Type_Invariant            |
                      Type_Invariant'Class      |
                      Default_Initial_Condition

ID_ASSERTION_KIND ::= Assertions           |
                      Assert_And_Cut       |
                      Assume               |
                      Contract_Cases       |
                      Debug                |
                      Ghost                |
                      Initial_Condition    |
                      Invariant            |
                      Invariant'Class      |
                      Loop_Invariant       |
                      Loop_Variant         |
                      Postcondition        |
                      Precondition         |
                      Predicate            |
                      Refined_Post         |
                      Statement_Assertions |
                      Subprogram_Variant

POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible

This is a standard Ada 2012 pragma that is available as an implementation-defined pragma in earlier versions of Ada. The assertion kinds RM_ASSERTION_KIND are those defined in the Ada standard. The assertion kinds ID_ASSERTION_KIND are implementation defined additions recognized by the GNAT compiler.

The pragma applies in both cases to pragmas and aspects with matching names, e.g. Pre applies to the Pre aspect, and Precondition applies to both the Precondition pragma and the aspect Precondition. Note that the identifiers for pragmas Pre_Class and Post_Class are Pre’Class and Post’Class (not Pre_Class and Post_Class), since these pragmas are intended to be identical to the corresponding aspects).

If the policy is CHECK, then assertions are enabled, i.e. the corresponding pragma or aspect is activated. If the policy is IGNORE, then assertions are ignored, i.e. the corresponding pragma or aspect is deactivated. This pragma overrides the effect of the `-gnata' switch on the command line. If the policy is SUPPRESSIBLE, then assertions are enabled by default, however, if the `-gnatp' switch is specified all assertions are ignored.

The implementation defined policy DISABLE is like IGNORE except that it completely disables semantic checking of the corresponding pragma or aspect. This is useful when the pragma or aspect argument references subprograms in a with’ed package which is replaced by a dummy package for the final build.

The implementation defined assertion kind Assertions applies to all assertion kinds. The form with no assertion kind given implies this choice, so it applies to all assertion kinds (RM defined, and implementation defined).

The implementation defined assertion kind Statement_Assertions applies to Assert, Assert_And_Cut, Assume, Loop_Invariant, and Loop_Variant.