Version 1.1 of ai12s/ai12-0401-1.txt

Unformatted version of ai12s/ai12-0401-1.txt version 1.1
Other versions for file ai12s/ai12-0401-1.txt

!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
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".
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.)
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.
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.
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.
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).
No ASIS effect.
!ACATS test
An ACATS B-Test is needed to check that the illegal cases are detected.

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


Questions? Ask the ACAA Technical Agent