[multiple changes]

2013-10-10  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi, a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads,
	a-cforse.ads, a-cofove.ads: Update comment and doc of formal containers

2013-10-10  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications): For Pre/Post
	conditions that apply to a subprogram body, preserve the placement
	and order of the generated pragmas, which must appear before
	other declarations in the body.

From-SVN: r203347

9 files changed, 102 insertions, 45 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b0b8654..7438dab 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,15 @@
+2013-10-10  Yannick Moy  <moy@adacore.com>
+
+	* gnat_rm.texi, a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads,
+	a-cforse.ads, a-cofove.ads: Update comment and doc of formal containers
+
+2013-10-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Analyze_Aspect_Specifications): For Pre/Post
+	conditions that apply to a subprogram body, preserve the placement
+	and order of the generated pragmas, which must appear before
+	other declarations in the body.
+
 2013-10-10  Bob Duff  <duff@adacore.com>
 
 	* gnat_ugn.texi: Add gnat2xml doc.
diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index bfa8ffb..0442fe6 100644
--- a/gcc/ada/a-cfdlli.ads
+++ b/gcc/ada/a-cfdlli.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists in the
---  Ada 2012 RM. The modifications are to facilitate formal proofs by making it
---  easier to express properties.
+--  Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+--  making it easier to express properties, and by making the specification of
+--  this unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -49,7 +51,7 @@
 --      function Left  (Container : List; Position : Cursor) return List;
 --      function Right (Container : List; Position : Cursor) return List;
 
---    See subprogram specifications that follow for details
+--    See subprogram specifications that follow for details.
 
 generic
    type Element_Type is private;
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index 93a47c5..2f1e7bb 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from package Ada.Containers.Bounded_Hashed_Maps in the
---  Ada 2012 RM. The modifications are to facilitate formal proofs by making it
---  easier to express properties.
+--  Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+--  making it easier to express properties, and by making the specification of
+--  this unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -49,7 +51,7 @@
 --      function Left  (Container : Map; Position : Cursor) return Map;
 --      function Right (Container : Map; Position : Cursor) return Map;
 
---    See detailed specifications for these subprograms
+--    See detailed specifications for these subprograms.
 
 private with Ada.Containers.Hash_Tables;
 
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index 22bfda9..147a332 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from package Ada.Containers.Bounded_Hashed_Sets in the
---  Ada 2012 RM. The modifications are to facilitate formal proofs by making it
---  easier to express properties.
+--  Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+--  making it easier to express properties, and by making the specification of
+--  this unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -49,7 +51,7 @@
 --      function Left  (Container : Set; Position : Cursor) return Set;
 --      function Right (Container : Set; Position : Cursor) return Set;
 
---    See detailed specifications for these subprograms
+--    See detailed specifications for these subprograms.
 
 private with Ada.Containers.Hash_Tables;
 
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 8e323e1..ca6db02 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from package Ada.Containers.Bounded_Ordered_Maps in
---  the Ada 2012 RM. The modifications are to facilitate formal proofs by
---  making it easier to express properties.
+--  the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+--  making it easier to express properties, and by making the specification of
+--  this unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -51,7 +53,7 @@
 --      function Left  (Container : Map; Position : Cursor) return Map;
 --      function Right (Container : Map; Position : Cursor) return Map;
 
---    See detailed specifications for these subprograms
+--    See detailed specifications for these subprograms.
 
 private with Ada.Containers.Red_Black_Trees;
 
diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 35e4613..7f93161 100644
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in
---  the Ada 2012 RM. The modifications are to facilitate formal proofs by
---  making it easier to express properties.
+--  the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+--  making it easier to express properties, and by making the specification of
+--  this unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -50,7 +52,7 @@
 --      function Left  (Container : Set; Position : Cursor) return Set;
 --      function Right (Container : Set; Position : Cursor) return Set;
 
---    See detailed specifications for these subprograms
+--    See detailed specifications for these subprograms.
 
 private with Ada.Containers.Red_Black_Trees;
 
diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index 9ca84da..58e7b8b 100644
--- a/gcc/ada/a-cofove.ads
+++ b/gcc/ada/a-cofove.ads
@@ -30,8 +30,10 @@
 ------------------------------------------------------------------------------
 
 --  This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
