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