!standard 3.3(23.2/3)                                    20-10-15  AI12-0401-1/01
!standard 8.5.1(4/5)
!class binding interpretation 20-10-15
!status work item 20-10-15
!status received 20-10-15
!priority Low
!difficulty Easy
!qualifier Omission
!subject Renaming of qualified expression of variable
!summary

We restrict renaming of a qualified expression to cases where the operand is a
constant, or the target subtype statically matches the nominal subtype of the 
operand, or is unconstrained with no predicates.

We correct "known to be constrained" so that the nominal subtype of a
qualified expression does not necessarily make a prefix "known to be
constrained" even then the operand would not be "known to be constrained".

!question

In the following situation:
   X : T := ...;
   Y : S renames S'(X);
   
if X is a variable and its nominal subtype is not the same as S, and in
particular has a subtype that includes values that do not all satisfy S,
then a later update to X to give it a value that is not within the subtype S
could create a bizarre situation where Y no longer satisfies its nominal
subtype S. Should this be detected? (Yes.)

!recommendation

Disallow renaming of a qualified expression if the operand denotes a
variable with a nominal subtype that does not statically match the
target subtype of the qualified expression, unless the target subtype
imposes no  constraints or predicates.

!wording

Modify 3.3(23.2/3)
  [to ensure known-to-be-constrained is not influenced by the nominal
   subtype of the qualified_expression]

  * its nominal subtype is constrained[,] and [is] not an untagged
    partial view{, and it is neither a value conversion nor a
    qualified_expression}; or

Add after 8.5.1(4/5):
  
  In the case where the /object_/name is a qualified expression whose
  expression is a name that denotes a variable, the nominal subtype of
  the [Redundant:(constant)] view denoted by the qualified_expression
  shall statically match the nominal subtype of that variable, or
  statically match either the base subtype of its type if scalar, or the
  first subtype of its type otherwise.

!discussion

This is analogous to the rule in 8.5.1(5/3) that disallows renaming of a
discriminant-dependent component unless the enclosing object is known to
be constrained.

This issue arose when looking at what sort of compile-time checks the SPARK
tools would have to perform in a renaming of a qualified expression.  It
became clear that there was an erroneous situation lurking here, if we
allow a renaming of a constant view of a variable that could later be
altered to no satisfy the nominal subtype of the qualified expression.

We modify the rule in 3.3(23.2/3) so that known-to-be-constrained is
determined by the operand of a conversion or a qualified_expression
(as specified in 3.3(23.8.5)), rather than by the nominal subtype. This
change will make some 'Access prefixes and renamings illegal when the
qualified (or converted) object is not itself "known to be constrained".
That was always intended, but not captured by the rules.

Note that we don't need to worry about generic formal in-out objects,
even though they are effectively renames of the generic actual object,
because a qualified_expression is a constant view, so would not be
permitted as the actual for a generic formal in-out object.

!example

In the situation mentioned in the !problem:

   X : T := ...;
   Y : S renames S'(X);
   
The renaming will be illegal unless S statically matches T, T'Base (if
scalar), or the first subtype of T (if nonscalar).

!ASIS

No ASIS effect.

!ACATS test

An ACATS B-Test is needed to check that the illegal cases are detected.

!appendix

Editor's note: I changed the version provided by Tucker to a Binding
Interpretation, since this is plugging holes caused by the introduction
of qualified expressions as names in Ada 2012. It seems to me that it
should apply to Ada 2012 as well, even if that is (very) marginally
incompatible.

****************************************************************