Ada Reference Manual — Legal Information

11.4.2 Pragmas Assert and Assertion_Policy

Pragma Assert is used to assert the truth of a Boolean expression at any point within a sequence of declarations or statements. Pragma Assertion_Policy is used to control whether such assertions are to be ignored by the implementation, checked at run-time, or handled in some implementation-defined manner.

Syntax

2/2

The form of a pragma Assert is as follows:

3/2

pragma Assert([Check =>] boolean_expression[, [Message =>] string_expression]);

4/2

A pragma Assert is allowed at the place where a declarative_item or a statement is allowed.

5/2

The form of a pragma Assertion_Policy is as follows:

6/2

pragma Assertion_Policy(policy_identifier);

7/2

A pragma Assertion_Policy is a configuration pragma.

Name Resolution Rules

8/2

The expected type for the boolean_expression of a pragma Assert is any boolean type. The expected type for the string_expression of a pragma Assert is type String.

Legality Rules

9/2

The policy_identifier of a pragma Assertion_Policy shall be either Check, Ignore, or an implementation-defined identifier.

Static Semantics

10/2

A pragma Assertion_Policy is a configuration pragma that specifies the assertion policy in effect for the compilation units to which it applies. Different policies may apply to different compilation units within the same partition. The default assertion policy is implementation-defined.

11/2

The following language-defined library package exists:

12/2

package Ada.Assertions is
pragma Pure(Assertions);

13/2

Assertion_Error : exception;

14/2

procedure Assert(Check : in Boolean);
procedure Assert(Check : in Boolean; Message : in String);

15/2

end Ada.Assertions;

16/2

A compilation unit containing a pragma Assert has a semantic dependence on the Assertions library unit.

17/2

The assertion policy that applies to a generic unit also applies to all its instances.

Dynamic Semantics

18/2

An assertion policy specifies how a pragma Assert is interpreted by the implementation. If the assertion policy is Ignore at the point of a pragma Assert, the pragma is ignored. If the assertion policy is Check at the point of a pragma Assert, the elaboration of the pragma consists of evaluating the boolean expression, and if the result is False, evaluating the Message argument, if any, and raising the exception Assertions.Assertion_Error, with a message if the Message argument is provided.

19/2

Calling the procedure Assertions.Assert without a Message parameter is equivalent to:

20/2

if Check = False then
raise Ada.Assertions.Assertion_Error;
end if;

21/2

Calling the procedure Assertions.Assert with a Message parameter is equivalent to:

22/2

if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
end if;

23/2

The procedures Assertions.Assert have these effects independently of the assertion policy in effect.

Implementation Permissions

24/2

Assertion_Error may be declared by renaming an implementation-defined exception from another package.

25/2

Implementations may define their own assertion policies.

NOTES

26/2

2 Normally, the boolean expression in a pragma Assert should not call functions that have significant side-effects when the result of the expression is True, so that the particular assertion policy in effect will not affect normal operation of the program.