AI22-0157-1

!standard 6.1.1(20/5)                                26-05-12  AI22-0157-1/09

!standard 6.1.1(22.1/5)

!standard 6.1.1(22.3/5)

!standard 6.1.1(22.4/5)

!class Binding Interpretation 26-02-10

!status Revision-202Y  26-02-20

!status ARG Approved  10-0-0  26-05-12

!status work item 26-04-30

!status ARG Approved  8-0-0  26-02-17

!status work item 26-02-10

!status received 26-02-10

!assigned author Tucker Taft

!submitter Tucker Taft

!priority Medium

!difficulty Easy

!qualifier Omission

!subject Fix holes in definition of "known on entry"

!summary

We fix an omission where short-circuit control forms, membership tests, and certain attribute references were not properly handled within the definition for known-on-entry.

We also address a restriction needed on a reference to a full constant declaration, to disallow referring to a constant local to an enclosing declare expression.

[Editor’s note: This AI is included in the draft 6 RM, even though it is not yet approved, as it was already included before problems were found and it was reopened. Removing it and then readding it on the next cycle would be wasteful with our limited resources.]

!issue

The definition of known on entry in the Ada RM 6.1.1(20/5-22.10/5) makes no mention of short-circuit control forms or membership tests. That seems unintended, since a function call to a pure function is permitted so long as all of the operands are known on entry, and there is nothing preventing such a function containing a short-circuit control form or a membership test.

RM 6.1.1(22.4/5) includes within the definition of known on entry:

an invocation of a predefined operator where all of the operands are known on entry;

Perhaps that should be generalized to include short-circuit control forms and membership tests.

In addition, RM 6.1.1(22.1/5) allows a reference to a full constant declaration, but that should probably not be permitted if the constant is declared within an enclosing declare expression, such as:

