Debugging and Assertion Control (GNAT User’s Guide for Native Platforms)

#### 4.3.5 Debugging and Assertion Control ¶

`-gnata`

  The `-gnata` option is equivalent to the following `Assertion_Policy` pragma:

      pragma Assertion_Policy (Check);

  Which is a shorthand for:

      pragma Assertion_Policy
      --  Ada RM assertion pragmas
        (Assert                    => Check,
         Static_Predicate          => Check,
         Dynamic_Predicate         => Check,
         Pre                       => Check,
         Pre'Class                 => Check,
         Post                      => Check,
         Post'Class                => Check,
         Type_Invariant            => Check,
         Type_Invariant'Class      => Check,
         Default_Initial_Condition => Check,
      --  GNAT specific assertion pragmas
         Assert_And_Cut            => Check,
         Assume                    => Check,
         Contract_Cases            => Check,
         Debug                     => Check,
         Ghost                     => Check,
         Initial_Condition         => Check,
         Loop_Invariant            => Check,
         Loop_Variant              => Check,
         Postcondition             => Check,
         Precondition              => Check,
         Predicate                 => Check,
         Refined_Post              => Check,
         Subprogram_Variant        => Check);

  The pragmas `Assert` and `Debug` normally have no effect and are ignored. This switch, where `a` stands for ‘assert’, causes pragmas `Assert` and `Debug` to be activated. This switch also causes preconditions, postconditions, subtype predicates, and type invariants to be activated.

  The pragmas have the form:

      pragma Assert (<Boolean-expression> [, <static-string-expression>])
      pragma Debug (<procedure call>)
      pragma Type_Invariant (<type-local-name>, <Boolean-expression>)
      pragma Predicate (<type-local-name>, <Boolean-expression>)
      pragma Precondition (<Boolean-expression>, <string-expression>)
      pragma Postcondition (<Boolean-expression>, <string-expression>)

  The aspects have the form:

      with [Pre|Post|Type_Invariant|Dynamic_Predicate|Static_Predicate]
        => <Boolean-expression>;

  The `Assert` pragma causes `Boolean-expression` to be tested. If the result is `True`, the pragma has no effect (other than possible side effects from evaluating the expression). If the result is `False`, the exception `Assert_Failure` declared in the package `System.Assertions` is raised (passing `static-string-expression`, if present, as the message associated with the exception). If no string expression is given, the default is a string containing the file name and line number of the pragma.

  The `Debug` pragma causes `procedure` to be called. Note that `pragma Debug` may appear within a declaration sequence, allowing debugging procedures to be called between declarations.

  For the aspect specification, the `Boolean-expression` is evaluated. If the result is `True`, the aspect has no effect. If the result is `False`, the exception `Assert_Failure` is raised.