A postcondition whose expression is a short-circuit is broken down into
individual aspects in order to provide better exception reporting. This
transformation is performed syntactically, before any analysis. The original
short-circuit expression is rewritten as its second operand, and an occurrence
of 'Old in that operand is potentially unevaluated, even though the parent
node does not come from source.
Compiling the following:
gcc -c -gnatct test06.adb
gcc -c test06.adb
must yield:
test06.adb:4:34: prefix of attribute "old" that is potentially unevaluated
must denote an entity
test06.adb:4:34: prefix of attribute "old" that is potentially unevaluated
must denote an entity
---
procedure test06 is
Tab : constant array (1 .. 10) of Integer := (others => 0);
procedure Bar (I : in out Natural)
with Post => I > 0 and then Tab(I)'Old = 1; -- Illegal
procedure Bar (I : in out Natural) is
begin
null;
end Bar;
J : Natural := 0;
begin
Bar (J);
end test06;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-08-04 Ed Schonberg <schonb...@adacore.com>
* sem_util.adb (Is_Potentially_Unevaluated): If the original
node of a parent node in the tree is a short-circuit operation,
the node is potentially unevaluated.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 213537)
+++ sem_util.adb (working copy)
@@ -11146,6 +11146,17 @@
begin
Expr := N;
Par := Parent (N);
+
+ -- A postcondition whose expression is a short-circuit is broken down
+ -- into individual aspects for better exception reporting. The original
+ -- short-circuit expression is rewritten as the second operand, and an
+ -- occurrence of 'Old in that operand is potentially unevaluated.
+ -- See Sem_ch13.adb for details of this transformation.
+
+ if Nkind (Original_Node (Par)) = N_And_Then then
+ return True;
+ end if;
+
while not Nkind_In (Par, N_If_Expression,
N_Case_Expression,
N_And_Then,
