Version 1.2 of ai12s/ai12-0401-1.txt
!standard 3.3(23.2/3) 20-10-21 AI12-0401-1/02
!standard 8.5.1(4.7/5)
!class binding interpretation 20-10-15
!status Amendment 1-2012 20-10-21
!status ARG Approved 13-0-1 20-10-21
!status work item 20-10-15
!status received 20-10-15
!priority Low
!difficulty Easy
!qualifier Omission
!subject Renaming of a qualified expression of a 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
Consider 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.7/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 longer 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.
Both of these changes are incompatable with Ada 2012 as defined, but are
necessary to meet the design goal that a legal renaming cannot be of something
that can be changed in a way that can cause erroneous execution.
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).
!corrigendum 3.3(23.2/3)
Replace the paragraph:
- its nominal subtype is constrained, and is not an untagged partial view; or
by:
- its nominal subtype is constrained and not an untagged partial view, and
it is neither a value conversion nor a qualified_expression; or
!corrigendum 8.5.1(4.6/2)
Insert after the paragraph:
- otherwise, the subtype of the object_name shall exclude null.
In addition to the places where Legality Rules normally apply (see 12.3), this
rule applies also in the private part of an instance of a generic unit.
the new paragraph:
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 (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.
!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.
****************************************************************
Questions? Ask the ACAA Technical Agent