Pragma Assertion_Policy (GNAT Reference Manual)

### 2.17 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 | ASSERTION_LEVEL

    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.

Additionally the pragma can apply to an assertion level defined by the `Assertion_Level` pragma. For more details see the SPARK 2014 Reference Manual, section 11.4.2.

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`.