11.4.2 Pragmas Assert and Assertion_Policy
1/2
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.
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.
Sponsored by Ada-Europe