[Ada] Enfore SPARK RM rule 7.1.5(2)

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the analysis of aspects Abstract_State, Initializes and
Initial_Condition to ensure that they are inserted after pragma SPARK_Mode.
The proper placement allows for SPARK_Mode to be analyzed first and dictate
the mode of the related package.

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

--  initializes_illegal_2.ads

package Initializes_Illegal_2
  with SPARK_Mode,
       Initializes    => (S, X),
       Abstract_State => S
is
   X : Integer;
end Initializes_Illegal_2;

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

$ gcc -c initializes_illegal_2.ads
initializes_illegal_2.ads:4:08: aspect "Abstract_State" cannot come after
  aspect "Initializes"

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

2014-07-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch13.adb (Insert_After_SPARK_Mode): Moved to
	the outer level of routine Analyze_Aspect_Specifications. Ensure
	that the corresponding pragmas of aspects Initial_Condition and
	Initializes are inserted after pragma SPARK_Mode.

Attachment: difs
Description: Text document