2013-07-05 Claire Dross <dross@adacore.com>

	* a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cforma.ads,
	a-cforse.ads, a-cofove.ads: Add preconditions when needed +
	container types are not tagged any more.

2013-07-05  Thomas Quinot  <quinot@adacore.com>

	* freeze.adb (Freeze_Entity): For an object with captured
	initialization statements, do not remove Init_Stmts from the
	enclosing list, as Freeze_All might rely on it to know where to
	stop freezing.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@200708 138bc75d-0d04-0410-961f-82ee72b054a4

9 files changed, 347 insertions, 140 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 44b72d4c969..1c3bbabfc00 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,16 @@
+2013-07-05  Claire Dross  <dross@adacore.com>
+
+	* a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cforma.ads,
+	a-cforse.ads, a-cofove.ads: Add preconditions when needed +
+	container types are not tagged any more.
+
+2013-07-05  Thomas Quinot  <quinot@adacore.com>
+
+	* freeze.adb (Freeze_Entity): For an object with captured
+	initialization statements, do not remove Init_Stmts from the
+	enclosing list, as Freeze_All might rely on it to know where to
+	stop freezing.
+
 2013-07-05  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch4.adb, a-cfdlli.ads, a-ngelfu.ads, s-bignum.adb: Minor
diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index 8ea3c4c348d..bfa8ffbcb90 100644
--- a/gcc/ada/a-cfdlli.ads
+++ b/gcc/ada/a-cfdlli.ads
@@ -153,15 +153,11 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
 
    procedure Delete_First
      (Container : in out List;
-      Count     : Count_Type := 1)
-   with
-     Pre => not Is_Empty (Container);
+      Count     : Count_Type := 1);
 
    procedure Delete_Last
      (Container : in out List;
-      Count     : Count_Type := 1)
-   with
-     Pre => not Is_Empty (Container);
+      Count     : Count_Type := 1);
 
    procedure Reverse_Elements (Container : in out List);
 
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index fdbd7a0a8a4..93a47c56817 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -64,7 +64,7 @@ generic
 package Ada.Containers.Formal_Hashed_Maps is
    pragma Pure;
 
-   type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
+   type Map (Capacity : Count_Type; Modulus : Hash_Type) is private;
    pragma Preelaborable_Initialization (Map);
 
    type Cursor is private;
@@ -80,7 +80,9 @@ package Ada.Containers.Formal_Hashed_Maps is
 
    procedure Reserve_Capacity
      (Container : in out Map;
-      Capacity  : Count_Type);
+      Capacity  : Count_Type)
+   with
+     Pre => Capacity <= Container.Capacity;
 
    function Length (Container : Map) return Count_Type;
 
@@ -88,67 +90,91 @@ package Ada.Containers.Formal_Hashed_Maps is
 
    procedure Clear (Container : in out Map);
 
-   procedure Assign (Target : in out Map; Source : Map);
+   procedure Assign (Target : in out Map; Source : Map) with
+     Pre => Target.Capacity >= Length (Source);
 
-   --  Copy returns a container stricty equal to Source
-   --  It must have the same cursors associated to each element
-   --  Therefore:
-   --  - capacity=0 means use container.capacity as cap of tgt
-   --  - the modulus cannot be changed.
    function Copy
      (Source   : Map;
-      Capacity : Count_Type := 0) return Map;
+      Capacity : Count_Type := 0) return Map
+   with
+     Pre => Capacity >= Source.Capacity;
+   --  Copy returns a container stricty equal to Source. It must have
+   --  the same cursors associated with each element. Therefore:
+   --  - capacity=0 means use container.capacity as capacity of target
+   --  - the modulus cannot be changed.
 
-   function Key (Container : Map; Position : Cursor) return Key_Type;
+   function Key (Container : Map; Position : Cursor) return Key_Type with
+     Pre => Has_Element (Container, Position);
 
-   function Element (Container : Map; Position : Cursor) return Element_Type;
+   function Element
+     (Container : Map;
+      Position  : Cursor) return Element_Type
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Map;
       Position  : Cursor;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Has_Element (Container, Position);
 
