[Ada] Order of evaluation between precondition and 'Old

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the expansion of attribute 'Old to insert the generated
temporary that captures the value of the prefix before routine _Postconditions.
As a result, the precondition of a subprogram will be evaluated first, before
any postcondition-related code is executed.

------------
-- Source --
------------

--  evaluation_order.adb

procedure Evaluation_Order is
   subtype Idx is Integer range 1 .. 10;
   type Arr is array (Integer range <>) of Integer;

   procedure Swap (A : in out Arr; X, Y : Idx)
     with Pre  => X in A'Range and Y in A'Range,
          Post => A(X) = A(Y)'Old and A(Y) = A(X)'Old;

   procedure Swap (A : in out Arr; X, Y : Idx) is begin null; end Swap;

   A : Arr (1 .. 2) := (1 => 1, others => 0);

begin
   Swap (A, 1, 3);

end Evaluation_Order;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnata evaluation_order.adb
$ ./evaluation_order
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from
  evaluation_order.adb:6

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

2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference): Alphabetize
	variables. Rename variabme Tnn to Temp. Do not create a temporary
	if assertions are disabled. Find enclosing routine _Postconditions
	and insert the temporary that captures the value of the prefix
	before the routine.
	* exp_ch6.adb (Build_Postconditions_Procedure):
	Insert the generated _Postconditions routine
	before the first source declaration of the related
	subprogram.
	(Insert_After_Last_Declaration): Removed.
	(Insert_Before_First_Source_Declaration): New routine.

Attachment: difs
Description: Text document