---  2012 RM. The modifications are to facilitate formal proofs by making it
---  easier to express properties.
+--  2012 RM. The modifications are meant to facilitate formal proofs by making
+--  it easier to express properties, and by making the specification of this
+--  unit compatible with SPARK 2014. Note that the API of this unit may be
+--  subject to incompatible changes as SPARK 2014 evolves.
 
 --  The modifications are:
 
@@ -48,12 +50,7 @@
 --      function Left  (Container : Vector; Position : Cursor) return Vector;
 --      function Right (Container : Vector; Position : Cursor) return Vector;
 
---      Left returns a container containing all elements preceding Position
---      (excluded) in Container. Right returns a container containing all
---      elements following Position (included) in Container. These two new
---      functions are useful to express invariant properties in loops which
---      iterate over containers. Left returns the part of the container already
---      scanned and Right the part not scanned yet.
+--    See detailed specifications for these subprograms.
 
 with Ada.Containers;
 use Ada.Containers;
@@ -350,9 +347,14 @@ package Ada.Containers.Formal_Vectors is
 
    function Left (Container : Vector; Position : Cursor) return Vector with
      Pre => Has_Element (Container, Position) or else Position = No_Element;
-
    function Right (Container : Vector; Position : Cursor) return Vector with
      Pre => Has_Element (Container, Position) or else Position = No_Element;
+   --  Left returns a container containing all elements preceding Position
+   --  (excluded) in Container. Right returns a container containing all
+   --  elements following Position (included) in Container. These two new
+   --  functions can be used to express invariant properties in loops which
+   --  iterate over containers. Left returns the part of the container already
+   --  scanned and Right the part not scanned yet.
 
 private
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index e301c7f..6dfda75 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -16995,9 +16995,11 @@ is specifically authorized by the Ada Reference Manual
 @cindex Formal container for doubly linked lists
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for doubly linked lists, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for doubly linked lists, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
 @section @code{Ada.Containers.Formal_Hashed_Maps} (@file{a-cfhama.ads})
@@ -17005,9 +17007,11 @@ code using such containers.
 @cindex Formal container for hashed maps
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for hashed maps, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for hashed maps, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
 @section @code{Ada.Containers.Formal_Hashed_Sets} (@file{a-cfhase.ads})
@@ -17015,9 +17019,11 @@ code using such containers.
 @cindex Formal container for hashed sets
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for hashed sets, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for hashed sets, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
 @section @code{Ada.Containers.Formal_Ordered_Maps} (@file{a-cforma.ads})
@@ -17025,9 +17031,11 @@ code using such containers.
 @cindex Formal container for ordered maps
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for ordered maps, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for ordered maps, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
 @section @code{Ada.Containers.Formal_Ordered_Sets} (@file{a-cforse.ads})
@@ -17035,9 +17043,11 @@ code using such containers.
 @cindex Formal container for ordered sets
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for ordered sets, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for ordered sets, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Containers.Formal_Vectors (a-cofove.ads)
 @section @code{Ada.Containers.Formal_Vectors} (@file{a-cofove.ads})
@@ -17045,9 +17055,11 @@ code using such containers.
 @cindex Formal container for vectors
 
 @noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for vectors, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for vectors, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
 
 @node Ada.Command_Line.Environment (a-colien.ads)
 @section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 0063a86..dbae075 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1189,10 +1189,29 @@ package body Sem_Ch13 is
 
          elsif Nkind (N) = N_Subprogram_Body then
             if No (Declarations (N)) then
-               Set_Declarations (N, New_List);
-            end if;
+               Set_Declarations (N, New_List (Prag));
+            else
+               declare
+                  D : Node_Id;
+               begin
+
+                  --  There may be several aspects associated with the body;
+                  --  preserve the ordering of the corresponding pragmas.
+
+                  D := First (Declarations (N));
+                  while Present (D) loop
+                     exit when Nkind (D) /= N_Pragma
+                       or else not From_Aspect_Specification (D);
+                     Next (D);
+                  end loop;
 
-            Append (Prag, Declarations (N));
+                  if No (D) then
+                     Append (Prag, Declarations (N));
+                  else
+                     Insert_Before (D, Prag);
+                  end if;
+               end;
+            end if;
 
          --  Default
 
@@ -2231,6 +2250,8 @@ package body Sem_Ch13 is
                               end;
                            end if;
 
+                           --  Otherwise, Convention must be specified
+
                            Error_Msg_N
                              ("missing Convention aspect for Export/Import",
                               Aspect);