Syntax:
pragma Assertion_Policy (CHECK | DISABLE | IGNORE | SUPPRESSIBLE); pragma Assertion_Policy ( ASSERTION_KIND => POLICY_IDENTIFIER {, ASSERTION_KIND => POLICY_IDENTIFIER}); ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND RM_ASSERTION_KIND ::= Assert | Static_Predicate | Dynamic_Predicate | Pre | Pre'Class | Post | Post'Class | Type_Invariant | Type_Invariant'Class | Default_Initial_Condition ID_ASSERTION_KIND ::= Assertions | Assert_And_Cut | Assume | Contract_Cases | Debug | Ghost | Initial_Condition | Invariant | Invariant'Class | Loop_Invariant | Loop_Variant | Postcondition | Precondition | Predicate | Refined_Post | Statement_Assertions | Subprogram_Variant POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible
This is a standard Ada 2012 pragma that is available as an
implementation-defined pragma in earlier versions of Ada.
The assertion kinds RM_ASSERTION_KIND
are those defined in
the Ada standard. The assertion kinds ID_ASSERTION_KIND
are implementation defined additions recognized by the GNAT compiler.
The pragma applies in both cases to pragmas and aspects with matching
names, e.g. Pre
applies to the Pre aspect, and Precondition
applies to both the Precondition
pragma
and the aspect Precondition
. Note that the identifiers for
pragmas Pre_Class and Post_Class are Pre’Class and Post’Class (not
Pre_Class and Post_Class), since these pragmas are intended to be
identical to the corresponding aspects.
If the policy is CHECK
, then assertions are enabled, i.e.
the corresponding pragma or aspect is activated.
If the policy is IGNORE
, then assertions are ignored, i.e.
the corresponding pragma or aspect is deactivated.
This pragma overrides the effect of the ‘-gnata’ switch on the
command line.
If the policy is SUPPRESSIBLE
, then assertions are enabled by default,
however, if the ‘-gnatp’ switch is specified all assertions are ignored.
The implementation defined policy DISABLE
is like
IGNORE
except that it completely disables semantic
checking of the corresponding pragma or aspect. This is
useful when the pragma or aspect argument references subprograms
in a with’ed package which is replaced by a dummy package
for the final build.
The implementation defined assertion kind Assertions
applies to all
assertion kinds. The form with no assertion kind given implies this
choice, so it applies to all assertion kinds (RM defined, and
implementation defined).
The implementation defined assertion kind Statement_Assertions
applies to Assert
, Assert_And_Cut
,
Assume
, Loop_Invariant
, and Loop_Variant
.