===================================================================
@@ -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;
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.