4.3.4 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
  (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);

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.