RM 6.1.1 (26/3) specifies that if the prefix of 'Old wihin a postcondition is
potentially unevaluated, as in the right-hand side of a short-circuit operation
then the prefix can only be an entity name.
Compiling main.adb must yield:
p.ads:5:44: prefix that is potentially unevaluated must denote an entity
---
with P; use P;
procedure Main is
A : My_Array := (1, 2, 3);
V : Integer;
begin
Extract (A, 6, V);
end Main;
---
package P is
type My_Array is array (Natural range <>) of Integer;
procedure Extract (A : in out My_Array; J : Integer; V : out Integer) with
Post => (if J in A'Range then V = A(J)'Old and A(J) = 0); -- INCORRECT
procedure Check (A : in out My_Array; J : Integer; V : out Integer) with
Post => (if A(A'First)'Old > A(A'Last)'Old then True
else raise program_error); -- OK
end P;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-23 Ed Schonberg <schonb...@adacore.com>
* sem_util.ads, sem_util.adb (Is_Potentially_Unevaluated): new
predicate to implement rule given in 6.1.1 (20/3).
* sem_attr.adb (Analyze_Attribute, case 'Old): Reject prefix of
'Old in a postcondition, if it is potentially unevaluated and
it is not an entity name.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 206980)
+++ sem_util.adb (working copy)
@@ -10249,6 +10249,48 @@
end if;
end Is_Partially_Initialized_Type;
+ --------------------------------
+ -- Is_Potentially_Unevaluated --
+ --------------------------------
+
+ function Is_Potentially_Unevaluated (N : Node_Id) return Boolean is
+ Par : Node_Id;
+ Expr : Node_Id;
+
+ begin
+ Expr := N;
+ Par := Parent (N);
+ while not Nkind_In (Par, N_If_Expression,
+ N_Case_Expression,
+ N_And_Then,
+ N_Or_Else,
+ N_In,
+ N_Not_In)
+ loop
+ Expr := Par;
+ Par := Parent (Par);
+ if Nkind (Par) not in N_Subexpr then
+ return False;
+ end if;
+ end loop;
+
+ if Nkind (Par) = N_If_Expression then
+ return Is_Elsif (Par) or else Expr /= First (Expressions (Par));
+
+ elsif Nkind (Par) = N_Case_Expression then
+ return Expr /= Expression (Par);
+
+ elsif Nkind_In (Par, N_And_Then, N_Or_Else) then
+ return Expr = Right_Opnd (Par);
+
+ elsif Nkind_In (Par, N_In, N_Not_In) then
+ return Expr /= Left_Opnd (Par);
+
+ else
+ return False;
+ end if;
+ end Is_Potentially_Unevaluated;
+
------------------------------------
-- Is_Potentially_Persistent_Type --
------------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 206918)
+++ sem_util.ads (working copy)
@@ -1116,6 +1116,9 @@
-- if Include_Implicit is False, these cases do not count as making the
-- type be partially initialized.
+ function Is_Potentially_Unevaluated (N : Node_Id) return Boolean;
+ -- Predicate to implement definition given in RM 6.1.1 (20/3)
+
function Is_Potentially_Persistent_Type (T : Entity_Id) return Boolean;
-- Determines if type T is a potentially persistent type. A potentially
-- persistent type is defined (recursively) as a scalar type, a non-tagged
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 206918)
+++ sem_attr.adb (working copy)
@@ -4337,6 +4337,8 @@
-- During pre-analysis, Prag is the enclosing pragma node if any
begin
+ Prag := Empty;
+
-- Find enclosing scopes, excluding loops
CS := Current_Scope;
@@ -4515,6 +4517,18 @@
("??attribute Old applied to constant has no effect", P);
end if;
+ -- Check that the prefix of 'Old is an entity, when it appears in
+ -- a postcondition and may be potentially unevaluated (6.1.1 (27/3)).
+
+ if Present (Prag)
+ and then Get_Pragma_Id (Prag) = Pragma_Postcondition
+ and then Is_Potentially_Unevaluated (N)
+ and then not Is_Entity_Name (P)
+ then
+ Error_Msg_N ("prefix that is potentially unevaluated must "
+ & "denote an entity", N);
+ end if;
+
-- The attribute appears within a pre/postcondition, but refers to
-- an entity in the enclosing subprogram. If it is a component of
-- a formal its expansion might generate actual subtypes that may
