11.4.2 Pragmas Assert and Assertion_Policy
1/2
{
AI95-00286-01}
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
3/2
4/2
5/2
6/2
7/2
A
pragma Assertion_Policy
is a configuration pragma.
Name Resolution Rules
8/2
8.a/2
Reason: We allow
any boolean type to be like if_statements
and other conditionals; we only allow String for the message in order
to match raise_statements.
Legality Rules
9/2
9.a/2
Implementation defined:
Implementation-defined policy_identifiers
allowed in a pragma
Assertion_Policy.
Static Semantics
10/2
{
AI95-00286-01}
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.
10.a/2
Implementation defined:
The default assertion policy.
11/2
{
AI95-00286-01}
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
{
AI95-00286-01}
A compilation unit containing a pragma
Assert has a semantic dependence on the Assertions library unit.
17/2
{
AI95-00286-01}
The assertion policy that applies to a generic
unit also applies to all its instances.
Dynamic Semantics
18/2
{
AI95-00286-01}
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
{
AI95-00286-01}
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
{
AI95-00286-01}
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
{
AI95-00286-01}
The procedures Assertions.Assert have these effects
independently of the assertion policy in effect.
Implementation Permissions
24/2
{
AI95-00286-01}
Assertion_Error may be declared by renaming an
implementation-defined exception from another package.
24.a/2
Reason: This permission
is intended to allow implementations which had an implementation-defined
Assert pragma to continue to use their originally defined exception.
Without this permission, such an implementation would be incorrect, as
Exception_Name would return the wrong name.
25/2
{
AI95-00286-01}
Implementations may define their own assertion
policies.
26/2
2 {
AI95-00286-01}
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.
Extensions to Ada 95
26.a/2
{
AI95-00286-01}
Pragmas Assert and Assertion_Policy,
and package Assertions are new.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe