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

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 ( [, ]) pragma Debug () pragma Type_Invariant (, ) pragma Predicate (, ) pragma Precondition (, ) pragma Postcondition (, )

The aspects have the form:

with [Pre|Post|Type_Invariant|Dynamic_Predicate|Static_Predicate] => ;

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 isFalse, the exception Assert_Failure declared in the packageSystem.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 thatpragma 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.