CVS difference for ai12s/ai12-0280-2.txt

Differences between 1.6 and version 1.7
Log of other versions for file ai12s/ai12-0280-2.txt

--- ai12s/ai12-0280-2.txt	2019/07/26 05:51:09	1.6
+++ ai12s/ai12-0280-2.txt	2019/09/08 07:59:03	1.7
@@ -9,6 +9,7 @@
 !standard 6.1.1(27/5)
 !standard 6.1.1(39/5)
 !class Amendment 18-05-15
+!status Amendment 1-2012 19-09-07
 !status work item 18-05-15
 !status received 18-05-14
 !priority Low
@@ -267,6 +268,122 @@
 as a side-effect, requires less evaluation of 'Old prefixes that are never
 going to be used).
 
+
+
+!corrigendum 6.1.1(20/3)
+
+@drepl
+An @fa<expression> is @i<potentially unevaluated> if it occurs within:
+@dby
+A subexpression of a postcondition expression is @i<known on entry> if it is any
+of:
+
+!corrigendum 6.1.1(21/3)
+
+@drepl
+@xbullet<any part of an @fa<if_expression> other than the first @fa<condition>;>
+@dby
+@xbullet<a static subexpression (see 4.9);>
+
+!corrigendum 6.1.1(22/3)
+
+@drepl
+@xbullet<a @i<dependent_>@fa<expression> of a @fa<case_expression>;>
+@dby
+@xbullet<a literal whose type does not have any Integer_Literal, Real_Literal, or
+  String_Literal aspect specified, or the function specified by such an
+  attribute has aspect Global specified to be @b<null>;>
+
+!corrigendum 6.1.1(22.1/4)
+
+@drepl
+@xbullet<the @fa<predicate> of a @fa<quantified_expression>;>
+@dby
+** See the conflict file **
+
+!corrigendum 6.1.1(23/3)
+
+@drepl
+@xbullet<the right operand of a short-circuit control form; or>
+@dby
+@xbullet<For a short-circuit control form that is not repeatedly evaluated,
+      a subexpression of the right-hand operand is conditionally
+      evaluated, and its determining expressions include the left-hand
+      operand of the short-circuit control form;>
+
+!corrigendum 6.1.1(24/3)
+
+@drepl
+@xbullet<a @fa<membership_choice> other than the first of a membership
+operation.>
+@dby
+@xbullet<For a membership test that is not repeatedly evaluated, a
+   subexpression of a @fa<membership_choice> other than the first is
+   conditionally evaluated, and its determining expressions include the
+   @i<tested_>@fa<simple_expression> and the preceding 
+   @fa<membership_choice>s of the
+   membership test.>
+
+A conditionally evaluated subexpression is @i<determined to be
+unevaluated> at run time if its set of determining expressions are all
+known on entry, and when evaluated on entry their values are such that
+the given subexpression is not evaluated.
+
+!corrigendum 6.1.1(26/4)
+
+@drepl
+@xhang<@xterm<X'Old>
+Each X'Old in a postcondition expression that is enabled denotes
+a constant that is implicitly declared at the beginning of the
+subprogram body, entry body, or accept statement.>
+@dby
+@xhang<@xterm<X'Old>
+Each X'Old in a postcondition expression that is enabled, other than those 
+that occur in subexpressions that are determined to be unevaluated, denotes
+a constant that is implicitly declared at the beginning of the
+subprogram body, entry body, or accept statement.>
+
+
+!corrigendum 6.1.1(27/5)
+
+@drepl
+@xindent<Reference to this attribute is only allowed within a postcondition
+   expression. The @fa<prefix> of an Old @fa<attribute_reference> shall not
+   contain a Result @fa<attribute_reference>, nor an Old
+   @fa<attribute_reference>, nor a use of an entity declared within the
+   postcondition expression but not within @fa<prefix> itself (for example,
+   the loop parameter of an enclosing @fa<quantified_expression>). The @fa<prefix>
+   of an Old @fa<attribute_reference> that is potentially unevaluated shall
+   statically denote an entity.>
+@dby
+@xindent<Reference to this attribute is only allowed within a postcondition
+   expression. The @fa<prefix> of an Old @fa<attribute_reference> shall not
+   contain a Result @fa<attribute_reference>, nor an Old
+   @fa<attribute_reference>, nor a use of an entity declared within the
+   postcondition expression but not within @fa<prefix> itself (for example,
+   the loop parameter of an enclosing @fa<quantified_expression>). The @fa<prefix>
+   of an Old @fa<attribute_reference> shall
+   statically name an entity, unless the attribute_reference is
+   unconditionally evaluated, or is conditionally evaluated where all of
+   the determining expressions are known on entry.>
+
+
+!corrigendum 6.1.1(39/5)
+
+@dinsa
+For a call via an access-to-subprogram value, all precondition and
+postcondition checks performed are determined by the subprogram or entry
+denoted by the prefix of the Access attribute reference that produced the
+value.
+@dinst
+@s8<@i<Implementation Permissions>>
+
+An implementation may evaluate known-on-entry subexpression of a
+postcondition expression of an entity at the place where X'Old
+constants are created for the entity, with the normal evaluation of
+the postcondition expression, or both.
+
+
 !ASIS
 
 No ASIS effect.
@@ -378,5 +495,15 @@
 Sent: Thursday, July 25, 2019  1:19 PM
 
 Good point.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 26, 2019 12:53 AM
+
+Despite Tucker having replaced more than 50% of the AI when he changed the
+terminology (he volunteered to do that when Steve was out of commission) -
+somehow that paragraph was unchanged. So I applied this fix (along with a number
+of other fixes to Tucker's work).
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent