===================================================================
@@ -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,
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 <schonberg@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.