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.
is a configuration pragma.
Name Resolution Rules
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.
allowed in 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.
The default assertion policy.
The following language-defined library package
package Ada.Assertions is
Assertion_Error : exception;
procedure Assert(Check : in Boolean);
procedure Assert(Check : in Boolean; Message : in String);
A compilation unit containing a pragma
Assert has a semantic dependence on the Assertions library unit.
The assertion policy that applies to a generic
unit also applies to all its instances.
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.
Calling the procedure Assertions.Assert without
a Message parameter is equivalent to:
if Check = False then
Calling the procedure Assertions.Assert with a
Message parameter is equivalent to:
if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
The procedures Assertions.Assert have these effects
independently of the assertion policy in effect.
Assertion_Error may be declared by renaming an
implementation-defined exception from another package.
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.
Implementations may define their own assertion
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
Pragmas Assert and Assertion_Policy,
and package Assertions are new.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe