!standard 13.12.1(6/2) 11-11-11 AI05-0273-1/00 !standard 13.12.1(7/2) !standard 2.8(10) !standard H.4(24) !class Amendment 11-11-11 !status work item 11-11-11 !status received 11-11-04 !priority Low !difficulty Easy !subject Problems with the Old attribute !summary !problem The prefix of the 'Old attribute used in a postcondition is unconditionally evaluated when the subprogram is entered. This causes a number of problems: (1) If the prefix uses something that doesn't exist when the subprogram is entered, there is a problem: procedure Proc (X : in out String) with Post => (for all I in X'Range => X(I) /= X(I)'Old); function Foo return String with Post => Foo'Result /= Foo'Result'Old; (2) If evaluating the prefix would raise an exception, there could be a problem: Table : array (1..10) of Integer := ... procedure Bar (I : in out Natural) with Post => I > 0 and then Tab(I)'Old = 1; If I = 0 on entry, the evaluation of Tab(0) will raise Constraint_Error. The "and then" provides no protection because there is no way for the compiler to tell what I is on exit from the subprogram, so it is not known whether the value Tab(I)'Old will be needed when Bar exits. So Tab(I) has to be unconditionally evaluated on entry. The language actually requires Tab(I) to be evaluated unconditionally even if the compiler can figure out that it is never needed. That makes the problem worse. !proposal ** TBD. !wording ** TBD. !discussion In the second example, the programmer probably meant procedure Bar (I : in out Natural) with Post => I > 0 and then Tab'Old(I) = 1; which will not raise Constraint_Error (but does require copying the entire Tab array). !example !ACATS Test !ASIS !appendix From: Steve Baird Sent: Friday, November 4, 2011 3:21 PM Are we missing some legality checks with respect to the allowable prefix of an Old attribute? I think both of the following attribute uses should be illegal: package Pkg is procedure Proc (X : in out String) with Post => (for all I in X'Range => X(I) /= X(I)'Old); function Foo return String with Post => Foo'Result /= Foo'Result'Old; end Pkg; Do others agree that a) they should be illegal and b) these cases are not covered by current RM wording and c) this is a very low-priority issue ? **************************************************************** From: Robert Dewar Sent: Friday, November 4, 2011 3:38 PM Right, GNAT detects both as erors, for the second it gives: 1. package Pkg is 2. -- procedure Proc (X : in out String) with 3. -- Post => (for all I in X'Range => X(I) /= X(I)'Old); 4. 5. function Foo return String with 6. Post => Foo'Result /= Foo'Result'Old; | >>> warning: attribute Old applied to constant has no effect 7. end Pkg; **************************************************************** From: Jean-Pierre Rosen Sent: Friday, November 4, 2011 5:07 PM > I think both of the following attribute uses should be illegal: > > package Pkg is > procedure Proc (X : in out String) with > Post => (for all I in X'Range => X(I) /= X(I)'Old); But I hope that X'Old(I) (which is the same thing) is legal... **************************************************************** From: Steve Baird Sent: Friday, November 4, 2011 5:11 PM Yes it is legal, but no it isn't the same thing. **************************************************************** From: Robert Dewar Sent: Friday, November 4, 2011 11:10 PM And of course X'Old (I) works fine in GNAT, though it takes a copy of the whole of X which is a bit wasteful. **************************************************************** From: Jean-Pierre Rosen Sent: Saturday, November 5, 2011 1:03 AM What did I miss? Since I is dynamic, X(I)'Old could be implemented only by saving the whole of X, isn't it? **************************************************************** From: Bob Duff Sent: Saturday, November 5, 2011 5:07 AM X(I)'Old is meaningless. It means "the value of X(I) on entry to this procedure", but that makes no sense, because I didn't exist at that point. X'Old(I) makes sense. **************************************************************** From: Steve Baird Sent: Friday, November 11, 2011 6:22 PM replace 6.1.1 (21/3-22/3) with: X'Old For each X'Old in a postcondition expression that is enabled, a constant is implicitly declared at the beginning of the subprogram or entry. The constant is of the type of X and is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. The value of X'Old in the postcondition expression is the value of this constant; the type of X'Old is the type of X. These implicit constant declarations occur in an arbitrary order, except that if one Old attribute use occurs as part of the prefix of another, then the constant declaration associated with the first use precedes that of the second. Use of this attribute is allowed only within a postcondition expression. The prefix of an Old attribute shall not contain either a Result attribute use or a use of a declaration declared within an enclosing expression but not within the given Old attribute prefix (e.g., the loop parameter of an enclosing quantified expression). **************************************************************** From: Edmond Schonberg Sent: Saturday, November 12, 2011 11:19 AM An expression is potentially unevaluated if it occurs within: o part of an if-expression other than the first condition o any dependent expression of a case expression o the right-hand side of a short-circuit operation o a membership choice other than the first in a membership operation The prefix of an attribute reference Old that is potentially unevaluated shall statically denote an entity. **************************************************************** From: Robert Dewar Sent: Saturday, November 12, 2011 6:11 PM I wonder if it is too restrictive to just say "the prefix of attribute reference Old must statically denote an entity". The special rules above seem horribly complex too me ****************************************************************