-   procedure Move (Target : in out Map; Source : in out Map);
+   procedure Move (Target : in out Map; Source : in out Map) with
+     Pre => Target.Capacity >= Length (Source);
 
    procedure Insert
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type;
       Position  : out Cursor;
-      Inserted  : out Boolean);
+      Inserted  : out Boolean)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity
+              and then (not Contains (Container, Key));
 
    procedure Include
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Replace
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Contains (Container, Key);
 
    procedure Exclude (Container : in out Map; Key : Key_Type);
 
-   procedure Delete (Container : in out Map; Key : Key_Type);
+   procedure Delete (Container : in out Map; Key : Key_Type) with
+     Pre => Contains (Container, Key);
 
-   procedure Delete (Container : in out Map; Position : in out Cursor);
+   procedure Delete (Container : in out Map; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position);
 
    function First (Container : Map) return Cursor;
 
-   function Next (Container : Map; Position : Cursor) return Cursor;
+   function Next (Container : Map; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Next (Container : Map; Position : in out Cursor);
+   procedure Next (Container : Map; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find (Container : Map; Key : Key_Type) return Cursor;
 
    function Contains (Container : Map; Key : Key_Type) return Boolean;
 
-   function Element (Container : Map; Key : Key_Type) return Element_Type;
+   function Element (Container : Map; Key : Key_Type) return Element_Type with
+     Pre => Contains (Container, Key);
 
    function Has_Element (Container : Map; Position : Cursor) return Boolean;
 
@@ -175,8 +201,10 @@ package Ada.Containers.Formal_Hashed_Maps is
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
-   function Left  (Container : Map; Position : Cursor) return Map;
-   function Right (Container : Map; Position : Cursor) return Map;
+   function Left  (Container : Map; Position : Cursor) return Map with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
+   function Right (Container : Map; Position : Cursor) return Map 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
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index a9278dcdbf0..22bfda97e89 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -66,7 +66,7 @@ generic
 package Ada.Containers.Formal_Hashed_Sets is
    pragma Pure;
 
-   type Set (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
+   type Set (Capacity : Count_Type; Modulus : Hash_Type) is private;
    pragma Preelaborable_Initialization (Set);
 
    type Cursor is private;
@@ -86,7 +86,9 @@ package Ada.Containers.Formal_Hashed_Sets is
 
    procedure Reserve_Capacity
      (Container : in out Set;
-      Capacity  : Count_Type);
+      Capacity  : Count_Type)
+   with
+     Pre => Capacity <= Container.Capacity;
 
    function Length (Container : Set) return Count_Type;
 
@@ -94,39 +96,60 @@ package Ada.Containers.Formal_Hashed_Sets is
 
    procedure Clear (Container : in out Set);
 
-   procedure Assign (Target : in out Set; Source : Set);
+   procedure Assign (Target : in out Set; Source : Set) with
+     Pre => Target.Capacity >= Length (Source);
 
-   function Copy (Source   : Set;
-                  Capacity : Count_Type := 0) return Set;
+   function Copy
+     (Source   : Set;
+      Capacity : Count_Type := 0) return Set
+   with
+     Pre => Capacity >= Source.Capacity;
 
-   function Element (Container : Set; Position : Cursor) return Element_Type;
+   function Element
+     (Container : Set;
+      Position  : Cursor) return Element_Type
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Set;
       Position  : Cursor;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Has_Element (Container, Position);
 
-   procedure Move (Target : in out Set; Source : in out Set);
+   procedure Move (Target : in out Set; Source : in out Set) with
+     Pre => Target.Capacity >= Length (Source);
 
    procedure Insert
      (Container : in out Set;
       New_Item  : Element_Type;
       Position  : out Cursor;
-      Inserted  : out Boolean);
+      Inserted  : out Boolean)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
-   procedure Insert  (Container : in out Set; New_Item : Element_Type);
+   procedure Insert  (Container : in out Set; New_Item : Element_Type) with
+     Pre => Length (Container) < Container.Capacity
+              and then (not Contains (Container, New_Item));
 
-   procedure Include (Container : in out Set; New_Item : Element_Type);
+   procedure Include (Container : in out Set; New_Item : Element_Type) with
+     Pre => Length (Container) < Container.Capacity;
 
-   procedure Replace (Container : in out Set; New_Item : Element_Type);
+   procedure Replace (Container : in out Set; New_Item : Element_Type) with
+     Pre => Contains (Container, New_Item);
 
    procedure Exclude (Container : in out Set; Item     : Element_Type);
 
-   procedure Delete  (Container : in out Set; Item     : Element_Type);
+   procedure Delete  (Container : in out Set; Item     : Element_Type) with
+     Pre => Contains (Container, Item);
 
-   procedure Delete (Container : in out Set; Position  : in out Cursor);
+   procedure Delete (Container : in out Set; Position  : in out Cursor) with
+     Pre => Has_Element (Container, Position);
 
-   procedure Union (Target : in out Set; Source : Set);
+   procedure Union (Target : in out Set; Source : Set) with
+     Pre => Length (Target) + Length (Source) -
+              Length (Intersection (Target, Source)) <= Target.Capacity;
 
    function Union (Left, Right : Set) return Set;
 
@@ -149,7 +172,7 @@ package Ada.Containers.Formal_Hashed_Sets is
    function Symmetric_Difference (Left, Right : Set) return Set;
 
    function "xor" (Left, Right : Set) return Set
-                   renames Symmetric_Difference;
+     renames Symmetric_Difference;
 
    function Overlap (Left, Right : Set) return Boolean;
 
@@ -157,9 +180,11 @@ package Ada.Containers.Formal_Hashed_Sets is
 
    function First (Container : Set) return Cursor;
 
-   function Next (Container : Set; Position : Cursor) return Cursor;
+   function Next (Container : Set; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Next (Container : Set; Position : in out Cursor);
+   procedure Next (Container : Set; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find
      (Container : Set;
@@ -217,8 +242,10 @@ package Ada.Containers.Formal_Hashed_Sets is
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
-   function Left  (Container : Set; Position : Cursor) return Set;
-   function Right (Container : Set; Position : Cursor) return Set;
+   function Left  (Container : Set; Position : Cursor) return Set with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
+   function Right (Container : Set; Position : Cursor) return Set 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
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index c96fee02d51..8e323e19dfb 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -67,7 +67,7 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
 
-   type Map (Capacity : Count_Type) is tagged private;
+   type Map (Capacity : Count_Type) is private;
    pragma Preelaborable_Initialization (Map);
 
    type Cursor is private;
@@ -85,48 +85,69 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    procedure Clear (Container : in out Map);
 
-   procedure Assign (Target : in out Map; Source : Map);
+   procedure Assign (Target : in out Map; Source : Map) with
+     Pre => Target.Capacity >= Length (Source);
 
-   function Copy (Source : Map; Capacity : Count_Type := 0) return Map;
+   function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
+     Pre => Capacity >= Source.Capacity;
 
-   function Key (Container : Map; Position : Cursor) return Key_Type;
+   function Key (Container : Map; Position : Cursor) return Key_Type with
+     Pre => Has_Element (Container, Position);
 
-   function Element (Container : Map; Position : Cursor) return Element_Type;
+   function Element
+     (Container : Map;
+      Position  : Cursor) return Element_Type
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Map;
       Position  : Cursor;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Has_Element (Container, Position);
 
-   procedure Move (Target : in out Map; Source : in out Map);
+   procedure Move (Target : in out Map; Source : in out Map) with
+     Pre => Target.Capacity >= Length (Source);
 
    procedure Insert
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type;
       Position  : out Cursor;
-      Inserted  : out Boolean);
+      Inserted  : out Boolean)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity
+              and then (not Contains (Container, Key));
 
    procedure Include
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Replace
      (Container : in out Map;
       Key       : Key_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Contains (Container, Key);
 
    procedure Exclude (Container : in out Map; Key : Key_Type);
 
-   procedure Delete (Container : in out Map; Key : Key_Type);
+   procedure Delete (Container : in out Map; Key : Key_Type) with
+     Pre => Contains (Container, Key);
 
-   procedure Delete (Container : in out Map; Position : in out Cursor);
+   procedure Delete (Container : in out Map; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position);
 
    procedure Delete_First (Container : in out Map);
 
@@ -134,27 +155,36 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    function First (Container : Map) return Cursor;
 
-   function First_Element (Container : Map) return Element_Type;
+   function First_Element (Container : Map) return Element_Type with
+     Pre => not Is_Empty (Container);
 
-   function First_Key (Container : Map) return Key_Type;
+   function First_Key (Container : Map) return Key_Type with
+     Pre => not Is_Empty (Container);
 
    function Last (Container : Map) return Cursor;
 
-   function Last_Element (Container : Map) return Element_Type;
+   function Last_Element (Container : Map) return Element_Type with
+     Pre => not Is_Empty (Container);
 
-   function Last_Key (Container : Map) return Key_Type;
+   function Last_Key (Container : Map) return Key_Type with
+     Pre => not Is_Empty (Container);
 
-   function Next (Container : Map; Position : Cursor) return Cursor;
+   function Next (Container : Map; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Next (Container : Map; Position : in out Cursor);
+   procedure Next (Container : Map; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Previous (Container : Map; Position : Cursor) return Cursor;
+   function Previous (Container : Map; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Previous (Container : Map; Position : in out Cursor);
+   procedure Previous (Container : Map; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find (Container : Map; Key : Key_Type) return Cursor;
 
-   function Element (Container : Map; Key : Key_Type) return Element_Type;
+   function Element (Container : Map; Key : Key_Type) return Element_Type with
+     Pre => Contains (Container, Key);
 
    function Floor (Container : Map; Key : Key_Type) return Cursor;
 
@@ -169,8 +199,10 @@ package Ada.Containers.Formal_Ordered_Maps is
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
-   function Left  (Container : Map; Position : Cursor) return Map;
-   function Right (Container : Map; Position : Cursor) return Map;
+   function Left  (Container : Map; Position : Cursor) return Map with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
+   function Right (Container : Map; Position : Cursor) return Map 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
diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 77862a6df34..35e4613b9a8 100644
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -65,9 +65,8 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
 
-   type Set (Capacity : Count_Type) is tagged private;
-   --  why is this commented out ???
-   --  pragma Preelaborable_Initialization (Set);
+   type Set (Capacity : Count_Type) is private;
+   pragma Preelaborable_Initialization (Set);
 
    type Cursor is private;
    pragma Preelaborable_Initialization (Cursor);
@@ -88,36 +87,54 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    procedure Clear (Container : in out Set);
 
-   procedure Assign (Target : in out Set; Source : Set);
+   procedure Assign (Target : in out Set; Source : Set) with
+     Pre => Target.Capacity >= Length (Source);
 
-   function Copy (Source : Set; Capacity : Count_Type := 0) return Set;
+   function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
+     Pre => Capacity >= Source.Capacity;
 
-   function Element (Container : Set; Position : Cursor) return Element_Type;
+   function Element
+     (Container : Set;
+      Position  : Cursor) return Element_Type
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Set;
       Position  : Cursor;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Has_Element (Container, Position);
 
-   procedure Move (Target : in out Set; Source : in out Set);
+   procedure Move (Target : in out Set; Source : in out Set) with
+     Pre => Target.Capacity >= Length (Source);
 
    procedure Insert
      (Container : in out Set;
       New_Item  : Element_Type;
       Position  : out Cursor;
-      Inserted  : out Boolean);
+      Inserted  : out Boolean)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Set;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity
+              and then (not Contains (Container, New_Item));
 
    procedure Include
      (Container : in out Set;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Replace
      (Container : in out Set;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Contains (Container, New_Item);
 
    procedure Exclude
      (Container : in out Set;
@@ -125,17 +142,23 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    procedure Delete
      (Container : in out Set;
-      Item      : Element_Type);
+      Item      : Element_Type)
+   with
+     Pre => Contains (Container, Item);
 
    procedure Delete
      (Container : in out Set;
-      Position  : in out Cursor);
+      Position  : in out Cursor)
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Delete_First (Container : in out Set);
 
    procedure Delete_Last (Container : in out Set);
 
-   procedure Union (Target : in out Set; Source : Set);
+   procedure Union (Target : in out Set; Source : Set) with
+     Pre => Length (Target) + Length (Source) -
+              Length (Intersection (Target, Source)) <= Target.Capacity;
 
    function Union (Left, Right : Set) return Set;
 
@@ -165,19 +188,25 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    function First (Container : Set) return Cursor;
 
-   function First_Element (Container : Set) return Element_Type;
+   function First_Element (Container : Set) return Element_Type with
+     Pre => not Is_Empty (Container);
 
    function Last (Container : Set) return Cursor;
 
-   function Last_Element (Container : Set) return Element_Type;
+   function Last_Element (Container : Set) return Element_Type with
+     Pre => not Is_Empty (Container);
 
-   function Next (Container : Set; Position : Cursor) return Cursor;
+   function Next (Container : Set; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Next (Container : Set; Position : in out Cursor);
+   procedure Next (Container : Set; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Previous (Container : Set; Position : Cursor) return Cursor;
+   function Previous (Container : Set; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Previous (Container : Set; Position : in out Cursor);
+   procedure Previous (Container : Set; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find (Container : Set; Item : Element_Type) return Cursor;
 
@@ -228,8 +257,10 @@ package Ada.Containers.Formal_Ordered_Sets is
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
-   function Left  (Container : Set; Position : Cursor) return Set;
-   function Right (Container : Set; Position : Cursor) return Set;
+   function Left  (Container : Set; Position : Cursor) return Set with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
+   function Right (Container : Set; Position : Cursor) return Set 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
diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb
index 69de29db5d4..240715dca75 100644
--- a/gcc/ada/a-cofove.adb
+++ b/gcc/ada/a-cofove.adb
@@ -251,7 +251,7 @@ package body Ada.Containers.Formal_Vectors is
          raise Constraint_Error;
       end if;
 
-      Target.Clear;
+      Clear (Target);
 
       Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
       Target.Last := Source.Last;
@@ -641,10 +641,10 @@ package body Ada.Containers.Formal_Vectors is
             --  I think we're missing this check in a-convec.adb...  ???
 
             I := Length (Target);
-            Target.Set_Length (I + Length (Source));
+            Set_Length (Target, I + Length (Source));
 
             J := Length (Target);
-            while not Source.Is_Empty loop
+            while not Is_Empty (Source) loop
                pragma Assert (Length (Source) <= 1
                  or else not (SA (Length (Source)) <
                      SA (Length (Source) - 1)));
@@ -1487,20 +1487,20 @@ package body Ada.Containers.Formal_Vectors is
 
    procedure Set_Length
      (Container : in out Vector;
-      Length    : Count_Type)
+      New_Length    : Count_Type)
    is
    begin
-      if Length = Formal_Vectors.Length (Container) then
+      if New_Length = Formal_Vectors.Length (Container) then
          return;
       end if;
 
-      if Length > Container.Capacity then
+      if New_Length > Container.Capacity then
          raise Constraint_Error;  -- ???
       end if;
 
       declare
          Last_As_Int : constant Int'Base :=
-           Int (Index_Type'First) + Int (Length) - 1;
+           Int (Index_Type'First) + Int (New_Length) - 1;
       begin
          Container.Last := Index_Type'Base (Last_As_Int);
       end;
diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index 4d943837b82..9ca84da460f 100644
--- a/gcc/ada/a-cofove.ads
+++ b/gcc/ada/a-cofove.ads
@@ -73,7 +73,7 @@ package Ada.Containers.Formal_Vectors is
 
    No_Index : constant Extended_Index := Extended_Index'First;
 
-   type Vector (Capacity : Count_Type) is tagged private;
+   type Vector (Capacity : Count_Type) is private;
 
    type Cursor is private;
    pragma Preelaborable_Initialization (Cursor);
@@ -100,23 +100,30 @@ package Ada.Containers.Formal_Vectors is
 
    procedure Reserve_Capacity
      (Container : in out Vector;
-      Capacity  : Count_Type);
+      Capacity  : Count_Type)
+   with
+     Pre => Capacity <= Container.Capacity;
 
    function Length (Container : Vector) return Count_Type;
 
    procedure Set_Length
      (Container : in out Vector;
-      Length    : Count_Type);
+      New_Length    : Count_Type)
+   with
+     Pre => New_Length <= Length (Container);
 
    function Is_Empty (Container : Vector) return Boolean;
 
    procedure Clear (Container : in out Vector);
 
-   procedure Assign (Target : in out Vector; Source : Vector);
+   procedure Assign (Target : in out Vector; Source : Vector) with
+     Pre => Length (Source) <= Target.Capacity;
 
    function Copy
      (Source   : Vector;
-      Capacity : Count_Type := 0) return Vector;
+      Capacity : Count_Type := 0) return Vector
+   with
+     Pre => Length (Source) <= Capacity;
 
    function To_Cursor
      (Container : Vector;
@@ -126,86 +133,134 @@ package Ada.Containers.Formal_Vectors is
 
    function Element
      (Container : Vector;
-      Index     : Index_Type) return Element_Type;
+      Index     : Index_Type) return Element_Type
+   with
+     Pre => First_Index (Container) <= Index
+              and then Index <= Last_Index (Container);
 
    function Element
      (Container : Vector;
-      Position  : Cursor) return Element_Type;
+      Position  : Cursor) return Element_Type
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Vector;
       Index     : Index_Type;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => First_Index (Container) <= Index
+              and then Index <= Last_Index (Container);
 
    procedure Replace_Element
      (Container : in out Vector;
       Position  : Cursor;
-      New_Item  : Element_Type);
+      New_Item  : Element_Type)
+   with
+     Pre => Has_Element (Container, Position);
 
-   procedure Move (Target : in out Vector; Source : in out Vector);
+   procedure Move (Target : in out Vector; Source : in out Vector) with
+     Pre => Length (Source) <= Target.Capacity;
 
    procedure Insert
      (Container : in out Vector;
       Before    : Extended_Index;
-      New_Item  : Vector);
+      New_Item  : Vector)
+   with
+     Pre => First_Index (Container) <= Before
+              and then Before <= Last_Index (Container) + 1
+              and then Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Vector;
       Before    : Cursor;
-      New_Item  : Vector);
+      New_Item  : Vector)
+   with
+     Pre => Length (Container) < Container.Capacity
+              and then (Has_Element (Container, Before)
+                         or else Before = No_Element);
 
    procedure Insert
      (Container : in out Vector;
       Before    : Cursor;
       New_Item  : Vector;
-      Position  : out Cursor);
+      Position  : out Cursor)
+   with
+     Pre => Length (Container) < Container.Capacity
+              and then (Has_Element (Container, Before)
+                         or else Before = No_Element);
 
    procedure Insert
      (Container : in out Vector;
       Before    : Extended_Index;
       New_Item  : Element_Type;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => First_Index (Container) <= Before
+              and then Before <= Last_Index (Container) + 1
+              and then Length (Container) + Count <= Container.Capacity;
 
    procedure Insert
      (Container : in out Vector;
       Before    : Cursor;
       New_Item  : Element_Type;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => Length (Container) + Count <= Container.Capacity
+              and then (Has_Element (Container, Before)
+                         or else Before = No_Element);
 
    procedure Insert
      (Container : in out Vector;
       Before    : Cursor;
       New_Item  : Element_Type;
       Position  : out Cursor;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => Length (Container) + Count <= Container.Capacity
+              and then (Has_Element (Container, Before)
+                         or else Before = No_Element);
 
    procedure Prepend
      (Container : in out Vector;
-      New_Item  : Vector);
+      New_Item  : Vector)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Prepend
      (Container : in out Vector;
       New_Item  : Element_Type;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => Length (Container) + Count <= Container.Capacity;
 
    procedure Append
      (Container : in out Vector;
-      New_Item  : Vector);
+      New_Item  : Vector)
+   with
+     Pre => Length (Container) < Container.Capacity;
 
    procedure Append
      (Container : in out Vector;
       New_Item  : Element_Type;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => Length (Container) + Count <= Container.Capacity;
 
    procedure Delete
      (Container : in out Vector;
       Index     : Extended_Index;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => First_Index (Container) <= Index
+              and then Index <= Last_Index (Container) + 1;
 
    procedure Delete
      (Container : in out Vector;
       Position  : in out Cursor;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Pre => Has_Element (Container, Position);
 
    procedure Delete_First
      (Container : in out Vector;
@@ -217,29 +272,39 @@ package Ada.Containers.Formal_Vectors is
 
    procedure Reverse_Elements (Container : in out Vector);
 
-   procedure Swap (Container : in out Vector; I, J : Index_Type);
+   procedure Swap (Container : in out Vector; I, J : Index_Type) with
+     Pre => First_Index (Container) <= I and then I <= Last_Index (Container)
+              and then First_Index (Container) <= J
+              and then J <= Last_Index (Container);
 
-   procedure Swap (Container : in out Vector; I, J : Cursor);
+   procedure Swap (Container : in out Vector; I, J : Cursor) with
+     Pre => Has_Element (Container, I) and then Has_Element (Container, J);
 
    function First_Index (Container : Vector) return Index_Type;
 
    function First (Container : Vector) return Cursor;
 
-   function First_Element (Container : Vector) return Element_Type;
+   function First_Element (Container : Vector) return Element_Type with
+     Pre => not Is_Empty (Container);
 
    function Last_Index (Container : Vector) return Extended_Index;
 
    function Last (Container : Vector) return Cursor;
 
-   function Last_Element (Container : Vector) return Element_Type;
+   function Last_Element (Container : Vector) return Element_Type with
+     Pre => not Is_Empty (Container);
 
-   function Next (Container : Vector; Position : Cursor) return Cursor;
+   function Next (Container : Vector; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Next (Container : Vector; Position : in out Cursor);
+   procedure Next (Container : Vector; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Previous (Container : Vector; Position : Cursor) return Cursor;
+   function Previous (Container : Vector; Position : Cursor) return Cursor with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
-   procedure Previous (Container : Vector; Position : in out Cursor);
+   procedure Previous (Container : Vector; Position : in out Cursor) with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find_Index
      (Container : Vector;
@@ -249,7 +314,9 @@ package Ada.Containers.Formal_Vectors is
    function Find
      (Container : Vector;
       Item      : Element_Type;
-      Position  : Cursor := No_Element) return Cursor;
+      Position  : Cursor := No_Element) return Cursor
+   with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Reverse_Find_Index
      (Container : Vector;
@@ -259,7 +326,9 @@ package Ada.Containers.Formal_Vectors is
    function Reverse_Find
      (Container : Vector;
       Item      : Element_Type;
-      Position  : Cursor := No_Element) return Cursor;
+      Position  : Cursor := No_Element) return Cursor
+   with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
    function Contains
      (Container : Vector;
@@ -279,9 +348,11 @@ package Ada.Containers.Formal_Vectors is
 
    end Generic_Sorting;
 
-   function Left (Container : Vector; Position : Cursor) return Vector;
+   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;
+   function Right (Container : Vector; Position : Cursor) return Vector with
+     Pre => Has_Element (Container, Position) or else Position = No_Element;
 
 private
 
@@ -298,7 +369,7 @@ private
    type Elements_Array is array (Count_Type range <>) of Element_Type;
    function "=" (L, R : Elements_Array) return Boolean is abstract;
 
-   type Vector (Capacity : Count_Type) is tagged record
+   type Vector (Capacity : Count_Type) is record
       Elements : Elements_Array (1 .. Capacity);
       Last     : Extended_Index := No_Index;
    end record;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 125c3bcb6ee..81a9359e548 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3360,7 +3360,16 @@ package body Freeze is
                     and then Nkind (Expression (Init_Stmts)) = N_Null_Statement
                   then
                      Insert_List_Before (Init_Stmts, Actions (Init_Stmts));
-                     Remove (Init_Stmts);
+
+                     --  Note that we rewrite Init_Stmts into a NULL statement,
+                     --  rather than just removing it, because Freeze_All may
+                     --  depend on this particular Node_Id still being present
+                     --  in the enclosing list to signal where to stop
+                     --  freezing.
+
+                     Rewrite (Init_Stmts,
+                       Make_Null_Statement (Sloc (Init_Stmts)));
+
                      Set_Initialization_Statements (E, Empty);
                   end if;
                end;