AI22-0094-1

!standard 10.2.1(9.1/5)                                    24-09-11  AI22-0094-1/06

!standard 11.4.2(28/5)

!standard 13.12(8.6/1)

!standard 13.12(9.1/1)

!class Binding Interpretation 24-02-12

!status Amendment 1-2022  24-07-18

!status WG9 Approved 24-10-10

!status ARG Approved  9-0-0  24-07-18

!status work item 23-12-14

!status received 23-12-14

!submitter Stephen Baird

!priority Low

!difficulty Easy

!qualifier Clarification

!subject  Assertion policy and preelaborability

!summary

Confirm that assertion policy has no effect on preelaborability.

!issue

In the discussion of AI22-0051-2, it was pointed out that adding or deleting an Assertion_Policy pragma should not change the preelaborability of any elaborable construct.

!recommendation

State explicitly (as is already done in a similar case for freezing rules) that Assertion_Policy  pragmas are ignored in determining preelaborability, and that instead, all relevant assertion policies are assumed to be Check.

In 11.4.2, state the general principle that a (legal) Assertion_Policy pragma should have no effect on the legality or the static semantics of any construct. One important exception to this general principle is the interaction between Assertion_Policy and Restrictions pragmas. Restrictions are not enforced in an assertion expression if the applicable assertion policy ensures that the assertion expression can never be evaluated.

A consequence of that general principle is that an Assertion_Policy pragma should not have an effect on the meaning of a restrictions pragma. That also is stated explicitly.

!wording

Add after 10.2.1(9.1/5):

In determining whether the elaboration of an elaborable construct performs some action, an assertion policy of Check is assumed to be in effect everywhere and for all assertion aspects.  [Redundant: Assertion_Policy pragmas are ignored in this determination.]

Add after 11.4.2(28/5)^[a]:

NOTE 2: In most cases, adding or deleting a legal Assertion_Policy pragma has no impact on the legality or the static semantics of any construct. In particular, the rules pertaining to freezing (see 13.14) and the definition of preelaborability (see 10.2.1) are unaffected by Assertion_Policy pragmas. However, this general principle does not always hold in the case of a Restrictions pragma (see 13.12).

Add after 13.12(8.6/1) (as the last bulleted list item):

• An assertion policy of Check is assumed to be in effect everywhere for the assertion aspects Static_Predicate and Dynamic_Predicate [Redundant: , but not for other assertion aspects.] Subject to this assumption, if the assertion policy in effect for the corresponding assertion aspect of an assertion expression is Ignore, then the expression is considered not to be used.

Modify 13.12(9.1/1):

An implementation is permitted to omit {enforcement of restrictions}[restriction checks] for code that is recognized at compile time to be unreachable and for which no code is generated {, subject to the aforementioned assumption that an Assertion_Policy of Check is in effect everywhere for the two subtype predicate assertion aspects}.

!discussion

The two subtype predicate assertion policies are treated differently than other assertion policies because of membership tests and Valid attribute references. See the “even when the applicable Assertion_Policy is Ignore,” part of RM 11.4.2(10).

It was decided that usability considerations require allowing restriction violations in other forms of disabled assertion expressions. Consider, for example, a cross-compiled application that is compiled in two modes: one for testing on the host and one for execution on the target.

If some restriction is only in effect for the target configuration, and if precondition checking, for example, is only enabled for the host configuration, then it would be useful to allow precondition assertion expressions which contain violations of the restriction.

!example

package Example is
   pragma Preelaborate;
   pragma Assertion_Policy (Ignore);
   X : Integer := 111;
   Y : Integer := 222;
   pragma Assert (X < Y); -- Illegal:
                          -- disabled assertion not preelaborable
end Example;

!corrigendum 10.2.1(9.1/5)

@dinsa

@xbullet{The elaboration of any elaborable construct that is not preelaborable.}

@dinst

In determining whether the elaboration of an elaborable construct performs some action, an assertion policy of Check is assumed to be in effect everywhere and for all assertion aspects. Assertion_Policy pragmas are ignored in this determination.

!corrigendum 11.4.2(28/5)

@dinsa

@xindent{@s9{NOTE @ Normally, the boolean expression in a @fa{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.}}

@dinst

@xindent{@s9{NOTE 2 @ In most cases, adding or deleting a legal Assertion_Policy pragma has no impact on the legality or the static semantics of any construct. In particular, the rules pertaining to freezing (see @ref{13.14}) and the definition of preelaborability (see @ref{10.2.1}) are unaffected by Assertion_Policy pragmas. However, this general principle does not always hold in the case of a Restrictions pragma (see @ref{13.12}).}}

!corrigendum 13.12(8.6/1)

@drepl

@xbullet{A @fa{default_expression} for a formal parameter or a generic formal object is considered to be used if and only if the corresponding actual parameter is not provided in a given call or instantiation.}

@dby

@xbullet{A @fa{default_expression} for a formal parameter or a generic formal object is considered to be used if and only if the corresponding actual parameter is not provided in a given call or instantiation;}

@xbullet{An assertion policy of Check is assumed to be in effect everywhere for the assertion aspects Static_Predicate and Dynamic_Predicate, but not for other assertion aspects. Subject to this assumption, if the assertion policy in effect for the corresponding assertion aspect of an assertion expression is Ignore, then the expression is considered not to be used.}

!corrigendum 13.12(9.1/1)

@drepl

An implementation is permitted to omit restriction checks for code that is recognized at compile time to be unreachable and for which no code is generated.

@dby

An implementation is permitted to omit enforcement of restrictions for code that is recognized at compile time to be unreachable and for which no code is generated, subject to the aforementioned assumption that an Assertion_Policy of Check is in effect everywhere for the two subtype predicate assertion aspects.

!ACATS test

A B-test similar to the example above would be appropriate; a B-Test of a restriction violation in an ignored pragma Assert is also needed.

!appendix

From: Randy Brukardt

Posted: Wednesday, September 11, 2024  7:45 PM

I moved the new bullet in 13.12 to the end of the list of bullets. Typically, one wants to list items in approximate order of likelihood, and surely an object declaration and use of default parameters are more likely than changing an Assertion_Policy pragma. This also avoids renumbering the existing bullets.

Additionally, the form of this bullet is inconsistent with the others. In the others something is “considered to be used”, while this one talks about “restriction checks” (a phrase that is used only once in the RM). I’ve reworded it to be consistent with the others.

Finally, the term “restriction checks” (used in 13.12(9.1/1)) is undefined (probably an informal meaning was intended), but incorporates part of a defined term (“checks”) which has a different meaning. Changing that phrase to “enforcement of restrictions” (the form used in 13.12(9.2/1)) avoids any confusion.

Consider this part of my (late) Editorial Review.

[a]Steve had this "in the Language Design Principles section". But that ends before this paragraph, and does not appear in the RM anyway. So either this should be an AARM note in a different place, or a user note given in the original place. I chose the latter.