procedure Foo is
   function Id (X : Integer) return Integer is (X);
   procedure P (X : in out Integer)
     with Post =>
           (declare Y : constant Integer := ... whatever ...;
             begin
                  (if Y <= 2 then Id (X)'Old >= X));
   procedure P (X : in out Integer) is null;
begin
   null;
end Foo;

!recommendation

We recommend including short-circuit control forms, membership tests, and certain attribute references within the constructs that can be known on entry. We also require any referenced full constant to be declared outside the postcondition expression itself.

!wording

Modify 6.1.1(20/5):

A subexpression of a postcondition expression{, or a name (including a subtype_mark) within such an expression,} is known on entry if it is any of:{

Modify 6.1.1(22.1/5):

Modify 6.1.1(22.3/5):

AARM Reason: Most array objects in Ada have their bounds determined when they are initialized (including all parameters, even in out parameters, in Ada 2022 and earlier), so they cannot be changed by a subprogram and thus are safe to be known on entry. The few objects that can have their bounds changed are not allowed to be renamed, thus we use that existing description to exclude those.

AARM Ramification: Attribute references that are static expressions are also known on entry by the earlier rule.

Modify 6.1.1(22.4/5):

!discussion

It seems to have been a simple oversight that short-circuit control forms and membership tests were not included among the possibilities for known-on-entry constructs. Short-circuit control forms impose no complexity beyond the two operands. Membership tests, however, can have a list of membership_choices, and these can be simple expressions, ranges, or subtype_marks.  Subtype_marks impose no problem, in general, because they are naturally constant, and if appearing on a postcondition, must come from the enclosing scope. But Dynamic_Predicates could introduce global references to variable state, which would not be good. Additionally, subtype_marks denoting a generic formal type might have an actual that contains such a Dynamic_Predicate. Expressions are not a special case, so it is ultimately only ranges and subtype_marks that require some additional wording.

The added restriction for references to full constants was similarly an unintended omission, related to the corner case of an enclosing declare expression. We could have tried to craft a rule allowing such nested constant declarations if they in fact denote an expression that is itself known on entry. But the extra capability that implies seemed minor at best, so we went with the simpler rule.

We have also included attribute references when the prefix is known on entry, or when the prefix is a renamable array and the attribute is First, Last, or Length.  We have included subtype marks in the list of constructs that can be known on entry, because they are used in both (range) attribute references, and in membership tests.

!example

Here we have a use of 'Old that appears in two places, the second of which is conditionally evaluated, and is only legal when the "if" condition (its determining expression) is known on entry.  See 6.1.1(20/5-24.1/5) for the vocabulary used here, and 6.1.1(27/5) for the actual legality rule.

procedure Check
  (X : in out Integer; L : Positive; A : in out String; Y : Positive)
   with Post =>
     (if X'Old in 1 .. L and then Y in A'Range
      then X >= Character'Pos (A(Y)'Old));

!corrigendum 6.1.1(20/5)

@drepl

A subexpression of a postcondition expression is @i{known on entry} if it is any of:

@dby

A subexpression of a postcondition expression, or a @fa{name} (including a @fa{subtype_mark}) within such an expression, is @i{known on entry} if it is any of:

@xbullet{a @fa{subtype_mark} that denotes a subtype that is not a subtype of a private type, a formal type, or an incomplete view, and not a subtype to which a Dynamic_Predicate applies;}

!corrigendum 6.1.1(22.1/5)

@drepl

@xbullet{a name statically denoting a full constant declaration which is known to have no variable views (see @ref{3.3});}

@dby

@xbullet{a name statically denoting a full constant declaration that occurs outside the postcondition expression itself, and which is known to have no variable views (see @ref{3.3});}

!corrigendum 6.1.1(22.3/5)

@drepl

@xbullet{an Old @fa{attribute_reference};}

@dby

@xbullet{an @fa{attribute_reference} (or @fa{range_attribute_reference}) whose @fa{prefix} is known on entry, or where the @fa{(range_)}@fa{attribute_designator} is:}

@xinbull{Old;}

@xinbull{Constrained;}

@xinbull{First, Last, Length, or Range (optionally followed by a parenthesized expression), and the @fa{prefix} denotes an array object for which renaming is allowed (see @ref{8.5.1});}

!corrigendum 6.1.1(22.4/5)

@drepl

@xbullet{an invocation of a predefined operator where all of the operands are known on entry;}

@dby

@xbullet{an invocation of a predefined operator or short-circuit control form where all of the operands are known on entry;}

@xbullet{a membership test where the tested expression is known on entry, any @i{choice_}@fa{simple_expression} is known on entry, every @fa{name} or @fa{expression} appearing within any @fa{range} is known on entry, and any @fa{subtype_mark} is known on entry;}

!ACATS test

A B-Test is needed to verify that short-circuit control forms and membership tests are considered known on entry if and only if their constituents are all known on entry.

A B-test is also needed to check that a reference to a constant from an enclosing declare expression is not considered known on entry.

!appendix

This addresses ARG GitHub issue #161 and ARG GitHub issue #151.

 

From: Randy Brukardt

Sent: Thursday, April 30, 2026  10:27 PM

Brad Moore has noted that the use of Old on A(Y) in the example did not make any sense, as both A and Y were in parameters, so neither should change during the execution of procedure Check. Changing the A parameter to be an in out parameter seemed like the best fix, as in that case the bounds of A would be unchanged by the call.

However, that shows another problem: the expression “Y in A’range” is not known on entry -- regardless of whether A is an in or in out parameter. It’s not completely clear for A’range, but replacing it with the supposedly equivalent “A’First .. A’Last” shows the problem: the prefix A is none of the things that are known on entry. We could fix that by introducing an extra ‘Old (done above). But that doesn’t help, as no attribute references are treated as known-on-entry.

This example seems too reasonable to ignore. Any postcondition involving an array is likely to test the bounds of the array somewhere.

It seems like we need to add at least ‘First and ‘Last to the definition of known-on-entry, as they are very likely to be used in such circumstances. Perhaps it would be best to add them with specific prefixes (object prefixes that are known-on-entry, or designate a parameter (of any mode), as the bounds of parameters cannot be changed, even for unconstrained arrays, or are of a constrained array type, or prefixes that are a constrained array subtype or a discrete subtype).

As the deadline for fixes to this AI has passed, I’ve reopened it to consider this question.