[Ada] Composite postconditions

[Arnaud Charlet <charlet at adacore dot com>]

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.

Attachment: difs
Description: Text document