[Ada] Composite postconditions

[Arnaud Charlet]

This patch fixes the order in which the conjuncts in complex postconditions
are tested. Such postconditions are expanded into individual tests, chained
to internal lists when aspects are processed, and combined with other tests
when building the contract checking procedure for a given subprogram. The
construction of this procedure did not take into account the order in which
conjuncts were processed.

Executing the following:

   gnatmake -gnata postand.adb
   postand

must yield:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
                     failed postcondition from postand.adb:3
---
procedure Postand is
   procedure Test (X, Y : out Integer) with
     Post => X /= 0
       and then Y / X /= 0
       and then X + Y > 2;
   procedure Test (X, Y : out Integer) is
   begin
      X := 0;
      Y := 1;
   end Test;
   X, Y : Integer;
begin
   Test (X, Y);
end Postand;

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-02-06  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch6.adb (Expand_Subprogram_Contract, Append_Enabled_Item):
	Take into account the Split_PPC flag to ensure that conjuncts
	in a composite postcondition aspect are tested in source order.

-------------- next part --------------
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 207533)
+++ exp_ch6.adb	(working copy)
@@ -8887,7 +8887,18 @@
                List := New_List;
             end if;
 
-            Append (Item, List);
+            --  If the pragma is a conjunct in a composite postcondition, it
+            --  has been processed in reverse order. In the postcondition body
+            --  if must appear before the others.
+
+            if Nkind (Item) = N_Pragma
+              and then From_Aspect_Specification (Item)
+              and then Split_PPC (Item)
+            then
+               Prepend (Item, List);
+            else
+               Append (Item, List);
+            end if;
          end if;
       end Append_Enabled_Item;