1 files changed, 106 insertions, 35 deletions

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;