Index: a-coinve.adb
===================================================================
--- a-coinve.adb	(revision 161073)
+++ a-coinve.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2010, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -33,9 +33,6 @@ with System;  use type System.Address;
 
 package body Ada.Containers.Indefinite_Vectors is
 
-   type Int is range System.Min_Int .. System.Max_Int;
-   type UInt is mod System.Max_Binary_Modulus;
-
    procedure Free is
      new Ada.Unchecked_Deallocation (Elements_Type, Elements_Access);
 
@@ -47,10 +44,22 @@ package body Ada.Containers.Indefinite_V
    ---------
 
    function "&" (Left, Right : Vector) return Vector is
-      LN : constant Count_Type := Length (Left);
-      RN : constant Count_Type := Length (Right);
+      LN   : constant Count_Type := Length (Left);
+      RN   : constant Count_Type := Length (Right);
+      N    : Count_Type'Base;  -- length of result
+      J    : Count_Type'Base;  -- for computing intermediate values
+      Last : Index_Type'Base;  -- Last index of result
 
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the vector parameters. We could decide to make it larger, but we
+      --  have no basis for knowing how much larger, so we just allocate the
+      --  minimum amount of storage.
+
+      --  Here we handle the easy cases first, when one of the vector
+      --  parameters is empty. (We say "easy" because there's nothing to
+      --  compute, that can potentially overflow.)
+
       if LN = 0 then
          if RN = 0 then
             return Empty_Vector;
@@ -64,6 +73,11 @@ package body Ada.Containers.Indefinite_V
                          new Elements_Type (Right.Last);
 
          begin
+            --  Elements of an indefinite vector are allocated, so we cannot
+            --  use simple slice assignment to give a value to our result.
+            --  Hence we must walk the array of the Right vector, and copy
+            --  each source element individually.
+
             for I in Elements.EA'Range loop
                begin
                   if RE (I) /= null then
@@ -95,6 +109,11 @@ package body Ada.Containers.Indefinite_V
                          new Elements_Type (Left.Last);
 
          begin
+            --  Elements of an indefinite vector are allocated, so we cannot
+            --  use simple slice assignment to give a value to our result.
+            --  Hence we must walk the array of the Left vector, and copy
+            --  each source element individually.
+
             for I in Elements.EA'Range loop
                begin
                   if LE (I) /= null then
@@ -116,121 +135,161 @@ package body Ada.Containers.Indefinite_V
          end;
       end if;
 
-      declare
-         N : constant Int'Base := Int (LN) + Int (RN);
-         J : Int'Base;
+      --  Neither of the vector parameters is empty, so we must compute the
+      --  length of the result vector and its last index. (This is the harder
+      --  case, because our computations must avoid overflow.)
+
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the combined lengths. Note that we cannot
+      --  simply add the lengths, because of the possibilty of overflow.
 
-      begin
-         --  There are two constraints we need to satisfy. The first constraint
-         --  is that a container cannot have more than Count_Type'Last
-         --  elements, so we must check the sum of the combined lengths. (It
-         --  would be rare for vectors to have such a large number of elements,
-         --  so we would normally expect this first check to succeed.) The
-         --  second constraint is that the new Last index value cannot exceed
-         --  Index_Type'Last.
+      if LN > Count_Type'Last - RN then
+         raise Constraint_Error with "new length is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector.
+
+      N := LN + RN;
 
-         if N > Count_Type'Pos (Count_Type'Last) then
+      --  The second constraint is that the new Last index value cannot
+      --  exceed Index_Type'Last. We use the wider of Index_Type'Base and
+      --  Count_Type'Base as the type for intermediate values.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (N) < No_Index then
             raise Constraint_Error with "new length is out of range";
          end if;
 
-         --  We now check whether the new length would create a Last index
-         --  value greater than Index_Type'Last. This calculation requires
-         --  care, because overflow can occur when Index_Type'First is near the
-         --  end of the range of Int.
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
 
-         if Index_Type'First <= 0 then
+         Last := No_Index + Index_Type'Base (N);
 
-            --  Compute the potential Last index value in the normal way, using
-            --  Int as the type in which to perform intermediate
-            --  calculations. Int is a 64-bit type, and Count_Type is a 32-bit
-            --  type, so no overflow can occur.
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
 
-            J := Int (Index_Type'First - 1) + N;
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "new length is out of range";
+         end if;
 
-            if J > Int (Index_Type'Last) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+      elsif Index_Type'First <= 0 then
 
-         else
-            --  If Index_Type'First is within N of Int'Last, then overflow
-            --  would occur if we simply computed Last directly. So instead of
-            --  computing Last, and then determining whether its value is
-            --  greater than Index_Type'Last (as we do above), we work
-            --  backwards by computing the potential First index value, and
-            --  then checking whether that value is less than Index_Type'First.
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of length.
 
-            J := Int (Index_Type'Last) - N + 1;
+         J := Count_Type'Base (No_Index) + N;  -- Last
 
-            if J < Int (Index_Type'First) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+         if J > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "new length is out of range";
+         end if;
+
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (J);
+
+      else
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
 
-            --  We have determined that Length would not create a Last index
-            --  value outside of the range of Index_Type, so we can now safely
-            --  compute its value.
+         J := Count_Type'Base (Index_Type'Last) - N;  -- No_Index
 
-            J := Int (Index_Type'First - 1) + N;
+         if J < Count_Type'Base (No_Index) then
+            raise Constraint_Error with "new length is out of range";
          end if;
 
-         declare
-            Last : constant Index_Type := Index_Type (J);
+         --  We have determined that the result length would not create a Last
+         --  index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
 
-            LE : Elements_Array renames
-                   Left.Elements.EA (Index_Type'First .. Left.Last);
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + N);
+      end if;
 
-            RE : Elements_Array renames
-                   Right.Elements.EA (Index_Type'First .. Right.Last);
+      declare
+         LE : Elements_Array renames
+                Left.Elements.EA (Index_Type'First .. Left.Last);
 
-            Elements : Elements_Access := new Elements_Type (Last);
+         RE : Elements_Array renames
+                Right.Elements.EA (Index_Type'First .. Right.Last);
 
-            I : Index_Type'Base := No_Index;
+         Elements : Elements_Access := new Elements_Type (Last);
 
-         begin
-            for LI in LE'Range loop
-               I := I + 1;
+         I : Index_Type'Base := No_Index;
 
-               begin
-                  if LE (LI) /= null then
-                     Elements.EA (I) := new Element_Type'(LE (LI).all);
-                  end if;
+      begin
+         --  Elements of an indefinite vector are allocated, so we cannot use
+         --  simple slice assignment to give a value to our result. Hence we
+         --  must walk the array of each vector parameter, and copy each source
+         --  element individually.
 
-               exception
-                  when others =>
-                     for J in Index_Type'First .. I - 1 loop
-                        Free (Elements.EA (J));
-                     end loop;
+         for LI in LE'Range loop
+            I := I + 1;
 
-                     Free (Elements);
-                     raise;
-               end;
-            end loop;
+            begin
+               if LE (LI) /= null then
+                  Elements.EA (I) := new Element_Type'(LE (LI).all);
+               end if;
 
-            for RI in RE'Range loop
-               I := I + 1;
+            exception
+               when others =>
+                  for J in Index_Type'First .. I - 1 loop
+                     Free (Elements.EA (J));
+                  end loop;
 
-               begin
-                  if RE (RI) /= null then
-                     Elements.EA (I) := new Element_Type'(RE (RI).all);
-                  end if;
+                  Free (Elements);
+                  raise;
+            end;
+         end loop;
 
-               exception
-                  when others =>
-                     for J in Index_Type'First .. I - 1 loop
-                        Free (Elements.EA (J));
-                     end loop;
+         for RI in RE'Range loop
+            I := I + 1;
 
-                     Free (Elements);
-                     raise;
-               end;
-            end loop;
+            begin
+               if RE (RI) /= null then
+                  Elements.EA (I) := new Element_Type'(RE (RI).all);
+               end if;
 
-            return (Controlled with Elements, Last, 0, 0);
-         end;
+            exception
+               when others =>
+                  for J in Index_Type'First .. I - 1 loop
+                     Free (Elements.EA (J));
+                  end loop;
+
+                  Free (Elements);
+                  raise;
+            end;
+         end loop;
+
+         return (Controlled with Elements, Last, 0, 0);
       end;
    end "&";
 
    function "&" (Left : Vector; Right : Element_Type) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  Here we handle the easy case first, when the vector parameter (Left)
+      --  is empty.
+
       if Left.Is_Empty then
          declare
             Elements : Elements_Access := new Elements_Type (Index_Type'First);
@@ -248,8 +307,10 @@ package body Ada.Containers.Indefinite_V
          end;
       end if;
 
-      --  We must satisfy two constraints: the new length cannot exceed
-      --  Count_Type'Last, and the new Last index cannot exceed
+      --  The vector parameter is not empty, so we must compute the length of
+      --  the result vector and its last index, but in such a way that overflow
+      --  is avoided. We must satisfy two constraints: the new length cannot
+      --  exceed Count_Type'Last, and the new Last index cannot exceed
       --  Index_Type'Last.
 
       if Left.Length = Count_Type'Last then
@@ -306,6 +367,14 @@ package body Ada.Containers.Indefinite_V
 
    function "&" (Left : Element_Type; Right : Vector) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  Here we handle the easy case first, when the vector parameter (Right)
+      --  is empty.
+
       if Right.Is_Empty then
          declare
             Elements : Elements_Access := new Elements_Type (Index_Type'First);
@@ -323,8 +392,10 @@ package body Ada.Containers.Indefinite_V
          end;
       end if;
 
-      --  We must satisfy two constraints: the new length cannot exceed
-      --  Count_Type'Last, and the new Last index cannot exceed
+      --  The vector parameter is not empty, so we must compute the length of
+      --  the result vector and its last index, but in such a way that overflow
+      --  is avoided. We must satisfy two constraints: the new length cannot
+      --  exceed Count_Type'Last, and the new Last index cannot exceed
       --  Index_Type'Last.
 
       if Right.Length = Count_Type'Last then
@@ -380,6 +451,17 @@ package body Ada.Containers.Indefinite_V
 
    function "&" (Left, Right : Element_Type) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  We must compute the length of the result vector and its last index,
+      --  but in such a way that overflow is avoided. We must satisfy two
+      --  constraints: the new length cannot exceed Count_Type'Last (here, we
+      --  know that that condition is satisfied), and the new Last index cannot
+      --  exceed Index_Type'Last.
+
       if Index_Type'First >= Index_Type'Last then
          raise Constraint_Error with "new length is out of range";
       end if;
@@ -572,75 +654,177 @@ package body Ada.Containers.Indefinite_V
       Index     : Extended_Index;
       Count     : Count_Type := 1)
    is
-   begin
+      Old_Last : constant Index_Type'Base := Container.Last;
+      New_Last : Index_Type'Base;
+      Count2   : Count_Type'Base;  -- count of items from Index to Old_Last
+      J        : Index_Type'Base;  -- first index of items that slide down
+
+   begin
+      --  Delete removes items from the vector, the number of which is the
+      --  minimum of the specified Count and the items (if any) that exist from
+      --  Index to Container.Last. There are no constraints on the specified
+      --  value of Count (it can be larger than what's available at this
+      --  position in the vector, for example), but there are constraints on
+      --  the allowed values of the Index.
+
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying which items
+      --  should be deleted, so we must manually check. (That the user is
+      --  allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
+
       if Index < Index_Type'First then
          raise Constraint_Error with "Index is out of range (too small)";
       end if;
 
-      if Index > Container.Last then
-         if Index > Container.Last + 1 then
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows the
+      --  corner case of deleting no items from the back end of the vector to
+      --  be treated as a no-op. (It is assumed that specifying an index value
+      --  greater than Last + 1 indicates some deeper flaw in the caller's
+      --  algorithm, so that case is treated as a proper error.)
+
+      if Index > Old_Last then
+         if Index > Old_Last + 1 then
             raise Constraint_Error with "Index is out of range (too large)";
          end if;
 
          return;
       end if;
 
+      --  Here and elsewhere we treat deleting 0 items from the container as a
+      --  no-op, even when the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
+      --  The internal elements array isn't guaranteed to exist unless we have
+      --  elements, so we handle that case here in order to avoid having to
+      --  check it later. (Note that an empty vector can never be busy, so
+      --  there's no semantic harm in returning early.)
+
+      if Container.Is_Empty then
+         return;
+      end if;
+
+      --  The tampering bits exist to prevent an item from being deleted (or
+      --  otherwise harmfully manipulated) while it is being visited. Query,
+      --  Update, and Iterate increment the busy count on entry, and decrement
+      --  the count on exit. Delete checks the count to determine whether it is
+      --  being called while the associated callback procedure is executing.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
-      declare
-         Index_As_Int    : constant Int := Int (Index);
-         Old_Last_As_Int : constant Int := Int (Container.Last);
+      --  We first calculate what's available for deletion starting at
+      --  Index. Here and elsewhere we use the wider of Index_Type'Base and
+      --  Count_Type'Base as the type for intermediate values. (See function
+      --  Length for more information.)
 
-         Count1 : constant Int'Base := Int (Count);
-         Count2 : constant Int'Base := Old_Last_As_Int - Index_As_Int + 1;
-         N      : constant Int'Base := Int'Min (Count1, Count2);
+      if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then
+         Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1;
 
-         J_As_Int : constant Int'Base := Index_As_Int + N;
-         E        : Elements_Array renames Container.Elements.EA;
+      else
+         Count2 := Count_Type'Base (Old_Last - Index + 1);
+      end if;
 
-      begin
-         if J_As_Int > Old_Last_As_Int then
+      --  If the number of elements requested (Count) for deletion is equal to
+      --  (or greater than) the number of elements available (Count2) for
+      --  deletion beginning at Index, then everything from Index to
+      --  Container.Last is deleted (this is equivalent to Delete_Last).
+
+      if Count >= Count2 then
+         --  Elements in an indefinite vector are allocated, so we must iterate
+         --  over the loop and deallocate elements one-at-a-time. We work from
+         --  back to front, deleting the last element during each pass, in
+         --  order to gracefully handle deallocation failures.
+
+         declare
+            EA : Elements_Array renames Container.Elements.EA;
+
+         begin
             while Container.Last >= Index loop
                declare
                   K : constant Index_Type := Container.Last;
-                  X : Element_Access := E (K);
+                  X : Element_Access := EA (K);
 
                begin
-                  E (K) := null;
+                  --  We first isolate the element we're deleting, removing it
+                  --  from the vector before we attempt to deallocate it, in
+                  --  case the deallocation fails.
+
+                  EA (K) := null;
                   Container.Last := K - 1;
+
+                  --  Container invariants have been restored, so it is now
+                  --  safe to attempt to deallocate the element.
+
                   Free (X);
                end;
             end loop;
+         end;
 
-         else
-            declare
-               J : constant Index_Type := Index_Type (J_As_Int);
+         return;
+      end if;
+
+      --  There are some elements that aren't being deleted (the requested
+      --  count was less than the available count), so we must slide them down
+      --  to Index. We first calculate the index values of the respective array
+      --  slices, using the wider of Index_Type'Base and Count_Type'Base as the
+      --  type for intermediate calculations. For the elements that slide down,
+      --  index value New_Last is the last index value of their new home, and
+      --  index value J is the first index of their old home.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := Old_Last - Index_Type'Base (Count);
+         J := Index + Index_Type'Base (Count);
 
-               New_Last_As_Int : constant Int'Base := Old_Last_As_Int - N;
-               New_Last        : constant Index_Type :=
-                                   Index_Type (New_Last_As_Int);
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count);
+         J := Index_Type'Base (Count_Type'Base (Index) + Count);
+      end if;
+
+      --  The internal elements array isn't guaranteed to exist unless we have
+      --  elements, but we have that guarantee here because we know we have
+      --  elements to slide.  The array index values for each slice have
+      --  already been determined, so what remains to be done is to first
+      --  deallocate the elements that are being deleted, and then slide down
+      --  to Index the elements that aren't being deleted.
+
+      declare
+         EA : Elements_Array renames Container.Elements.EA;
+
+      begin
+         --  Before we can slide down the elements that aren't being deleted,
+         --  we need to deallocate the elements that are being deleted.
+
+         for K in Index .. J - 1 loop
+            declare
+               X : Element_Access := EA (K);
 
             begin
-               for K in Index .. J - 1 loop
-                  declare
-                     X : Element_Access := E (K);
-                  begin
-                     E (K) := null;
-                     Free (X);
-                  end;
-               end loop;
+               --  First we remove the element we're about to deallocate from
+               --  the vector, in case the deallocation fails, in order to
+               --  preserve representation invariants.
 
-               E (Index .. New_Last) := E (J .. Container.Last);
-               Container.Last := New_Last;
+               EA (K) := null;
+
+               --  The element has been removed from the vector, so it is now
+               --  safe to attempt to deallocate it.
+
+               Free (X);
             end;
-         end if;
+         end loop;
+
+         EA (Index .. New_Last) := EA (J .. Old_Last);
+         Container.Last := New_Last;
       end;
    end Delete;
 
@@ -698,32 +882,64 @@ package body Ada.Containers.Indefinite_V
      (Container : in out Vector;
       Count     : Count_Type := 1)
    is
-      N : constant Count_Type := Length (Container);
-
    begin
-      if Count = 0
-        or else N = 0
-      then
+      --  It is not permitted to delete items while the container is busy (for
+      --  example, we're in the middle of a passive iteration). However, we
+      --  always treat deleting 0 items as a no-op, even when we're busy, so we
+      --  simply return without checking.
+
+      if Count = 0 then
+         return;
+      end if;
+
+      --  We cannot simply subsume the empty case into the loop below (the loop
+      --  would iterate 0 times), because we rename the internal array object
+      --  (which is allocated), but an empty vector isn't guaranteed to have
+      --  actually allocated an array. (Note that an empty vector can never be
+      --  busy, so there's no semantic harm in returning early here.)
+
+      if Container.Is_Empty then
          return;
       end if;
 
+      --  The tampering bits exist to prevent an item from being deleted (or
+      --  otherwise harmfully manipulated) while it is being visited. Query,
+      --  Update, and Iterate increment the busy count on entry, and decrement
+      --  the count on exit. Delete_Last checks the count to determine whether
+      --  it is being called while the associated callback procedure is
+      --  executing.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
+      --  Elements in an indefinite vector are allocated, so we must iterate
+      --  over the loop and deallocate elements one-at-a-time. We work from
+      --  back to front, deleting the last element during each pass, in order
+      --  to gracefully handle deallocation failures.
+
       declare
          E : Elements_Array renames Container.Elements.EA;
 
       begin
-         for Indx in 1 .. Count_Type'Min (Count, N) loop
+         for Indx in 1 .. Count_Type'Min (Count, Container.Length) loop
             declare
                J : constant Index_Type := Container.Last;
                X : Element_Access := E (J);
 
             begin
+               --  Note that we first isolate the element we're deleting,
+               --  removing it from the vector, before we actually deallocate
+               --  it, in order to preserve representation invariants even if
+               --  the deallocation fails.
+
                E (J) := null;
                Container.Last := J - 1;
+
+               --  Container invariants have been restored, so it is now safe
+               --  to deallocate the element.
+
                Free (X);
             end;
          end loop;
@@ -1073,22 +1289,42 @@ package body Ada.Containers.Indefinite_V
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    is
-      N               : constant Int := Int (Count);
-
-      First           : constant Int := Int (Index_Type'First);
-      New_Last_As_Int : Int'Base;
-      New_Last        : Index_Type;
-      New_Length      : UInt;
-      Max_Length      : constant UInt := UInt (Count_Type'Last);
+      Old_Length : constant Count_Type := Container.Length;
 
-      Dst             : Elements_Access;
+      Max_Length : Count_Type'Base;  -- determined from range of Index_Type
+      New_Length : Count_Type'Base;  -- sum of current length and Count
+      New_Last   : Index_Type'Base;  -- last index of vector after insertion
+
+      Index : Index_Type'Base;  -- scratch for intermediate values
+      J     : Count_Type'Base;  -- scratch
+
+      New_Capacity : Count_Type'Base;  -- length of new, expanded array
+      Dst_Last     : Index_Type'Base;  -- last index of new, expanded array
+      Dst          : Elements_Access;  -- new, expanded internal array
+
+   begin
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying where the new
+      --  items should be inserted, so we must manually check. (That the user
+      --  is allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
 
-   begin
       if Before < Index_Type'First then
          raise Constraint_Error with
            "Before index is out of range (too small)";
       end if;
 
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows for the
+      --  case of appending items to the back end of the vector. (It is assumed
+      --  that specifying an index value greater than Last + 1 indicates some
+      --  deeper flaw in the caller's algorithm, so that case is treated as a
+      --  proper error.)
+
       if Before > Container.Last
         and then Before > Container.Last + 1
       then
@@ -1096,197 +1332,371 @@ package body Ada.Containers.Indefinite_V
            "Before index is out of range (too large)";
       end if;
 
+      --  We treat inserting 0 items into the container as a no-op, even when
+      --  the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
-      declare
-         Old_Last_As_Int : constant Int := Int (Container.Last);
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the current length and the insertion
+      --  count. Note that we cannot simply add these values, because of the
+      --  possibilty of overflow.
+
+      if Old_Length > Count_Type'Last - Count then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector, without fear of
+      --  overflow.
+
+      New_Length := Old_Length + Count;
+
+      --  The second constraint is that the new Last index value cannot exceed
+      --  Index_Type'Last. In each branch below, we calculate the maximum
+      --  length (computed from the range of values in Index_Type), and then
+      --  compare the new length to the maximum length. If the new length is
+      --  acceptable, then we compute the new last index from that.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We have to handle the case when there might be more values in the
+         --  range of Index_Type than in the range of Count_Type.
 
-      begin
-         if Old_Last_As_Int > Int'Last - N then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+         if Index_Type'First <= 0 then
+            --  We know that No_Index (the same as Index_Type'First - 1) is
+            --  less than 0, so it is safe to compute the following sum without
+            --  fear of overflow.
+
+            Index := No_Index + Index_Type'Base (Count_Type'Last);
+
+            if Index <= Index_Type'Last then
+               --  We have determined that range of Index_Type has at least as
+               --  many values as in Count_Type, so Count_Type'Last is the
+               --  maximum number of items that are allowed.
 
-         New_Last_As_Int := Old_Last_As_Int + N;
+               Max_Length := Count_Type'Last;
 
-         if New_Last_As_Int > Int (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
+            else
+               --  The range of Index_Type has fewer values than in Count_Type,
+               --  so the maximum number of items is computed from the range of
+               --  the Index_Type.
+
+               Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
+            end if;
+
+         else
+            --  No_Index is equal or greater than 0, so we can safely compute
+            --  the difference without fear of overflow (which we would have to
+            --  worry about if No_Index were less than 0, but that case is
+            --  handled above).
+
+            Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
          end if;
 
-         New_Length := UInt (New_Last_As_Int - First + 1);
+      elsif Index_Type'First <= 0 then
+         --  We know that No_Index (the same as Index_Type'First - 1) is less
+         --  than 0, so it is safe to compute the following sum without fear of
+         --  overflow.
 
-         if New_Length > Max_Length then
-            raise Constraint_Error with "new length is out of range";
+         J := Count_Type'Base (No_Index) + Count_Type'Last;
+
+         if J <= Count_Type'Base (Index_Type'Last) then
+            --  We have determined that range of Index_Type has at least as
+            --  many values as in Count_Type, so Count_Type'Last is the maximum
+            --  number of items that are allowed.
+
+            Max_Length := Count_Type'Last;
+
+         else
+            --  The range of Index_Type has fewer values than Count_Type does,
+            --  so the maximum number of items is computed from the range of
+            --  the Index_Type.
+
+            Max_Length :=
+              Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
          end if;
 
-         New_Last := Index_Type (New_Last_As_Int);
-      end;
+      else
+         --  No_Index is equal or greater than 0, so we can safely compute the
+         --  difference without fear of overflow (which we would have to worry
+         --  about if No_Index were less than 0, but that case is handled
+         --  above).
 
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
+         Max_Length :=
+           Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
+      end if;
+
+      --  We have just computed the maximum length (number of items). We must
+      --  now compare the requested length to the maximum length, as we do not
+      --  allow a vector expand beyond the maximum (because that would create
+      --  an internal array with a last index value greater than
+      --  Index_Type'Last, with no way to index those elements).
+
+      if New_Length > Max_Length then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  New_Last is the last index value of the items in the container after
+      --  insertion.  Use the wider of Index_Type'Base and Count_Type'Base to
+      --  compute its value from the New_Length.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := No_Index + Index_Type'Base (New_Length);
+
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
       end if;
 
       if Container.Elements = null then
+         pragma Assert (Container.Last = No_Index);
+
+         --  This is the simplest case, with which we must always begin: we're
+         --  inserting items into an empty vector that hasn't allocated an
+         --  internal array yet. Note that we don't need to check the busy bit
+         --  here, because an empty container cannot be busy.
+
+         --  In an indefinite vector, elements are allocated individually, and
+         --  stored as access values on the internal array (the length of which
+         --  represents the vector "capacity"), which is separately allocated.
+
          Container.Elements := new Elements_Type (New_Last);
-         Container.Last := No_Index;
 
-         for J in Container.Elements.EA'Range loop
-            Container.Elements.EA (J) := new Element_Type'(New_Item);
-            Container.Last := J;
+         --  The element backbone has been successfully allocated, so now we
+         --  allocate the elements.
+
+         for Idx in Container.Elements.EA'Range loop
+            --  In order to preserve container invariants, we always attempt
+            --  the element allocation first, before setting the Last index
+            --  value, in case the allocation fails (either because there is no
+            --  storage available, or because element initialization fails).
+
+            Container.Elements.EA (Idx) := new Element_Type'(New_Item);
+
+            --  The allocation of the element succeeded, so it is now safe to
+            --  update the Last index, restoring container invariants.
+
+            Container.Last := Idx;
          end loop;
 
          return;
       end if;
 
-      if New_Last <= Container.Elements.Last then
+      --  The tampering bits exist to prevent an item from being harmfully
+      --  manipulated while it is being visited. Query, Update, and Iterate
+      --  increment the busy count on entry, and decrement the count on
+      --  exit. Insert checks the count to determine whether it is being called
+      --  while the associated callback procedure is executing.
+
+      if Container.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with elements (vector is busy)";
+      end if;
+
+      if New_Length <= Container.Elements.EA'Length then
+         --  In this case, we're inserting elements into a vector that has
+         --  already allocated an internal array, and the existing array has
+         --  enough unused storage for the new items.
+
          declare
             E : Elements_Array renames Container.Elements.EA;
+            K : Index_Type'Base;
 
          begin
-            if Before <= Container.Last then
-               declare
-                  Index_As_Int : constant Int'Base :=
-                                   Index_Type'Pos (Before) + N;
+            if Before > Container.Last then
+               --  The new items are being appended to the vector, so no
+               --  sliding of existing elements is required.
+
+               for Idx in Before .. New_Last loop
+                  --  In order to preserve container invariants, we always
+                  --  attempt the element allocation first, before setting the
+                  --  Last index value, in case the allocation fails (either
+                  --  because there is no storage available, or because element
+                  --  initialization fails).
+
+                  E (Idx) := new Element_Type'(New_Item);
 
-                  Index : constant Index_Type := Index_Type (Index_As_Int);
+                  --  The allocation of the element succeeded, so it is now
+                  --  safe to update the Last index, restoring container
+                  --  invariants.
 
-                  J : Index_Type'Base;
+                  Container.Last := Idx;
+               end loop;
+
+            else
+               --  The new items are being inserted before some existing
+               --  elements, so we must slide the existing elements up to their
+               --  new home. We use the wider of Index_Type'Base and
+               --  Count_Type'Base as the type for intermediate index values.
 
+               if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+                  Index := Before + Index_Type'Base (Count);
+
+               else
+                  Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+               end if;
+
+               --  The new items are being inserted in the middle of the array,
+               --  in the range [Before, Index). Copy the existing elements to
+               --  the end of the array, to make room for the new items.
+
+               E (Index .. New_Last) := E (Before .. Container.Last);
+               Container.Last := New_Last;
+
+               --  We have copied the existing items up to the end of the
+               --  array, to make room for the new items in the middle of
+               --  the array.  Now we actually allocate the new items.
+
+               --  Note: initialize K outside loop to make it clear that
+               --  K always has a value if the exception handler triggers.
+
+               K := Before;
                begin
-                  --  The new items are being inserted in the middle of the
-                  --  array, in the range [Before, Index). Copy the existing
-                  --  elements to the end of the array, to make room for the
-                  --  new items.
-
-                  E (Index .. New_Last) := E (Before .. Container.Last);
-                  Container.Last := New_Last;
-
-                  --  We have copied the existing items up to the end of the
-                  --  array, to make room for the new items in the middle of
-                  --  the array.  Now we actually allocate the new items.
-
-                  --  Note: initialize J outside loop to make it clear that
-                  --  J always has a value if the exception handler triggers.
-
-                  J := Before;
-                  begin
-                     while J < Index loop
-                        E (J) := new Element_Type'(New_Item);
-                        J := J + 1;
-                     end loop;
+                  while K < Index loop
+                     E (K) := new Element_Type'(New_Item);
+                     K := K + 1;
+                  end loop;
 
-                  exception
-                     when others =>
+               exception
+                  when others =>
 
-                        --  Values in the range [Before, J) were successfully
-                        --  allocated, but values in the range [J, Index) are
-                        --  stale (these array positions contain copies of the
-                        --  old items, that did not get assigned a new item,
-                        --  because the allocation failed). We must finish what
-                        --  we started by clearing out all of the stale values,
-                        --  leaving a "hole" in the middle of the array.
-
-                        E (J .. Index - 1) := (others => null);
-                        raise;
-                  end;
-               end;
+                     --  Values in the range [Before, K) were successfully
+                     --  allocated, but values in the range [K, Index) are
+                     --  stale (these array positions contain copies of the
+                     --  old items, that did not get assigned a new item,
+                     --  because the allocation failed). We must finish what
+                     --  we started by clearing out all of the stale values,
+                     --  leaving a "hole" in the middle of the array.
 
-            else
-               for J in Before .. New_Last loop
-                  E (J) := new Element_Type'(New_Item);
-                  Container.Last := J;
-               end loop;
+                     E (K .. Index - 1) := (others => null);
+                     raise;
+               end;
             end if;
          end;
 
          return;
       end if;
 
-      --  There follows LOTS of code completely devoid of comments ???
-      --  This is not our general style ???
-
-      declare
-         C, CC : UInt;
+      --  In this case, we're inserting elements into a vector that has already
+      --  allocated an internal array, but the existing array does not have
+      --  enough storage, so we must allocate a new, longer array. In order to
+      --  guarantee that the amortized insertion cost is O(1), we always
+      --  allocate an array whose length is some power-of-two factor of the
+      --  current array length. (The new array cannot have a length less than
+      --  the New_Length of the container, but its last index value cannot be
+      --  greater than Index_Type'Last.)
+
+      New_Capacity := Count_Type'Max (1, Container.Elements.EA'Length);
+      while New_Capacity < New_Length loop
+         if New_Capacity > Count_Type'Last / 2 then
+            New_Capacity := Count_Type'Last;
+            exit;
+         end if;
 
-      begin
-         C := UInt'Max (1, Container.Elements.EA'Length);  -- ???
-         while C < New_Length loop
-            if C > UInt'Last / 2 then
-               C := UInt'Last;
-               exit;
-            end if;
+         New_Capacity := 2 * New_Capacity;
+      end loop;
 
-            C := 2 * C;
-         end loop;
+      if New_Capacity > Max_Length then
+         --  We have reached the limit of capacity, so no further expansion
+         --  will occur. (This is not a problem, as there is never a need to
+         --  have more capacity than the maximum container length.)
 
-         if C > Max_Length then
-            C := Max_Length;
-         end if;
+         New_Capacity := Max_Length;
+      end if;
 
-         if Index_Type'First <= 0
-           and then Index_Type'Last >= 0
-         then
-            CC := UInt (Index_Type'Last) + UInt (-Index_Type'First) + 1;
-         else
-            CC := UInt (Int (Index_Type'Last) - First + 1);
-         end if;
+      --  We have computed the length of the new internal array (and this is
+      --  what "vector capacity" means), so use that to compute its last index.
 
-         if C > CC then
-            C := CC;
-         end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         Dst_Last := No_Index + Index_Type'Base (New_Capacity);
 
-         declare
-            Dst_Last : constant Index_Type :=
-                         Index_Type (First + UInt'Pos (C) - Int'(1));
+      else
+         Dst_Last :=
+           Index_Type'Base (Count_Type'Base (No_Index) + New_Capacity);
+      end if;
 
-         begin
-            Dst := new Elements_Type (Dst_Last);
-         end;
-      end;
+      --  Now we allocate the new, longer internal array. If the allocation
+      --  fails, we have not changed any container state, so no side-effect
+      --  will occur as a result of propagating the exception.
 
-      if Before <= Container.Last then
-         declare
-            Index_As_Int : constant Int'Base :=
-                             Index_Type'Pos (Before) + N;
+      Dst := new Elements_Type (Dst_Last);
 
-            Index : constant Index_Type := Index_Type (Index_As_Int);
+      --  We have our new internal array. All that needs to be done now is to
+      --  copy the existing items (if any) from the old array (the "source"
+      --  array) to the new array (the "destination" array), and then
+      --  deallocate the old array.
 
-            Src : Elements_Access := Container.Elements;
+      declare
+         Src : Elements_Access := Container.Elements;
 
-         begin
-            Dst.EA (Index_Type'First .. Before - 1) :=
-              Src.EA (Index_Type'First .. Before - 1);
+      begin
+         Dst.EA (Index_Type'First .. Before - 1) :=
+           Src.EA (Index_Type'First .. Before - 1);
 
-            Dst.EA (Index .. New_Last) := Src.EA (Before .. Container.Last);
+         if Before > Container.Last then
+            --  The new items are being appended to the vector, so no
+            --  sliding of existing elements is required.
+
+            --  We have copied the elements from to the old, source array to
+            --  the new, destination array, so we can now deallocate the old
+            --  array.
 
             Container.Elements := Dst;
-            Container.Last := New_Last;
             Free (Src);
 
-            for J in Before .. Index - 1 loop
-               Dst.EA (J) := new Element_Type'(New_Item);
+            --  Now we append the new items.
+
+            for Idx in Before .. New_Last loop
+               --  In order to preserve container invariants, we always
+               --  attempt the element allocation first, before setting the
+               --  Last index value, in case the allocation fails (either
+               --  because there is no storage available, or because element
+               --  initialization fails).
+
+               Dst.EA (Idx) := new Element_Type'(New_Item);
+
+               --  The allocation of the element succeeded, so it is now safe
+               --  to update the Last index, restoring container invariants.
+
+               Container.Last := Idx;
             end loop;
-         end;
 
-      else
-         declare
-            Src : Elements_Access := Container.Elements;
+         else
+            --  The new items are being inserted before some existing elements,
+            --  so we must slide the existing elements up to their new home.
 
-         begin
-            Dst.EA (Index_Type'First .. Container.Last) :=
-              Src.EA (Index_Type'First .. Container.Last);
+            if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+               Index := Before + Index_Type'Base (Count);
+
+            else
+               Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+            end if;
+
+            Dst.EA (Index .. New_Last) := Src.EA (Before .. Container.Last);
+
+            --  We have copied the elements from to the old, source array to
+            --  the new, destination array, so we can now deallocate the old
+            --  array.
 
             Container.Elements := Dst;
+            Container.Last := New_Last;
             Free (Src);
 
-            for J in Before .. New_Last loop
-               Dst.EA (J) := new Element_Type'(New_Item);
-               Container.Last := J;
+            --  The new array has a range in the middle containing null access
+            --  values. We now fill in that partion of the array with the new
+            --  items.
+
+            for Idx in Before .. Index - 1 loop
+               --  Note that container invariants have already been satisfied
+               --  (in particular, the Last index value of the vector has
+               --  already been updated), so if this allocation fails we simply
+               --  let it propagate.
+
+               Dst.EA (Idx) := new Element_Type'(New_Item);
             end loop;
-         end;
-      end if;
+         end if;
+      end;
    end Insert;
 
    procedure Insert
@@ -1295,96 +1705,147 @@ package body Ada.Containers.Indefinite_V
       New_Item  : Vector)
    is
       N : constant Count_Type := Length (New_Item);
+      J : Index_Type'Base;
 
    begin
-      if Before < Index_Type'First then
-         raise Constraint_Error with
-           "Before index is out of range (too small)";
-      end if;
+      --  Use Insert_Space to create the "hole" (the destination slice) into
+      --  which we copy the source items.
 
-      if Before > Container.Last
-        and then Before > Container.Last + 1
-      then
-         raise Constraint_Error with
-           "Before index is out of range (too large)";
-      end if;
+      Insert_Space (Container, Before, Count => N);
 
       if N = 0 then
+         --  There's nothing else to do here (vetting of parameters was
+         --  performed already in Insert_Space), so we simply return.
+
+         return;
+      end if;
+
+      if Container'Address /= New_Item'Address then
+         --  This is the simple case.  New_Item denotes an object different
+         --  from Container, so there's nothing special we need to do to copy
+         --  the source items to their destination, because all of the source
+         --  items are contiguous.
+
+         declare
+            subtype Src_Index_Subtype is Index_Type'Base range
+              Index_Type'First .. New_Item.Last;
+
+            Src : Elements_Array renames
+                    New_Item.Elements.EA (Src_Index_Subtype);
+
+            Dst : Elements_Array renames Container.Elements.EA;
+
+            Dst_Index : Index_Type'Base;
+
+         begin
+            Dst_Index := Before - 1;
+            for Src_Index in Src'Range loop
+               Dst_Index := Dst_Index + 1;
+
+               if Src (Src_Index) /= null then
+                  Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
+               end if;
+            end loop;
+         end;
+
          return;
       end if;
 
-      Insert_Space (Container, Before, Count => N);
+      --  New_Item denotes the same object as Container, so an insertion has
+      --  potentially split the source items.  The first source slice is
+      --  [Index_Type'First, Before), and the second source slice is
+      --  [J, Container.Last], where index value J is the first index of the
+      --  second slice. (J gets computed below, but only after we have
+      --  determined that the second source slice is non-empty.) The
+      --  destination slice is always the range [Before, J). We perform the
+      --  copy in two steps, using each of the two slices of the source items.
 
       declare
-         Dst_Last_As_Int : constant Int'Base :=
-                             Int'Base (Before) + Int'Base (N) - 1;
+         L : constant Index_Type'Base := Before - 1;
+
+         subtype Src_Index_Subtype is Index_Type'Base range
+           Index_Type'First .. L;
 
-         Dst_Last : constant Index_Type := Index_Type (Dst_Last_As_Int);
+         Src : Elements_Array renames
+                 Container.Elements.EA (Src_Index_Subtype);
 
-         Dst : Elements_Array renames
-                 Container.Elements.EA (Before .. Dst_Last);
+         Dst : Elements_Array renames Container.Elements.EA;
 
-         Dst_Index : Index_Type'Base := Before - 1;
+         Dst_Index : Index_Type'Base;
 
       begin
-         if Container'Address /= New_Item'Address then
-            declare
-               subtype Src_Index_Subtype is Index_Type'Base range
-                 Index_Type'First .. New_Item.Last;
+         --  We first copy the source items that precede the space we
+         --  inserted. (If Before equals Index_Type'First, then this first
+         --  source slice will be empty, which is harmless.)
 
-               Src : Elements_Array renames
-                       New_Item.Elements.EA (Src_Index_Subtype);
+         Dst_Index := Before - 1;
+         for Src_Index in Src'Range loop
+            Dst_Index := Dst_Index + 1;
 
-            begin
-               for Src_Index in Src'Range loop
-                  Dst_Index := Dst_Index + 1;
+            if Src (Src_Index) /= null then
+               Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
+            end if;
+         end loop;
 
-                  if Src (Src_Index) /= null then
-                     Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
-                  end if;
-               end loop;
-            end;
+         if Src'Length = N then
+            --  The new items were effectively appended to the container, so we
+            --  have already copied all of the items that need to be copied.
+            --  We return early here, even though the source slice below is
+            --  empty (so the assignment would be harmless), because we want to
+            --  avoid computing J, which will overflow if J is greater than
+            --  Index_Type'Base'Last.
 
             return;
          end if;
+      end;
 
-         declare
-            subtype Src_Index_Subtype is Index_Type'Base range
-              Index_Type'First .. Before - 1;
+      --  Index value J is the first index of the second source slice. (It is
+      --  also 1 greater than the last index of the destination slice.) Note
+      --  that we want to avoid computing J, if J is greater than
+      --  Index_Type'Base'Last, in order to avoid overflow. We prevent that by
+      --  returning early above, immediately after copying the first slice of
+      --  the source, and determining that this second slice of the source is
+      --  empty.
 
-            Src : Elements_Array renames
-                    Container.Elements.EA (Src_Index_Subtype);
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         J := Before + Index_Type'Base (N);
 
-         begin
-            for Src_Index in Src'Range loop
-               Dst_Index := Dst_Index + 1;
+      else
+         J := Index_Type'Base (Count_Type'Base (Before) + N);
+      end if;
 
-               if Src (Src_Index) /= null then
-                  Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
-               end if;
-            end loop;
-         end;
+      declare
+         subtype Src_Index_Subtype is Index_Type'Base range
+           J .. Container.Last;
 
-         if Dst_Last = Container.Last then
-            return;
-         end if;
+         Src : Elements_Array renames
+                 Container.Elements.EA (Src_Index_Subtype);
 
-         declare
-            subtype Src_Index_Subtype is Index_Type'Base range
-              Dst_Last + 1 .. Container.Last;
+         Dst : Elements_Array renames Container.Elements.EA;
 
-            Src : Elements_Array renames
-                    Container.Elements.EA (Src_Index_Subtype);
+         Dst_Index : Index_Type'Base;
 
-         begin
-            for Src_Index in Src'Range loop
-               Dst_Index := Dst_Index + 1;
+      begin
+         --  We next copy the source items that follow the space we
+         --  inserted. Index value Dst_Index is the first index of that portion
+         --  of the destination that receives this slice of the source. (For
+         --  the reasons given above, this slice is guaranteed to be
+         --  non-empty.)
 
-               if Src (Src_Index) /= null then
-                  Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
-               end if;
-            end loop;
-         end;
+         if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+            Dst_Index := J - Index_Type'Base (Src'Length);
+
+         else
+            Dst_Index := Index_Type'Base (Count_Type'Base (J) - Src'Length);
+         end if;
+
+         for Src_Index in Src'Range loop
+            if Src (Src_Index) /= null then
+               Dst (Dst_Index) := new Element_Type'(Src (Src_Index).all);
+            end if;
+
+            Dst_Index := Dst_Index + 1;
+         end loop;
       end;
    end Insert;
 
@@ -1561,22 +2022,42 @@ package body Ada.Containers.Indefinite_V
       Before    : Extended_Index;
       Count     : Count_Type := 1)
    is
-      N               : constant Int := Int (Count);
+      Old_Length : constant Count_Type := Container.Length;
 
-      First           : constant Int := Int (Index_Type'First);
-      New_Last_As_Int : Int'Base;
-      New_Last        : Index_Type;
-      New_Length      : UInt;
-      Max_Length      : constant UInt := UInt (Count_Type'Last);
+      Max_Length : Count_Type'Base;  -- determined from range of Index_Type
+      New_Length : Count_Type'Base;  -- sum of current length and Count
+      New_Last   : Index_Type'Base;  -- last index of vector after insertion
+
+      Index : Index_Type'Base;  -- scratch for intermediate values
+      J     : Count_Type'Base;  -- scratch
+
+      New_Capacity : Count_Type'Base;  -- length of new, expanded array
+      Dst_Last     : Index_Type'Base;  -- last index of new, expanded array
+      Dst          : Elements_Access;  -- new, expanded internal array
+
+   begin
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying where the new
+      --  items should be inserted, so we must manually check. (That the user
+      --  is allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
 
-      Dst             : Elements_Access;
-
-   begin
       if Before < Index_Type'First then
          raise Constraint_Error with
            "Before index is out of range (too small)";
       end if;
 
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows for the
+      --  case of appending items to the back end of the vector. (It is assumed
+      --  that specifying an index value greater than Last + 1 indicates some
+      --  deeper flaw in the caller's algorithm, so that case is treated as a
+      --  proper error.)
+
       if Before > Container.Last
         and then Before > Container.Last + 1
       then
@@ -1584,60 +2065,178 @@ package body Ada.Containers.Indefinite_V
            "Before index is out of range (too large)";
       end if;
 
+      --  We treat inserting 0 items into the container as a no-op, even when
+      --  the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
-      declare
-         Old_Last_As_Int : constant Int := Int (Container.Last);
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the current length and the insertion
+      --  count. Note that we cannot simply add these values, because of the
+      --  possibilty of overflow.
+
+      if Old_Length > Count_Type'Last - Count then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector, without fear of
+      --  overflow.
+
+      New_Length := Old_Length + Count;
+
+      --  The second constraint is that the new Last index value cannot exceed
+      --  Index_Type'Last. In each branch below, we calculate the maximum
+      --  length (computed from the range of values in Index_Type), and then
+      --  compare the new length to the maximum length. If the new length is
+      --  acceptable, then we compute the new last index from that.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We have to handle the case when there might be more values in the
+         --  range of Index_Type than in the range of Count_Type.
 
-      begin
-         if Old_Last_As_Int > Int'Last - N then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+         if Index_Type'First <= 0 then
+            --  We know that No_Index (the same as Index_Type'First - 1) is
+            --  less than 0, so it is safe to compute the following sum without
+            --  fear of overflow.
+
+            Index := No_Index + Index_Type'Base (Count_Type'Last);
+
+            if Index <= Index_Type'Last then
+               --  We have determined that range of Index_Type has at least as
+               --  many values as in Count_Type, so Count_Type'Last is the
+               --  maximum number of items that are allowed.
 
-         New_Last_As_Int := Old_Last_As_Int + N;
+               Max_Length := Count_Type'Last;
 
-         if New_Last_As_Int > Int (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
+            else
+               --  The range of Index_Type has fewer values than in Count_Type,
+               --  so the maximum number of items is computed from the range of
+               --  the Index_Type.
+
+               Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
+            end if;
+
+         else
+            --  No_Index is equal or greater than 0, so we can safely compute
+            --  the difference without fear of overflow (which we would have to
+            --  worry about if No_Index were less than 0, but that case is
+            --  handled above).
+
+            Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
          end if;
 
-         New_Length := UInt (New_Last_As_Int - First + 1);
+      elsif Index_Type'First <= 0 then
+         --  We know that No_Index (the same as Index_Type'First - 1) is less
+         --  than 0, so it is safe to compute the following sum without fear of
+         --  overflow.
 
-         if New_Length > Max_Length then
-            raise Constraint_Error with "new length is out of range";
+         J := Count_Type'Base (No_Index) + Count_Type'Last;
+
+         if J <= Count_Type'Base (Index_Type'Last) then
+            --  We have determined that range of Index_Type has at least as
+            --  many values as in Count_Type, so Count_Type'Last is the maximum
+            --  number of items that are allowed.
+
+            Max_Length := Count_Type'Last;
+
+         else
+            --  The range of Index_Type has fewer values than Count_Type does,
+            --  so the maximum number of items is computed from the range of
+            --  the Index_Type.
+
+            Max_Length :=
+              Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
          end if;
 
-         New_Last := Index_Type (New_Last_As_Int);
-      end;
+      else
+         --  No_Index is equal or greater than 0, so we can safely compute the
+         --  difference without fear of overflow (which we would have to worry
+         --  about if No_Index were less than 0, but that case is handled
+         --  above).
 
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
+         Max_Length :=
+           Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
+      end if;
+
+      --  We have just computed the maximum length (number of items). We must
+      --  now compare the requested length to the maximum length, as we do not
+      --  allow a vector expand beyond the maximum (because that would create
+      --  an internal array with a last index value greater than
+      --  Index_Type'Last, with no way to index those elements).
+
+      if New_Length > Max_Length then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  New_Last is the last index value of the items in the container after
+      --  insertion.  Use the wider of Index_Type'Base and Count_Type'Base to
+      --  compute its value from the New_Length.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := No_Index + Index_Type'Base (New_Length);
+
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
       end if;
 
       if Container.Elements = null then
+         pragma Assert (Container.Last = No_Index);
+
+         --  This is the simplest case, with which we must always begin: we're
+         --  inserting items into an empty vector that hasn't allocated an
+         --  internal array yet. Note that we don't need to check the busy bit
+         --  here, because an empty container cannot be busy.
+
+         --  In an indefinite vector, elements are allocated individually, and
+         --  stored as access values on the internal array (the length of which
+         --  represents the vector "capacity"), which is separately
+         --  allocated. We have no elements here (because we're inserting
+         --  "space"), so all we need to do is allocate the backbone.
+
          Container.Elements := new Elements_Type (New_Last);
          Container.Last := New_Last;
+
          return;
       end if;
 
-      if New_Last <= Container.Elements.Last then
+      --  The tampering bits exist to prevent an item from being harmfully
+      --  manipulated while it is being visited. Query, Update, and Iterate
+      --  increment the busy count on entry, and decrement the count on
+      --  exit. Insert checks the count to determine whether it is being called
+      --  while the associated callback procedure is executing.
+
+      if Container.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with elements (vector is busy)";
+      end if;
+
+      if New_Length <= Container.Elements.EA'Length then
+         --  In this case, we're inserting elements into a vector that has
+         --  already allocated an internal array, and the existing array has
+         --  enough unused storage for the new items.
+
          declare
             E : Elements_Array renames Container.Elements.EA;
 
          begin
             if Before <= Container.Last then
-               declare
-                  Index_As_Int : constant Int'Base :=
-                                   Index_Type'Pos (Before) + N;
+               --  The new space is being inserted before some existing
+               --  elements, so we must slide the existing elements up to their
+               --  new home. We use the wider of Index_Type'Base and
+               --  Count_Type'Base as the type for intermediate index values.
 
-                  Index : constant Index_Type := Index_Type (Index_As_Int);
+               if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+                  Index := Before + Index_Type'Base (Count);
 
-               begin
-                  E (Index .. New_Last) := E (Before .. Container.Last);
-                  E (Before .. Index - 1) := (others => null);
-               end;
+               else
+                  Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+               end if;
+
+               E (Index .. New_Last) := E (Before .. Container.Last);
+               E (Before .. Index - 1) := (others => null);
             end if;
          end;
 
@@ -1645,68 +2244,80 @@ package body Ada.Containers.Indefinite_V
          return;
       end if;
 
-      declare
-         C, CC : UInt;
+      --  In this case, we're inserting elements into a vector that has already
+      --  allocated an internal array, but the existing array does not have
+      --  enough storage, so we must allocate a new, longer array. In order to
+      --  guarantee that the amortized insertion cost is O(1), we always
+      --  allocate an array whose length is some power-of-two factor of the
+      --  current array length. (The new array cannot have a length less than
+      --  the New_Length of the container, but its last index value cannot be
+      --  greater than Index_Type'Last.)
+
+      New_Capacity := Count_Type'Max (1, Container.Elements.EA'Length);
+      while New_Capacity < New_Length loop
+         if New_Capacity > Count_Type'Last / 2 then
+            New_Capacity := Count_Type'Last;
+            exit;
+         end if;
 
-      begin
-         C := UInt'Max (1, Container.Elements.EA'Length);  -- ???
-         while C < New_Length loop
-            if C > UInt'Last / 2 then
-               C := UInt'Last;
-               exit;
-            end if;
+         New_Capacity := 2 * New_Capacity;
+      end loop;
 
-            C := 2 * C;
-         end loop;
+      if New_Capacity > Max_Length then
+         --  We have reached the limit of capacity, so no further expansion
+         --  will occur. (This is not a problem, as there is never a need to
+         --  have more capacity than the maximum container length.)
 
-         if C > Max_Length then
-            C := Max_Length;
-         end if;
+         New_Capacity := Max_Length;
+      end if;
 
-         if Index_Type'First <= 0
-           and then Index_Type'Last >= 0
-         then
-            CC := UInt (Index_Type'Last) + UInt (-Index_Type'First) + 1;
-         else
-            CC := UInt (Int (Index_Type'Last) - First + 1);
-         end if;
+      --  We have computed the length of the new internal array (and this is
+      --  what "vector capacity" means), so use that to compute its last index.
 
-         if C > CC then
-            C := CC;
-         end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         Dst_Last := No_Index + Index_Type'Base (New_Capacity);
 
-         declare
-            Dst_Last : constant Index_Type :=
-                         Index_Type (First + UInt'Pos (C) - 1);
+      else
+         Dst_Last :=
+           Index_Type'Base (Count_Type'Base (No_Index) + New_Capacity);
+      end if;
 
-         begin
-            Dst := new Elements_Type (Dst_Last);
-         end;
-      end;
+      --  Now we allocate the new, longer internal array. If the allocation
+      --  fails, we have not changed any container state, so no side-effect
+      --  will occur as a result of propagating the exception.
+
+      Dst := new Elements_Type (Dst_Last);
+
+      --  We have our new internal array. All that needs to be done now is to
+      --  copy the existing items (if any) from the old array (the "source"
+      --  array) to the new array (the "destination" array), and then
+      --  deallocate the old array.
 
       declare
          Src : Elements_Access := Container.Elements;
 
       begin
-         if Before <= Container.Last then
-            declare
-               Index_As_Int : constant Int'Base :=
-                                Index_Type'Pos (Before) + N;
+         Dst.EA (Index_Type'First .. Before - 1) :=
+           Src.EA (Index_Type'First .. Before - 1);
 
-               Index : constant Index_Type := Index_Type (Index_As_Int);
+         if Before <= Container.Last then
+            --  The new items are being inserted before some existing elements,
+            --  so we must slide the existing elements up to their new home.
 
-            begin
-               Dst.EA (Index_Type'First .. Before - 1) :=
-                 Src.EA (Index_Type'First .. Before - 1);
+            if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+               Index := Before + Index_Type'Base (Count);
 
-               Dst.EA (Index .. New_Last) := Src.EA (Before .. Container.Last);
-            end;
+            else
+               Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+            end if;
 
-         else
-            Dst.EA (Index_Type'First .. Container.Last) :=
-              Src.EA (Index_Type'First .. Container.Last);
+            Dst.EA (Index .. New_Last) := Src.EA (Before .. Container.Last);
          end if;
 
+         --  We have copied the elements from to the old, source array to the
+         --  new, destination array, so we can now restore invariants, and
+         --  deallocate the old array.
+
          Container.Elements := Dst;
          Container.Last := New_Last;
          Free (Src);
@@ -1808,7 +2419,7 @@ package body Ada.Containers.Indefinite_V
       return (Container'Unchecked_Access, Container.Last);
    end Last;
 
-   ------------------
+   -----------------
    -- Last_Element --
    ------------------
 
@@ -1845,12 +2456,33 @@ package body Ada.Containers.Indefinite_V
    ------------
 
    function Length (Container : Vector) return Count_Type is
-      L : constant Int := Int (Container.Last);
-      F : constant Int := Int (Index_Type'First);
-      N : constant Int'Base := L - F + 1;
+      L : constant Index_Type'Base := Container.Last;
+      F : constant Index_Type := Index_Type'First;
 
    begin
-      return Count_Type (N);
+      --  The base range of the index type (Index_Type'Base) might not include
+      --  all values for length (Count_Type). Contrariwise, the index type
+      --  might include values outside the range of length.  Hence we use
+      --  whatever type is wider for intermediate values when calculating
+      --  length. Note that no matter what the index type is, the maximum
+      --  length to which a vector is allowed to grow is always the minimum
+      --  of Count_Type'Last and (IT'Last - IT'First + 1).
+
+      --  For example, an Index_Type with range -127 .. 127 is only guaranteed
+      --  to have a base range of -128 .. 127, but the corresponding vector
+      --  would have lengths in the range 0 .. 255. In this case we would need
+      --  to use Count_Type'Base for intermediate values.
+
+      --  Another case would be the index range -2**63 + 1 .. -2**63 + 10. The
+      --  vector would have a maximum length of 10, but the index values lie
+      --  outside the range of Count_Type (which is only 32 bits). In this
+      --  case we would need to use Index_Type'Base for intermediate values.
+
+      if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then
+         return Count_Type'Base (L) - Count_Type'Base (F) + 1;
+      else
+         return Count_Type (L - F + 1);
+      end if;
    end Length;
 
    ----------
@@ -2131,17 +2763,53 @@ package body Ada.Containers.Indefinite_V
    is
       N : constant Count_Type := Length (Container);
 
+      Index : Count_Type'Base;
+      Last  : Index_Type'Base;
+
    begin
+      --  Reserve_Capacity can be used to either expand the storage available
+      --  for elements (this would be its typical use, in anticipation of
+      --  future insertion), or to trim back storage. In the latter case,
+      --  storage can only be trimmed back to the limit of the container
+      --  length. Note that Reserve_Capacity neither deletes (active) elements
+      --  nor inserts elements; it only affects container capacity, never
+      --  container length.
+
       if Capacity = 0 then
+         --  This is a request to trim back storage, to the minimum amount
+         --  possible given the current state of the container.
+
          if N = 0 then
+            --  The container is empty, so in this unique case we can
+            --  deallocate the entire internal array. Note that an empty
+            --  container can never be busy, so there's no need to check the
+            --  tampering bits.
+
             declare
                X : Elements_Access := Container.Elements;
             begin
+               --  First we remove the internal array from the container, to
+               --  handle the case when the deallocation raises an exception
+               --  (although that's unlikely, since this is simply an array of
+               --  access values, all of which are null).
+
                Container.Elements := null;
+
+               --  Container invariants have been restored, so it is now safe
+               --  to attempt to deallocate the internal array.
+
                Free (X);
             end;
 
          elsif N < Container.Elements.EA'Length then
+            --  The container is not empty, and the current length is less than
+            --  the current capacity, so there's storage available to trim. In
+            --  this case, we allocate a new internal array having a length
+            --  that exactly matches the number of items in the
+            --  container. (Reserve_Capacity does not delete active elements,
+            --  so this is the best we can do with respect to minimizing
+            --  storage).
+
             if Container.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with elements (vector is busy)";
@@ -2157,7 +2825,19 @@ package body Ada.Containers.Indefinite_V
                X : Elements_Access := Container.Elements;
 
             begin
+               --  Although we have isolated the old internal array that we're
+               --  going to deallocate, we don't deallocate it until we have
+               --  successfully allocated a new one. If there is an exception
+               --  during allocation (because there is not enough storage), we
+               --  let it propagate without causing any side-effect.
+
                Container.Elements := new Elements_Type'(Container.Last, Src);
+
+               --  We have succesfully allocated a new internal array (with a
+               --  smaller length than the old one, and containing a copy of
+               --  just the active elements in the container), so we can
+               --  deallocate the old array.
+
                Free (X);
             end;
          end if;
@@ -2165,29 +2845,102 @@ package body Ada.Containers.Indefinite_V
          return;
       end if;
 
-      if Container.Elements = null then
-         declare
-            Last_As_Int : constant Int'Base :=
-                            Int (Index_Type'First) + Int (Capacity) - 1;
+      --  Reserve_Capacity can be used to expand the storage available for
+      --  elements, but we do not let the capacity grow beyond the number of
+      --  values in Index_Type'Range. (Were it otherwise, there would be no way
+      --  to refer to the elements with index values greater than
+      --  Index_Type'Last, so that storage would be wasted.) Here we compute
+      --  the Last index value of the new internal array, in a way that avoids
+      --  any possibility of overflow.
 
-         begin
-            if Last_As_Int > Index_Type'Pos (Index_Type'Last) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
 
-            declare
-               Last : constant Index_Type := Index_Type (Last_As_Int);
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
 
-            begin
-               Container.Elements := new Elements_Type (Last);
-            end;
-         end;
+         if Index_Type'Base'Last - Index_Type'Base (Capacity) < No_Index then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Capacity);
+
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
+
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Capacity.
+
+         Index := Count_Type'Base (No_Index) + Capacity;  -- Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
+      else
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
+
+         Index := Count_Type'Base (Index_Type'Last) - Capacity;  -- No_Index
+
+         if Index < Count_Type'Base (No_Index) then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
 
+         --  We have determined that the value of Capacity would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Capacity);
+      end if;
+
+      --  The requested capacity is non-zero, but we don't know yet whether
+      --  this is a request for expansion or contraction of storage.
+
+      if Container.Elements = null then
+         --  The container is empty (it doesn't even have an internal array),
+         --  so this represents a request to allocate storage having the given
+         --  capacity.
+
+         Container.Elements := new Elements_Type (Last);
          return;
       end if;
 
       if Capacity <= N then
+         --  This is a request to trim back storage, but only to the limit of
+         --  what's already in the container. (Reserve_Capacity never deletes
+         --  active elements, it only reclaims excess storage.)
+
          if N < Container.Elements.EA'Length then
+            --  The container is not empty (because the requested capacity is
+            --  positive, and less than or equal to the container length), and
+            --  the current length is less than the current capacity, so
+            --  there's storage available to trim. In this case, we allocate a
+            --  new internal array having a length that exactly matches the
+            --  number of items in the container.
+
             if Container.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with elements (vector is busy)";
@@ -2203,7 +2956,19 @@ package body Ada.Containers.Indefinite_V
                X : Elements_Access := Container.Elements;
 
             begin
+               --  Although we have isolated the old internal array that we're
+               --  going to deallocate, we don't deallocate it until we have
+               --  successfully allocated a new one. If there is an exception
+               --  during allocation (because there is not enough storage), we
+               --  let it propagate without causing any side-effect.
+
                Container.Elements := new Elements_Type'(Container.Last, Src);
+
+               --  We have succesfully allocated a new internal array (with a
+               --  smaller length than the old one, and containing a copy of
+               --  just the active elements in the container), so it is now
+               --  safe to deallocate the old array.
+
                Free (X);
             end;
          end if;
@@ -2211,47 +2976,57 @@ package body Ada.Containers.Indefinite_V
          return;
       end if;
 
+      --  The requested capacity is larger than the container length (the
+      --  number of active elements). Whether this represents a request for
+      --  expansion or contraction of the current capacity depends on what the
+      --  current capacity is.
+
       if Capacity = Container.Elements.EA'Length then
+         --  The requested capacity matches the existing capacity, so there's
+         --  nothing to do here. We treat this case as a no-op, and simply
+         --  return without checking the busy bit.
+
          return;
       end if;
 
+      --  There is a change in the capacity of a non-empty container, so a new
+      --  internal array will be allocated. (The length of the new internal
+      --  array could be less or greater than the old internal array. We know
+      --  only that the length of the new internal array is greater than the
+      --  number of active elements in the container.) We must check whether
+      --  the container is busy before doing anything else.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
-      declare
-         Last_As_Int : constant Int'Base :=
-                         Int (Index_Type'First) + Int (Capacity) - 1;
+      --  We now allocate a new internal array, having a length different from
+      --  its current value.
 
-      begin
-         if Last_As_Int > Index_Type'Pos (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+      declare
+         X : Elements_Access := Container.Elements;
 
-         declare
-            Last : constant Index_Type := Index_Type (Last_As_Int);
-            X    : Elements_Access := Container.Elements;
+         subtype Index_Subtype is Index_Type'Base range
+           Index_Type'First .. Container.Last;
 
-            subtype Index_Subtype is Index_Type'Base range
-              Index_Type'First .. Container.Last;
+      begin
+         --  We now allocate a new internal array, having a length different
+         --  from its current value.
 
-         begin
-            Container.Elements := new Elements_Type (Last);
+         Container.Elements := new Elements_Type (Last);
 
-            declare
-               Src : Elements_Array renames
-                       X.EA (Index_Subtype);
+         --  We have successfully allocated the new internal array, so now we
+         --  move the existing elements from the existing the old internal
+         --  array onto the new one. Note that we're just copying access
+         --  values, to this should not raise any exceptions.
 
-               Tgt : Elements_Array renames
-                       Container.Elements.EA (Index_Subtype);
+         Container.Elements.EA (Index_Subtype) := X.EA (Index_Subtype);
 
-            begin
-               Tgt := Src;
-            end;
+         --  We have moved the elements from the old interal array, so now we
+         --  can deallocate it.
 
-            Free (X);
-         end;
+         Free (X);
       end;
    end Reserve_Capacity;
 
@@ -2388,45 +3163,25 @@ package body Ada.Containers.Indefinite_V
      (Container : in out Vector;
       Length    : Count_Type)
    is
-      N : constant Count_Type := Indefinite_Vectors.Length (Container);
+      Count : constant Count_Type'Base := Container.Length - Length;
 
    begin
-      if Length = N then
-         return;
-      end if;
-
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
-      end if;
-
-      if Length < N then
-         for Index in 1 .. N - Length loop
-            declare
-               J : constant Index_Type := Container.Last;
-               X : Element_Access := Container.Elements.EA (J);
+      --  Set_Length allows the user to set the length explicitly, instead of
+      --  implicitly as a side-effect of deletion or insertion. If the
+      --  requested length is less than the current length, this is equivalent
+      --  to deleting items from the back end of the vector. If the requested
+      --  length is greater than the current length, then this is equivalent to
+      --  inserting "space" (nonce items) at the end.
 
-            begin
-               Container.Elements.EA (J) := null;
-               Container.Last := J - 1;
-               Free (X);
-            end;
-         end loop;
+      if Count >= 0 then
+         Container.Delete_Last (Count);
 
-         return;
-      end if;
+      elsif Container.Last >= Index_Type'Last then
+         raise Constraint_Error with "vector is already at its maximum length";
 
-      if Length > Capacity (Container) then
-         Reserve_Capacity (Container, Capacity => Length);
+      else
+         Container.Insert_Space (Container.Last + 1, -Count);
       end if;
-
-      declare
-         Last_As_Int : constant Int'Base :=
-                         Int (Index_Type'First) + Int (Length) - 1;
-
-      begin
-         Container.Last := Index_Type (Last_As_Int);
-      end;
    end Set_Length;
 
    ----------
@@ -2529,8 +3284,8 @@ package body Ada.Containers.Indefinite_V
    ---------------
 
    function To_Vector (Length : Count_Type) return Vector is
-      Index    : Int'Base;
-      Last     : Index_Type;
+      Index    : Count_Type'Base;
+      Last     : Index_Type'Base;
       Elements : Elements_Access;
 
    begin
@@ -2539,45 +3294,75 @@ package body Ada.Containers.Indefinite_V
       end if;
 
       --  We create a vector object with a capacity that matches the specified
-      --  Length. We do not allow the vector capacity (the length of the
+      --  Length, but we do not allow the vector capacity (the length of the
       --  internal array) to exceed the number of values in Index_Type'Range
       --  (otherwise, there would be no way to refer to those components via an
-      --  index), so we must check whether the specified Length would create a
-      --  Last index value greater than Index_Type'Last. This calculation
-      --  requires care, because overflow can occur when Index_Type'First is
-      --  near the end of the range of Int.
-
-      if Index_Type'First <= 0 then
-         --  Compute the potential Last index value in the normal way, using
-         --  Int as the type in which to perform intermediate calculations. Int
-         --  is a 64-bit type, and Count_Type is a 32-bit type, so no overflow
-         --  can occur.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+      --  index).  We must therefore check whether the specified Length would
+      --  create a Last index value greater than Index_Type'Last.
 
-         if Index > Int (Index_Type'Last) then
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (Length) < No_Index then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Length);
+
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
+
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Length.
+
+         Index := Count_Type'Base (No_Index) + Length;  -- Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
       else
-         --  If Index_Type'First is within Length of Int'Last, then overflow
-         --  would occur if we simply computed Last directly. So instead of
-         --  computing Last, and then determining whether its value is greater
-         --  than Index_Type'Last, we work backwards by computing the potential
-         --  First index value, and then checking whether that value is less
-         --  than Index_Type'First.
-         Index := Int (Index_Type'Last) - Int (Length) + 1;
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
 
-         if Index < Int (Index_Type'First) then
+         Index := Count_Type'Base (Index_Type'Last) - Length;  -- No_Index
+
+         if Index < Count_Type'Base (No_Index) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
-         --  We have determined that Length would not create a Last index value
-         --  outside of the range of Index_Type, so we can now safely compute
-         --  its value.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+         --  We have determined that the value of Length would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Length);
       end if;
 
-      Last := Index_Type (Index);
       Elements := new Elements_Type (Last);
 
       return Vector'(Controlled with Elements, Last, 0, 0);
@@ -2587,8 +3372,8 @@ package body Ada.Containers.Indefinite_V
      (New_Item : Element_Type;
       Length   : Count_Type) return Vector
    is
-      Index    : Int'Base;
-      Last     : Index_Type;
+      Index    : Count_Type'Base;
+      Last     : Index_Type'Base;
       Elements : Elements_Access;
 
    begin
@@ -2597,51 +3382,81 @@ package body Ada.Containers.Indefinite_V
       end if;
 
       --  We create a vector object with a capacity that matches the specified
-      --  Length.  We do not allow the vector capacity (the length of the
+      --  Length, but we do not allow the vector capacity (the length of the
       --  internal array) to exceed the number of values in Index_Type'Range
       --  (otherwise, there would be no way to refer to those components via an
-      --  index), so we must check whether the specified Length would create a
-      --  Last index value greater than Index_Type'Last. This calculation
-      --  requires care, because overflow can occur when Index_Type'First is
-      --  near the end of the range of Int.
-
-      if Index_Type'First <= 0 then
-         --  Compute the potential Last index value in the normal way, using
-         --  Int as the type in which to perform intermediate calculations. Int
-         --  is a 64-bit type, and Count_Type is a 32-bit type, so no overflow
-         --  can occur.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+      --  index). We must therefore check whether the specified Length would
+      --  create a Last index value greater than Index_Type'Last.
 
-         if Index > Int (Index_Type'Last) then
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (Length) < No_Index then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Length);
+
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
+
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Length.
+
+         Index := Count_Type'Base (No_Index) + Length;  -- Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
       else
-         --  If Index_Type'First is within Length of Int'Last, then overflow
-         --  would occur if we simply computed Last directly. So instead of
-         --  computing Last, and then determining whether its value is greater
-         --  than Index_Type'Last, we work backwards by computing the potential
-         --  First index value, and then checking whether that value is less
-         --  than Index_Type'First.
-         Index := Int (Index_Type'Last) - Int (Length) + 1;
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
 
-         if Index < Int (Index_Type'First) then
+         Index := Count_Type'Base (Index_Type'Last) - Length;  -- No_Index
+
+         if Index < Count_Type'Base (No_Index) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
-         --  We have determined that Length would not create a Last index value
-         --  outside of the range of Index_Type, so we can now safely compute
-         --  its value.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+         --  We have determined that the value of Length would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Length);
       end if;
 
-      Last := Index_Type (Index);
       Elements := new Elements_Type (Last);
 
       --  We use Last as the index of the loop used to populate the internal
       --  array with items. In general, we prefer to initialize the loop index
       --  immediately prior to entering the loop. However, Last is also used in
-      --  the exception handler (it reclaims elements that have been allocated,
+      --  the exception handler (to reclaim elements that have been allocated,
       --  before propagating the exception), and the initialization of Last
       --  after entering the block containing the handler confuses some static
       --  analysis tools, with respect to whether Last has been properly
Index: a-convec.adb
===================================================================
--- a-convec.adb	(revision 161073)
+++ a-convec.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2010, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -34,9 +34,6 @@ with System; use type System.Address;
 
 package body Ada.Containers.Vectors is
 
-   type Int is range System.Min_Int .. System.Max_Int;
-   type UInt is mod System.Max_Binary_Modulus;
-
    procedure Free is
      new Ada.Unchecked_Deallocation (Elements_Type, Elements_Access);
 
@@ -45,10 +42,22 @@ package body Ada.Containers.Vectors is
    ---------
 
    function "&" (Left, Right : Vector) return Vector is
-      LN : constant Count_Type := Length (Left);
-      RN : constant Count_Type := Length (Right);
+      LN   : constant Count_Type := Length (Left);
+      RN   : constant Count_Type := Length (Right);
+      N    : Count_Type'Base;  -- length of result
+      J    : Count_Type'Base;  -- for computing intermediate index values
+      Last : Index_Type'Base;  -- Last index of result
 
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the vector parameters. We could decide to make it larger, but we
+      --  have no basis for knowing how much larger, so we just allocate the
+      --  minimum amount of storage.
+
+      --  Here we handle the easy cases first, when one of the vector
+      --  parameters is empty. (We say "easy" because there's nothing to
+      --  compute, that can potentially overflow.)
+
       if LN = 0 then
          if RN = 0 then
             return Empty_Vector;
@@ -80,82 +89,116 @@ package body Ada.Containers.Vectors is
 
       end if;
 
-      declare
-         N : constant Int'Base := Int (LN) + Int (RN);
-         J : Int'Base;
+      --  Neither of the vector parameters is empty, so must compute the length
+      --  of the result vector and its last index. (This is the harder case,
+      --  because our computations must avoid overflow.)
+
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the combined lengths. Note that we cannot
+      --  simply add the lengths, because of the possibilty of overflow.
 
-      begin
-         --  There are two constraints we need to satisfy. The first constraint
-         --  is that a container cannot have more than Count_Type'Last
-         --  elements, so we must check the sum of the combined lengths. (It
-         --  would be rare for vectors to have such a large number of elements,
-         --  so we would normally expect this first check to succeed.) The
-         --  second constraint is that the new Last index value cannot exceed
-         --  Index_Type'Last.
+      if LN > Count_Type'Last - RN then
+         raise Constraint_Error with "new length is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector, without fear of
+      --  overflow.
 
-         if N > Count_Type'Pos (Count_Type'Last) then
+      N := LN + RN;
+
+      --  The second constraint is that the new Last index value cannot
+      --  exceed Index_Type'Last. We use the wider of Index_Type'Base and
+      --  Count_Type'Base as the type for intermediate values.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (N) < No_Index then
             raise Constraint_Error with "new length is out of range";
          end if;
 
-         --  We now check whether the new length would create a Last index
-         --  value greater than Index_Type'Last. This calculation requires
-         --  care, because overflow can occur when Index_Type'First is near the
-         --  end of the range of Int.
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
 
-         if Index_Type'First <= 0 then
+         Last := No_Index + Index_Type'Base (N);
 
-            --  Compute the potential Last index value in the normal way, using
-            --  Int as the type in which to perform intermediate
-            --  calculations. Int is a 64-bit type, and Count_Type is a 32-bit
-            --  type, so no overflow can occur.
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
 
-            J := Int (Index_Type'First - 1) + N;
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "new length is out of range";
+         end if;
 
-            if J > Int (Index_Type'Last) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of length.
 
-         else
-            --  If Index_Type'First is within N of Int'Last, then overflow
-            --  would occur if we simply computed Last directly. So instead of
-            --  computing Last, and then determining whether its value is
-            --  greater than Index_Type'Last (as we do above), we work
-            --  backwards by computing the potential First index value, and
-            --  then checking whether that value is less than Index_Type'First.
+         J := Count_Type'Base (No_Index) + N;  -- Last
 
-            J := Int (Index_Type'Last) - N + 1;
+         if J > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "new length is out of range";
+         end if;
 
-            if J < Int (Index_Type'First) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (J);
+
+      else
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
 
-            --  We have determined that Length would not create a Last index
-            --  value outside of the range of Index_Type, so we can now safely
-            --  compute its value.
+         J := Count_Type'Base (Index_Type'Last) - N;  -- No_Index
 
-            J := Int (Index_Type'First - 1) + N;
+         if J < Count_Type'Base (No_Index) then
+            raise Constraint_Error with "new length is out of range";
          end if;
 
-         declare
-            Last : constant Index_Type := Index_Type (J);
+         --  We have determined that the result length would not create a Last
+         --  index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
 
-            LE : Elements_Array renames
-                   Left.Elements.EA (Index_Type'First .. Left.Last);
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + N);
+      end if;
 
-            RE : Elements_Array renames
-                   Right.Elements.EA (Index_Type'First .. Right.Last);
+      declare
+         LE : Elements_Array renames
+                Left.Elements.EA (Index_Type'First .. Left.Last);
 
-            Elements : constant Elements_Access :=
-                         new Elements_Type'(Last, LE & RE);
+         RE : Elements_Array renames
+                Right.Elements.EA (Index_Type'First .. Right.Last);
 
-         begin
-            return (Controlled with Elements, Last, 0, 0);
-         end;
+         Elements : constant Elements_Access :=
+                      new Elements_Type'(Last, LE & RE);
+
+      begin
+         return (Controlled with Elements, Last, 0, 0);
       end;
    end "&";
 
    function "&" (Left  : Vector; Right : Element_Type) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  Here we handle the easy case first, when the vector parameter (Left)
+      --  is empty.
+
       if Left.Is_Empty then
          declare
             Elements : constant Elements_Access :=
@@ -168,8 +211,10 @@ package body Ada.Containers.Vectors is
          end;
       end if;
 
-      --  We must satisfy two constraints: the new length cannot exceed
-      --  Count_Type'Last, and the new Last index cannot exceed
+      --  The vector parameter is not empty, so we must compute the length of
+      --  the result vector and its last index, but in such a way that overflow
+      --  is avoided. We must satisfy two constraints: the new length cannot
+      --  exceed Count_Type'Last, and the new Last index cannot exceed
       --  Index_Type'Last.
 
       if Left.Length = Count_Type'Last then
@@ -198,6 +243,14 @@ package body Ada.Containers.Vectors is
 
    function "&" (Left  : Element_Type; Right : Vector) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  Here we handle the easy case first, when the vector parameter (Right)
+      --  is empty.
+
       if Right.Is_Empty then
          declare
             Elements : constant Elements_Access :=
@@ -210,8 +263,10 @@ package body Ada.Containers.Vectors is
          end;
       end if;
 
-      --  We must satisfy two constraints: the new length cannot exceed
-      --  Count_Type'Last, and the new Last index cannot exceed
+      --  The vector parameter is not empty, so we must compute the length of
+      --  the result vector and its last index, but in such a way that overflow
+      --  is avoided. We must satisfy two constraints: the new length cannot
+      --  exceed Count_Type'Last, and the new Last index cannot exceed
       --  Index_Type'Last.
 
       if Right.Length = Count_Type'Last then
@@ -240,6 +295,17 @@ package body Ada.Containers.Vectors is
 
    function "&" (Left, Right : Element_Type) return Vector is
    begin
+      --  We decide that the capacity of the result is the sum of the lengths
+      --  of the parameters. We could decide to make it larger, but we have no
+      --  basis for knowing how much larger, so we just allocate the minimum
+      --  amount of storage.
+
+      --  We must compute the length of the result vector and its last index,
+      --  but in such a way that overflow is avoided. We must satisfy two
+      --  constraints: the new length cannot exceed Count_Type'Last (here, we
+      --  know that that condition is satisfied), and the new Last index cannot
+      --  exceed Index_Type'Last.
+
       if Index_Type'First >= Index_Type'Last then
          raise Constraint_Error with "new length is out of range";
       end if;
@@ -401,56 +467,117 @@ package body Ada.Containers.Vectors is
       Index     : Extended_Index;
       Count     : Count_Type := 1)
    is
-   begin
+      Old_Last : constant Index_Type'Base := Container.Last;
+      New_Last : Index_Type'Base;
+      Count2   : Count_Type'Base;  -- count of items from Index to Old_Last
+      J        : Index_Type'Base;  -- first index of items that slide down
+
+   begin
+      --  Delete removes items from the vector, the number of which is the
+      --  minimum of the specified Count and the items (if any) that exist from
+      --  Index to Container.Last. There are no constraints on the specified
+      --  value of Count (it can be larger than what's available at this
+      --  position in the vector, for example), but there are constraints on
+      --  the allowed values of the Index.
+
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying which items
+      --  should be deleted, so we must manually check. (That the user is
+      --  allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
+
       if Index < Index_Type'First then
          raise Constraint_Error with "Index is out of range (too small)";
       end if;
 
-      if Index > Container.Last then
-         if Index > Container.Last + 1 then
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows the
+      --  corner case of deleting no items from the back end of the vector to
+      --  be treated as a no-op. (It is assumed that specifying an index value
+      --  greater than Last + 1 indicates some deeper flaw in the caller's
+      --  algorithm, so that case is treated as a proper error.)
+
+      if Index > Old_Last then
+         if Index > Old_Last + 1 then
             raise Constraint_Error with "Index is out of range (too large)";
          end if;
 
          return;
       end if;
 
+      --  Here and elsewhere we treat deleting 0 items from the container as a
+      --  no-op, even when the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
+      --  The tampering bits exist to prevent an item from being deleted (or
+      --  otherwise harmfully manipulated) while it is being visited. Query,
+      --  Update, and Iterate increment the busy count on entry, and decrement
+      --  the count on exit. Delete checks the count to determine whether it is
+      --  being called while the associated callback procedure is executing.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
-      declare
-         I_As_Int        : constant Int := Int (Index);
-         Old_Last_As_Int : constant Int := Index_Type'Pos (Container.Last);
+      --  We first calculate what's available for deletion starting at
+      --  Index. Here and elsewhere we use the wider of Index_Type'Base and
+      --  Count_Type'Base as the type for intermediate values. (See function
+      --  Length for more information.)
+
+      if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then
+         Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1;
+
+      else
+         Count2 := Count_Type'Base (Old_Last - Index + 1);
+      end if;
 
-         Count1 : constant Int'Base := Count_Type'Pos (Count);
-         Count2 : constant Int'Base := Old_Last_As_Int - I_As_Int + 1;
-         N      : constant Int'Base := Int'Min (Count1, Count2);
+      --  If more elements are requested (Count) for deletion than are
+      --  available (Count2) for deletion beginning at Index, then everything
+      --  from Index is deleted. There are no elements to slide down, and so
+      --  all we need to do is set the value of Container.Last.
 
-         J_As_Int : constant Int'Base := I_As_Int + N;
+      if Count >= Count2 then
+         Container.Last := Index - 1;
+         return;
+      end if;
 
-      begin
-         if J_As_Int > Old_Last_As_Int then
-            Container.Last := Index - 1;
+      --  There are some elements aren't being deleted (the requested count was
+      --  less than the available count), so we must slide them down to
+      --  Index. We first calculate the index values of the respective array
+      --  slices, using the wider of Index_Type'Base and Count_Type'Base as the
+      --  type for intermediate calculations. For the elements that slide down,
+      --  index value New_Last is the last index value of their new home, and
+      --  index value J is the first index of their old home.
 
-         else
-            declare
-               J  : constant Index_Type := Index_Type (J_As_Int);
-               EA : Elements_Array renames Container.Elements.EA;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := Old_Last - Index_Type'Base (Count);
+         J := Index + Index_Type'Base (Count);
 
-               New_Last_As_Int : constant Int'Base := Old_Last_As_Int - N;
-               New_Last        : constant Index_Type :=
-                                   Index_Type (New_Last_As_Int);
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count);
+         J := Index_Type'Base (Count_Type'Base (Index) + Count);
+      end if;
 
-            begin
-               EA (Index .. New_Last) := EA (J .. Container.Last);
-               Container.Last := New_Last;
-            end;
-         end if;
+      --  The internal elements array isn't guaranteed to exist unless we have
+      --  elements, but we have that guarantee here because we know we have
+      --  elements to slide.  The array index values for each slice have
+      --  already been determined, so we just slide down to Index the elements
+      --  that weren't deleted.
+
+      declare
+         EA : Elements_Array renames Container.Elements.EA;
+
+      begin
+         EA (Index .. New_Last) := EA (J .. Old_Last);
+         Container.Last := New_Last;
       end;
    end Delete;
 
@@ -507,24 +634,47 @@ package body Ada.Containers.Vectors is
      (Container : in out Vector;
       Count     : Count_Type := 1)
    is
-      Index : Int'Base;
-
    begin
+      --  It is not permitted to delete items while the container is busy (for
+      --  example, we're in the middle of a passive iteration). However, we
+      --  always treat deleting 0 items as a no-op, even when we're busy, so we
+      --  simply return without checking.
+
       if Count = 0 then
          return;
       end if;
 
+      --  The tampering bits exist to prevent an item from being deleted (or
+      --  otherwise harmfully manipulated) while it is being visited. Query,
+      --  Update, and Iterate increment the busy count on entry, and decrement
+      --  the count on exit. Delete_Last checks the count to determine whether
+      --  it is being called while the associated callback procedure is
+      --  executing.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
+      --  There is no restriction on how large Count can be when deleting
+      --  items. If it is equal or greater than the current length, then this
+      --  is equivalent to clearing the vector. (In particular, there's no need
+      --  for us to actually calculate the new value for Last.)
+
+      --  If the requested count is less than the current length, then we must
+      --  calculate the new value for Last. For the type we use the widest of
+      --  Index_Type'Base and Count_Type'Base for the intermediate values of
+      --  our calculation.  (See the comments in Length for more information.)
+
       if Count >= Container.Length then
          Container.Last := No_Index;
 
+      elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         Container.Last := Container.Last - Index_Type'Base (Count);
+
       else
-         Index := Int (Container.Last) - Int (Count);
-         Container.Last := Index_Type (Index);
+         Container.Last :=
+           Index_Type'Base (Count_Type'Base (Container.Last) - Count);
       end if;
    end Delete_Last;
 
@@ -804,22 +954,42 @@ package body Ada.Containers.Vectors is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    is
-      N : constant Int := Count_Type'Pos (Count);
-
-      First           : constant Int := Int (Index_Type'First);
-      New_Last_As_Int : Int'Base;
-      New_Last        : Index_Type;
-      New_Length      : UInt;
-      Max_Length      : constant UInt := UInt (Count_Type'Last);
+      Old_Length : constant Count_Type := Container.Length;
 
-      Dst : Elements_Access;
+      Max_Length : Count_Type'Base;  -- determined from range of Index_Type
+      New_Length : Count_Type'Base;  -- sum of current length and Count
+      New_Last   : Index_Type'Base;  -- last index of vector after insertion
+
+      Index : Index_Type'Base;  -- scratch for intermediate values
+      J     : Count_Type'Base;  -- scratch
+
+      New_Capacity : Count_Type'Base;  -- length of new, expanded array
+      Dst_Last     : Index_Type'Base;  -- last index of new, expanded array
+      Dst          : Elements_Access;  -- new, expanded internal array
+
+   begin
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying where the new
+      --  items should be inserted, so we must manually check. (That the user
+      --  is allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
 
-   begin
       if Before < Index_Type'First then
          raise Constraint_Error with
            "Before index is out of range (too small)";
       end if;
 
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows for the
+      --  case of appending items to the back end of the vector. (It is assumed
+      --  that specifying an index value greater than Last + 1 indicates some
+      --  deeper flaw in the caller's algorithm, so that case is treated as a
+      --  proper error.)
+
       if Before > Container.Last
         and then Before > Container.Last + 1
       then
@@ -827,67 +997,192 @@ package body Ada.Containers.Vectors is
            "Before index is out of range (too large)";
       end if;
 
+      --  We treat inserting 0 items into the container as a no-op, even when
+      --  the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
-      declare
-         Old_Last_As_Int : constant Int := Int (Container.Last);
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the current length and the insertion
+      --  count. Note that we cannot simply add these values, because of the
+      --  possibilty of overflow.
+
+      if Old_Length > Count_Type'Last - Count then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector, without fear of
+      --  overflow.
+
+      New_Length := Old_Length + Count;
+
+      --  The second constraint is that the new Last index value cannot exceed
+      --  Index_Type'Last. In each branch below, we calculate the maximum
+      --  length (computed from the range of values in Index_Type), and then
+      --  compare the new length to the maximum length. If the new length is
+      --  acceptable, then we compute the new last index from that.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We have to handle the case when there might be more values in the
+         --  range of Index_Type than in the range of Count_Type.
 
-      begin
-         if Old_Last_As_Int > Int'Last - N then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+         if Index_Type'First <= 0 then
+            --  We know that No_Index (the same as Index_Type'First - 1) is
+            --  less than 0, so it is safe to compute the following sum without
+            --  fear of overflow.
+
+            Index := No_Index + Index_Type'Base (Count_Type'Last);
+
+            if Index <= Index_Type'Last then
+               --  We have determined that range of Index_Type has at least as
+               --  many values as in Count_Type, so Count_Type'Last is the
+               --  maximum number of items that are allowed.
 
-         New_Last_As_Int := Old_Last_As_Int + N;
+               Max_Length := Count_Type'Last;
 
-         if New_Last_As_Int > Int (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
+            else
+               --  The range of Index_Type has fewer values than in Count_Type,
+               --  so the maximum number of items is computed from the range of
+               --  the Index_Type.
+
+               Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
+            end if;
+
+         else
+            --  No_Index is equal or greater than 0, so we can safely compute
+            --  the difference without fear of overflow (which we would have to
+            --  worry about if No_Index were less than 0, but that case is
+            --  handled above).
+
+            Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
          end if;
 
-         New_Length := UInt (New_Last_As_Int - First + Int'(1));
+      elsif Index_Type'First <= 0 then
+         --  We know that No_Index (the same as Index_Type'First - 1) is less
+         --  than 0, so it is safe to compute the following sum without fear of
+         --  overflow.
 
-         if New_Length > Max_Length then
-            raise Constraint_Error with "new length is out of range";
+         J := Count_Type'Base (No_Index) + Count_Type'Last;
+
+         if J <= Count_Type'Base (Index_Type'Last) then
+            --  We have determined that range of Index_Type has at least as
+            --  many values as in Count_Type, so Count_Type'Last is the maximum
+            --  number of items that are allowed.
+
+            Max_Length := Count_Type'Last;
+
+         else
+            --  The range of Index_Type has fewer values than Count_Type does,
+            --  so the maximum number of items is computed from the range of
+            --  the Index_Type.
+
+            Max_Length :=
+              Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
          end if;
 
-         New_Last := Index_Type (New_Last_As_Int);
-      end;
+      else
+         --  No_Index is equal or greater than 0, so we can safely compute the
+         --  difference without fear of overflow (which we would have to worry
+         --  about if No_Index were less than 0, but that case is handled
+         --  above).
 
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
+         Max_Length :=
+           Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
+      end if;
+
+      --  We have just computed the maximum length (number of items). We must
+      --  now compare the requested length to the maximum length, as we do not
+      --  allow a vector expand beyond the maximum (because that would create
+      --  an internal array with a last index value greater than
+      --  Index_Type'Last, with no way to index those elements).
+
+      if New_Length > Max_Length then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  New_Last is the last index value of the items in the container after
+      --  insertion.  Use the wider of Index_Type'Base and Count_Type'Base to
+      --  compute its value from the New_Length.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := No_Index + Index_Type'Base (New_Length);
+
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
       end if;
 
       if Container.Elements = null then
+         pragma Assert (Container.Last = No_Index);
+
+         --  This is the simplest case, with which we must always begin: we're
+         --  inserting items into an empty vector that hasn't allocated an
+         --  internal array yet. Note that we don't need to check the busy bit
+         --  here, because an empty container cannot be busy.
+
+         --  In order to preserve container invariants, we allocate the new
+         --  internal array first, before setting the Last index value, in case
+         --  the allocation fails (which can happen either because there is no
+         --  storage available, or because element initialization fails).
+
          Container.Elements := new Elements_Type'
                                      (Last => New_Last,
                                       EA   => (others => New_Item));
+
+         --  The allocation of the new, internal array succeeded, so it is now
+         --  safe to update the Last index, restoring container invariants.
+
          Container.Last := New_Last;
+
          return;
       end if;
 
-      if New_Last <= Container.Elements.Last then
+      --  The tampering bits exist to prevent an item from being harmfully
+      --  manipulated while it is being visited. Query, Update, and Iterate
+      --  increment the busy count on entry, and decrement the count on
+      --  exit. Insert checks the count to determine whether it is being called
+      --  while the associated callback procedure is executing.
+
+      if Container.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with elements (vector is busy)";
+      end if;
+
+      --  An internal array has already been allocated, so we must determine
+      --  whether there is enough unused storage for the new items.
+
+      if New_Length <= Container.Elements.EA'Length then
+         --  In this case, we're inserting elements into a vector that has
+         --  already allocated an internal array, and the existing array has
+         --  enough unused storage for the new items.
+
          declare
             EA : Elements_Array renames Container.Elements.EA;
 
          begin
-            if Before <= Container.Last then
-               declare
-                  Index_As_Int : constant Int'Base :=
-                                   Index_Type'Pos (Before) + N;
-
-                  Index : constant Index_Type := Index_Type (Index_As_Int);
-
-               begin
-                  EA (Index .. New_Last) := EA (Before .. Container.Last);
-
-                  EA (Before .. Index_Type'Pred (Index)) :=
-                      (others => New_Item);
-               end;
+            if Before > Container.Last then
+               --  The new items are being appended to the vector, so no
+               --  sliding of existing elements is required.
 
-            else
                EA (Before .. New_Last) := (others => New_Item);
+
+            else
+               --  The new items are being inserted before some existing
+               --  elements, so we must slide the existing elements up to their
+               --  new home. We use the wider of Index_Type'Base and
+               --  Count_Type'Base as the type for intermediate index values.
+
+               if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+                  Index := Before + Index_Type'Base (Count);
+
+               else
+                  Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+               end if;
+
+               EA (Index .. New_Last) := EA (Before .. Container.Last);
+               EA (Before .. Index - 1) := (others => New_Item);
             end if;
          end;
 
@@ -895,67 +1190,79 @@ package body Ada.Containers.Vectors is
          return;
       end if;
 
-      declare
-         C, CC : UInt;
+      --  In this case, we're inserting elements into a vector that has already
+      --  allocated an internal array, but the existing array does not have
+      --  enough storage, so we must allocate a new, longer array. In order to
+      --  guarantee that the amortized insertion cost is O(1), we always
+      --  allocate an array whose length is some power-of-two factor of the
+      --  current array length. (The new array cannot have a length less than
+      --  the New_Length of the container, but its last index value cannot be
+      --  greater than Index_Type'Last.)
+
+      New_Capacity := Count_Type'Max (1, Container.Elements.EA'Length);
+      while New_Capacity < New_Length loop
+         if New_Capacity > Count_Type'Last / 2 then
+            New_Capacity := Count_Type'Last;
+            exit;
+         end if;
 
-      begin
-         C := UInt'Max (1, Container.Elements.EA'Length);  -- ???
-         while C < New_Length loop
-            if C > UInt'Last / 2 then
-               C := UInt'Last;
-               exit;
-            end if;
+         New_Capacity := 2 * New_Capacity;
+      end loop;
 
-            C := 2 * C;
-         end loop;
+      if New_Capacity > Max_Length then
+         --  We have reached the limit of capacity, so no further expansion
+         --  will occur. (This is not a problem, as there is never a need to
+         --  have more capacity than the maximum container length.)
 
-         if C > Max_Length then
-            C := Max_Length;
-         end if;
+         New_Capacity := Max_Length;
+      end if;
 
-         if Index_Type'First <= 0
-           and then Index_Type'Last >= 0
-         then
-            CC := UInt (Index_Type'Last) + UInt (-Index_Type'First) + 1;
-         else
-            CC := UInt (Int (Index_Type'Last) - First + 1);
-         end if;
+      --  We have computed the length of the new internal array (and this is
+      --  what "vector capacity" means), so use that to compute its last index.
 
-         if C > CC then
-            C := CC;
-         end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         Dst_Last := No_Index + Index_Type'Base (New_Capacity);
 
-         declare
-            Dst_Last : constant Index_Type :=
-                         Index_Type (First + UInt'Pos (C) - 1);
+      else
+         Dst_Last :=
+           Index_Type'Base (Count_Type'Base (No_Index) + New_Capacity);
+      end if;
 
-         begin
-            Dst := new Elements_Type (Dst_Last);
-         end;
-      end;
+      --  Now we allocate the new, longer internal array. If the allocation
+      --  fails, we have not changed any container state, so no side-effect
+      --  will occur as a result of propagating the exception.
+
+      Dst := new Elements_Type (Dst_Last);
+
+      --  We have our new internal array. All that needs to be done now is to
+      --  copy the existing items (if any) from the old array (the "source"
+      --  array, object SA below) to the new array (the "destination" array,
+      --  object DA below), and then deallocate the old array.
 
       declare
-         SA : Elements_Array renames Container.Elements.EA;
-         DA : Elements_Array renames Dst.EA;
+         SA : Elements_Array renames Container.Elements.EA; -- source
+         DA : Elements_Array renames Dst.EA;                -- destination
 
       begin
-         DA (Index_Type'First .. Index_Type'Pred (Before)) :=
-           SA (Index_Type'First .. Index_Type'Pred (Before));
+         DA (Index_Type'First .. Before - 1) :=
+           SA (Index_Type'First .. Before - 1);
 
-         if Before <= Container.Last then
-            declare
-               Index_As_Int : constant Int'Base :=
-                                Index_Type'Pos (Before) + N;
+         if Before > Container.Last then
+            DA (Before .. New_Last) := (others => New_Item);
+
+         else
+            --  The new items are being inserted before some existing elements,
+            --  so we must slide the existing elements up to their new home.
 
-               Index : constant Index_Type := Index_Type (Index_As_Int);
+            if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+               Index := Before + Index_Type'Base (Count);
 
-            begin
-               DA (Before .. Index_Type'Pred (Index)) := (others => New_Item);
-               DA (Index .. New_Last) := SA (Before .. Container.Last);
-            end;
+            else
+               Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+            end if;
 
-         else
-            DA (Before .. New_Last) := (others => New_Item);
+            DA (Before .. Index - 1) := (others => New_Item);
+            DA (Index .. New_Last) := SA (Before .. Container.Last);
          end if;
       exception
          when others =>
@@ -963,11 +1270,23 @@ package body Ada.Containers.Vectors is
             raise;
       end;
 
+      --  We have successfully copied the items onto the new array, so the
+      --  final thing to do is deallocate the old array.
+
       declare
          X : Elements_Access := Container.Elements;
       begin
+         --  We first isolate the old internal array, removing it from the
+         --  container and replacing it with the new internal array, before we
+         --  deallocate the old array (which can fail if finalization of
+         --  elements propagates an exception).
+
          Container.Elements := Dst;
          Container.Last := New_Last;
+
+         --  The container invariants have been restored, so it is now safe to
+         --  attempt to deallocate the old array.
+
          Free (X);
       end;
    end Insert;
@@ -978,83 +1297,118 @@ package body Ada.Containers.Vectors is
       New_Item  : Vector)
    is
       N : constant Count_Type := Length (New_Item);
+      J : Index_Type'Base;
 
    begin
-      if Before < Index_Type'First then
-         raise Constraint_Error with
-           "Before index is out of range (too small)";
+      --  Use Insert_Space to create the "hole" (the destination slice) into
+      --  which we copy the source items.
+
+      Insert_Space (Container, Before, Count => N);
+
+      if N = 0 then
+         --  There's nothing else to do here (vetting of parameters was
+         --  performed already in Insert_Space), so we simply return.
+
+         return;
       end if;
 
-      if Before > Container.Last
-        and then Before > Container.Last + 1
-      then
-         raise Constraint_Error with
-           "Before index is out of range (too large)";
+      --  We calculate the last index value of the destination slice using the
+      --  wider of Index_Type'Base and count_Type'Base.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         J := (Before - 1) + Index_Type'Base (N);
+
+      else
+         J := Index_Type'Base (Count_Type'Base (Before - 1) + N);
       end if;
 
-      if N = 0 then
+      if Container'Address /= New_Item'Address then
+         --  This is the simple case.  New_Item denotes an object different
+         --  from Container, so there's nothing special we need to do to copy
+         --  the source items to their destination, because all of the source
+         --  items are contiguous.
+
+         Container.Elements.EA (Before .. J) :=
+           New_Item.Elements.EA (Index_Type'First .. New_Item.Last);
+
          return;
       end if;
 
-      Insert_Space (Container, Before, Count => N);
+      --  New_Item denotes the same object as Container, so an insertion has
+      --  potentially split the source items. The destination is always the
+      --  range [Before, J], but the source is [Index_Type'First, Before) and
+      --  (J, Container.Last]. We perform the copy in two steps, using each of
+      --  the two slices of the source items.
 
       declare
-         Dst_Last_As_Int : constant Int'Base :=
-                             Int'Base (Before) + Int'Base (N) - 1;
+         L : constant Index_Type'Base := Before - 1;
 
-         Dst_Last : constant Index_Type := Index_Type (Dst_Last_As_Int);
+         subtype Src_Index_Subtype is Index_Type'Base range
+           Index_Type'First .. L;
 
-      begin
-         if Container'Address /= New_Item'Address then
-            Container.Elements.EA (Before .. Dst_Last) :=
-              New_Item.Elements.EA (Index_Type'First .. New_Item.Last);
+         Src : Elements_Array renames
+           Container.Elements.EA (Src_Index_Subtype);
 
-            return;
-         end if;
-
-         declare
-            subtype Src_Index_Subtype is Index_Type'Base range
-              Index_Type'First .. Before - 1;
+         K : Index_Type'Base;
 
-            Src : Elements_Array renames
-                    Container.Elements.EA (Src_Index_Subtype);
+      begin
+         --  We first copy the source items that precede the space we
+         --  inserted. Index value K is the last index of that portion
+         --  destination that receives this slice of the source. (If Before
+         --  equals Index_Type'First, then this first source slice will be
+         --  empty, which is harmless.)
 
-            Index_As_Int : constant Int'Base :=
-                             Int (Before) + Src'Length - 1;
+         if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+            K := L + Index_Type'Base (Src'Length);
 
-            Index : constant Index_Type'Base :=
-                      Index_Type'Base (Index_As_Int);
+         else
+            K := Index_Type'Base (Count_Type'Base (L) + Src'Length);
+         end if;
 
-            Dst : Elements_Array renames
-                    Container.Elements.EA (Before .. Index);
+         Container.Elements.EA (Before .. K) := Src;
 
-         begin
-            Dst := Src;
-         end;
+         if Src'Length = N then
+            --  The new items were effectively appended to the container, so we
+            --  have already copied all of the items that need to be copied.
+            --  We return early here, even though the source slice below is
+            --  empty (so the assignment would be harmless), because we want to
+            --  avoid computing J + 1, which will overflow if J equals
+            --  Index_Type'Base'Last.
 
-         if Dst_Last = Container.Last then
             return;
          end if;
+      end;
 
-         declare
-            subtype Src_Index_Subtype is Index_Type'Base range
-              Dst_Last + 1 .. Container.Last;
+      declare
+         --  Note that we want to avoid computing J + 1 here, in case J equals
+         --  Index_Type'Base'Last. We prevent that by returning early above,
+         --  immediately after copying the first slice of the source, and
+         --  determining that this second slice of the source is empty.
 
-            Src : Elements_Array renames
-                    Container.Elements.EA (Src_Index_Subtype);
+         F : constant Index_Type'Base := J + 1;
 
-            Index_As_Int : constant Int'Base :=
-                             Dst_Last_As_Int - Src'Length + 1;
+         subtype Src_Index_Subtype is Index_Type'Base range
+           F .. Container.Last;
 
-            Index : constant Index_Type :=
-                      Index_Type (Index_As_Int);
+         Src : Elements_Array renames
+           Container.Elements.EA (Src_Index_Subtype);
 
-            Dst : Elements_Array renames
-                    Container.Elements.EA (Index .. Dst_Last);
+         K : Index_Type'Base;
 
-         begin
-            Dst := Src;
-         end;
+      begin
+         --  We next copy the source items that follow the space we
+         --  inserted. Index value K is the first index of that portion of the
+         --  destination that receives this slice of the source. (For the
+         --  reasons given above, this slice is guaranteed to be non-empty.)
+
+         if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+            K := F - Index_Type'Base (Src'Length);
+
+         else
+            K := Index_Type'Base (Count_Type'Base (F) - Src'Length);
+         end if;
+
+         Container.Elements.EA (K .. J) := Src;
       end;
    end Insert;
 
@@ -1256,22 +1610,42 @@ package body Ada.Containers.Vectors is
       Before    : Extended_Index;
       Count     : Count_Type := 1)
    is
-      N : constant Int := Count_Type'Pos (Count);
-
-      First           : constant Int := Int (Index_Type'First);
-      New_Last_As_Int : Int'Base;
-      New_Last        : Index_Type;
-      New_Length      : UInt;
-      Max_Length      : constant UInt := UInt (Count_Type'Last);
+      Old_Length : constant Count_Type := Container.Length;
 
-      Dst : Elements_Access;
+      Max_Length : Count_Type'Base;  -- determined from range of Index_Type
+      New_Length : Count_Type'Base;  -- sum of current length and Count
+      New_Last   : Index_Type'Base;  -- last index of vector after insertion
+
+      Index : Index_Type'Base;  -- scratch for intermediate values
+      J     : Count_Type'Base;  -- scratch
+
+      New_Capacity : Count_Type'Base;  -- length of new, expanded array
+      Dst_Last     : Index_Type'Base;  -- last index of new, expanded array
+      Dst          : Elements_Access;  -- new, expanded internal array
+
+   begin
+      --  As a precondition on the generic actual Index_Type, the base type
+      --  must include Index_Type'Pred (Index_Type'First); this is the value
+      --  that Container.Last assumes when the vector is empty. However, we do
+      --  not allow that as the value for Index when specifying where the new
+      --  items should be inserted, so we must manually check. (That the user
+      --  is allowed to specify the value at all here is a consequence of the
+      --  declaration of the Extended_Index subtype, which includes the values
+      --  in the base range that immediately precede and immediately follow the
+      --  values in the Index_Type.)
 
-   begin
       if Before < Index_Type'First then
          raise Constraint_Error with
            "Before index is out of range (too small)";
       end if;
 
+      --  We do allow a value greater than Container.Last to be specified as
+      --  the Index, but only if it's immediately greater. This allows for the
+      --  case of appending items to the back end of the vector. (It is assumed
+      --  that specifying an index value greater than Last + 1 indicates some
+      --  deeper flaw in the caller's algorithm, so that case is treated as a
+      --  proper error.)
+
       if Before > Container.Last
         and then Before > Container.Last + 1
       then
@@ -1279,58 +1653,184 @@ package body Ada.Containers.Vectors is
            "Before index is out of range (too large)";
       end if;
 
+      --  We treat inserting 0 items into the container as a no-op, even when
+      --  the container is busy, so we simply return.
+
       if Count = 0 then
          return;
       end if;
 
-      declare
-         Old_Last_As_Int : constant Int := Int (Container.Last);
+      --  There are two constraints we need to satisfy. The first constraint is
+      --  that a container cannot have more than Count_Type'Last elements, so
+      --  we must check the sum of the current length and the insertion
+      --  count. Note that we cannot simply add these values, because of the
+      --  possibilty of overflow.
+
+      if Old_Length > Count_Type'Last - Count then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  It is now safe compute the length of the new vector, without fear of
+      --  overflow.
+
+      New_Length := Old_Length + Count;
+
+      --  The second constraint is that the new Last index value cannot exceed
+      --  Index_Type'Last. In each branch below, we calculate the maximum
+      --  length (computed from the range of values in Index_Type), and then
+      --  compare the new length to the maximum length. If the new length is
+      --  acceptable, then we compute the new last index from that.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We have to handle the case when there might be more values in the
+         --  range of Index_Type than in the range of Count_Type.
 
-      begin
-         if Old_Last_As_Int > Int'Last - N then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+         if Index_Type'First <= 0 then
+            --  We know that No_Index (the same as Index_Type'First - 1) is
+            --  less than 0, so it is safe to compute the following sum without
+            --  fear of overflow.
+
+            Index := No_Index + Index_Type'Base (Count_Type'Last);
+
+            if Index <= Index_Type'Last then
+               --  We have determined that range of Index_Type has at least as
+               --  many values as in Count_Type, so Count_Type'Last is the
+               --  maximum number of items that are allowed.
 
-         New_Last_As_Int := Old_Last_As_Int + N;
+               Max_Length := Count_Type'Last;
 
-         if New_Last_As_Int > Int (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
+            else
+               --  The range of Index_Type has fewer values than in Count_Type,
+               --  so the maximum number of items is computed from the range of
+               --  the Index_Type.
+
+               Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
+            end if;
+
+         else
+            --  No_Index is equal or greater than 0, so we can safely compute
+            --  the difference without fear of overflow (which we would have to
+            --  worry about if No_Index were less than 0, but that case is
+            --  handled above).
+
+            Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
          end if;
 
-         New_Length := UInt (New_Last_As_Int - First + Int'(1));
+      elsif Index_Type'First <= 0 then
+         --  We know that No_Index (the same as Index_Type'First - 1) is less
+         --  than 0, so it is safe to compute the following sum without fear of
+         --  overflow.
 
-         if New_Length > Max_Length then
-            raise Constraint_Error with "new length is out of range";
+         J := Count_Type'Base (No_Index) + Count_Type'Last;
+
+         if J <= Count_Type'Base (Index_Type'Last) then
+            --  We have determined that range of Index_Type has at least as
+            --  many values as in Count_Type, so Count_Type'Last is the maximum
+            --  number of items that are allowed.
+
+            Max_Length := Count_Type'Last;
+
+         else
+            --  The range of Index_Type has fewer values than Count_Type does,
+            --  so the maximum number of items is computed from the range of
+            --  the Index_Type.
+
+            Max_Length :=
+              Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
          end if;
 
-         New_Last := Index_Type (New_Last_As_Int);
-      end;
+      else
+         --  No_Index is equal or greater than 0, so we can safely compute the
+         --  difference without fear of overflow (which we would have to worry
+         --  about if No_Index were less than 0, but that case is handled
+         --  above).
 
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
+         Max_Length :=
+           Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
+      end if;
+
+      --  We have just computed the maximum length (number of items). We must
+      --  now compare the requested length to the maximum length, as we do not
+      --  allow a vector expand beyond the maximum (because that would create
+      --  an internal array with a last index value greater than
+      --  Index_Type'Last, with no way to index those elements).
+
+      if New_Length > Max_Length then
+         raise Constraint_Error with "Count is out of range";
+      end if;
+
+      --  New_Last is the last index value of the items in the container after
+      --  insertion.  Use the wider of Index_Type'Base and Count_Type'Base to
+      --  compute its value from the New_Length.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         New_Last := No_Index + Index_Type'Base (New_Length);
+
+      else
+         New_Last := Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
       end if;
 
       if Container.Elements = null then
+         pragma Assert (Container.Last = No_Index);
+
+         --  This is the simplest case, with which we must always begin: we're
+         --  inserting items into an empty vector that hasn't allocated an
+         --  internal array yet. Note that we don't need to check the busy bit
+         --  here, because an empty container cannot be busy.
+
+         --  In order to preserve container invariants, we allocate the new
+         --  internal array first, before setting the Last index value, in case
+         --  the allocation fails (which can happen either because there is no
+         --  storage available, or because default-valued element
+         --  initialization fails).
+
          Container.Elements := new Elements_Type (New_Last);
+
+         --  The allocation of the new, internal array succeeded, so it is now
+         --  safe to update the Last index, restoring container invariants.
+
          Container.Last := New_Last;
+
          return;
       end if;
 
+      --  The tampering bits exist to prevent an item from being harmfully
+      --  manipulated while it is being visited. Query, Update, and Iterate
+      --  increment the busy count on entry, and decrement the count on
+      --  exit. Insert checks the count to determine whether it is being called
+      --  while the associated callback procedure is executing.
+
+      if Container.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with elements (vector is busy)";
+      end if;
+
+      --  An internal array has already been allocated, so we must determine
+      --  whether there is enough unused storage for the new items.
+
       if New_Last <= Container.Elements.Last then
+         --  In this case, we're inserting space into a vector that has already
+         --  allocated an internal array, and the existing array has enough
+         --  unused storage for the new items.
+
          declare
             EA : Elements_Array renames Container.Elements.EA;
+
          begin
             if Before <= Container.Last then
-               declare
-                  Index_As_Int : constant Int'Base :=
-                                   Index_Type'Pos (Before) + N;
-
-                  Index : constant Index_Type := Index_Type (Index_As_Int);
-
-               begin
-                  EA (Index .. New_Last) := EA (Before .. Container.Last);
-               end;
+               --  The space is being inserted before some existing elements,
+               --  so we must slide the existing elements up to their new
+               --  home. We use the wider of Index_Type'Base and
+               --  Count_Type'Base as the type for intermediate index values.
+
+               if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+                  Index := Before + Index_Type'Base (Count);
+
+               else
+                  Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+               end if;
+
+               EA (Index .. New_Last) := EA (Before .. Container.Last);
             end if;
          end;
 
@@ -1338,63 +1838,75 @@ package body Ada.Containers.Vectors is
          return;
       end if;
 
-      declare
-         C, CC : UInt;
+      --  In this case, we're inserting space into a vector that has already
+      --  allocated an internal array, but the existing array does not have
+      --  enough storage, so we must allocate a new, longer array. In order to
+      --  guarantee that the amortized insertion cost is O(1), we always
+      --  allocate an array whose length is some power-of-two factor of the
+      --  current array length. (The new array cannot have a length less than
+      --  the New_Length of the container, but its last index value cannot be
+      --  greater than Index_Type'Last.)
+
+      New_Capacity := Count_Type'Max (1, Container.Elements.EA'Length);
+      while New_Capacity < New_Length loop
+         if New_Capacity > Count_Type'Last / 2 then
+            New_Capacity := Count_Type'Last;
+            exit;
+         end if;
 
-      begin
-         C := UInt'Max (1, Container.Elements.EA'Length);  -- ???
-         while C < New_Length loop
-            if C > UInt'Last / 2 then
-               C := UInt'Last;
-               exit;
-            end if;
+         New_Capacity := 2 * New_Capacity;
+      end loop;
 
-            C := 2 * C;
-         end loop;
+      if New_Capacity > Max_Length then
+         --  We have reached the limit of capacity, so no further expansion
+         --  will occur. (This is not a problem, as there is never a need to
+         --  have more capacity than the maximum container length.)
 
-         if C > Max_Length then
-            C := Max_Length;
-         end if;
+         New_Capacity := Max_Length;
+      end if;
 
-         if Index_Type'First <= 0
-           and then Index_Type'Last >= 0
-         then
-            CC := UInt (Index_Type'Last) + UInt (-Index_Type'First) + 1;
-         else
-            CC := UInt (Int (Index_Type'Last) - First + 1);
-         end if;
+      --  We have computed the length of the new internal array (and this is
+      --  what "vector capacity" means), so use that to compute its last index.
 
-         if C > CC then
-            C := CC;
-         end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         Dst_Last := No_Index + Index_Type'Base (New_Capacity);
 
-         declare
-            Dst_Last : constant Index_Type :=
-                         Index_Type (First + UInt'Pos (C) - 1);
+      else
+         Dst_Last :=
+           Index_Type'Base (Count_Type'Base (No_Index) + New_Capacity);
+      end if;
 
-         begin
-            Dst := new Elements_Type (Dst_Last);
-         end;
-      end;
+      --  Now we allocate the new, longer internal array. If the allocation
+      --  fails, we have not changed any container state, so no side-effect
+      --  will occur as a result of propagating the exception.
+
+      Dst := new Elements_Type (Dst_Last);
+
+      --  We have our new internal array. All that needs to be done now is to
+      --  copy the existing items (if any) from the old array (the "source"
+      --  array, object SA below) to the new array (the "destination" array,
+      --  object DA below), and then deallocate the old array.
 
       declare
-         SA : Elements_Array renames Container.Elements.EA;
-         DA : Elements_Array renames Dst.EA;
+         SA : Elements_Array renames Container.Elements.EA;  -- source
+         DA : Elements_Array renames Dst.EA;                 -- destination
 
       begin
-         DA (Index_Type'First .. Index_Type'Pred (Before)) :=
-           SA (Index_Type'First .. Index_Type'Pred (Before));
+         DA (Index_Type'First .. Before - 1) :=
+           SA (Index_Type'First .. Before - 1);
 
          if Before <= Container.Last then
-            declare
-               Index_As_Int : constant Int'Base :=
-                                Index_Type'Pos (Before) + N;
+            --  The space is being inserted before some existing elements, so
+            --  we must slide the existing elements up to their new home.
 
-               Index : constant Index_Type := Index_Type (Index_As_Int);
+            if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+               Index := Before + Index_Type'Base (Count);
 
-            begin
-               DA (Index .. New_Last) := SA (Before .. Container.Last);
-            end;
+            else
+               Index := Index_Type'Base (Count_Type'Base (Before) + Count);
+            end if;
+
+            DA (Index .. New_Last) := SA (Before .. Container.Last);
          end if;
       exception
          when others =>
@@ -1402,11 +1914,24 @@ package body Ada.Containers.Vectors is
             raise;
       end;
 
+      --  We have successfully copied the items onto the new array, so the
+      --  final thing to do is restore invariants, and deallocate the old
+      --  array.
+
       declare
          X : Elements_Access := Container.Elements;
       begin
+         --  We first isolate the old internal array, removing it from the
+         --  container and replacing it with the new internal array, before we
+         --  deallocate the old array (which can fail if finalization of
+         --  elements propagates an exception).
+
          Container.Elements := Dst;
          Container.Last := New_Last;
+
+         --  The container invariants have been restored, so it is now safe to
+         --  attempt to deallocate the old array.
+
          Free (X);
       end;
    end Insert_Space;
@@ -1533,12 +2058,33 @@ package body Ada.Containers.Vectors is
    ------------
 
    function Length (Container : Vector) return Count_Type is
-      L : constant Int := Int (Container.Last);
-      F : constant Int := Int (Index_Type'First);
-      N : constant Int'Base := L - F + 1;
+      L : constant Index_Type'Base := Container.Last;
+      F : constant Index_Type := Index_Type'First;
 
    begin
-      return Count_Type (N);
+      --  The base range of the index type (Index_Type'Base) might not include
+      --  all values for length (Count_Type). Contrariwise, the index type
+      --  might include values outside the range of length.  Hence we use
+      --  whatever type is wider for intermediate values when calculating
+      --  length. Note that no matter what the index type is, the maximum
+      --  length to which a vector is allowed to grow is always the minimum
+      --  of Count_Type'Last and (IT'Last - IT'First + 1).
+
+      --  For example, an Index_Type with range -127 .. 127 is only guaranteed
+      --  to have a base range of -128 .. 127, but the corresponding vector
+      --  would have lengths in the range 0 .. 255. In this case we would need
+      --  to use Count_Type'Base for intermediate values.
+
+      --  Another case would be the index range -2**63 + 1 .. -2**63 + 10. The
+      --  vector would have a maximum length of 10, but the index values lie
+      --  outside the range of Count_Type (which is only 32 bits). In this
+      --  case we would need to use Index_Type'Base for intermediate values.
+
+      if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then
+         return Count_Type'Base (L) - Count_Type'Base (F) + 1;
+      else
+         return Count_Type (L - F + 1);
+      end if;
    end Length;
 
    ----------
@@ -1799,17 +2345,51 @@ package body Ada.Containers.Vectors is
    is
       N : constant Count_Type := Length (Container);
 
+      Index : Count_Type'Base;
+      Last  : Index_Type'Base;
+
    begin
+      --  Reserve_Capacity can be used to either expand the storage available
+      --  for elements (this would be its typical use, in anticipation of
+      --  future insertion), or to trim back storage. In the latter case,
+      --  storage can only be trimmed back to the limit of the container
+      --  length. Note that Reserve_Capacity neither deletes (active) elements
+      --  nor inserts elements; it only affects container capacity, never
+      --  container length.
+
       if Capacity = 0 then
+         --  This is a request to trim back storage, to the minimum amount
+         --  possible given the current state of the container.
+
          if N = 0 then
+            --  The container is empty, so in this unique case we can
+            --  deallocate the entire internal array. Note that an empty
+            --  container can never be busy, so there's no need to check the
+            --  tampering bits.
+
             declare
                X : Elements_Access := Container.Elements;
             begin
+               --  First we remove the internal array from the container, to
+               --  handle the case when the deallocation raises an exception.
+
                Container.Elements := null;
+
+               --  Container invariants have been restored, so it is now safe
+               --  to attempt to deallocate the internal array.
+
                Free (X);
             end;
 
          elsif N < Container.Elements.EA'Length then
+            --  The container is not empty, and the current length is less than
+            --  the current capacity, so there's storage available to trim. In
+            --  this case, we allocate a new internal array having a length
+            --  that exactly matches the number of items in the
+            --  container. (Reserve_Capacity does not delete active elements,
+            --  so this is the best we can do with respect to minimizing
+            --  storage).
+
             if Container.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with elements (vector is busy)";
@@ -1825,7 +2405,23 @@ package body Ada.Containers.Vectors is
                X : Elements_Access := Container.Elements;
 
             begin
+               --  Although we have isolated the old internal array that we're
+               --  going to deallocate, we don't deallocate it until we have
+               --  successfully allocated a new one. If there is an exception
+               --  during allocation (either because there is not enough
+               --  storage, or because initialization of the elements fails),
+               --  we let it propagate without causing any side-effect.
+
                Container.Elements := new Elements_Type'(Container.Last, Src);
+
+               --  We have succesfully allocated a new internal array (with a
+               --  smaller length than the old one, and containing a copy of
+               --  just the active elements in the container), so it is now
+               --  safe to attempt to deallocate the old array. The old array
+               --  has been isolated, and container invariants have been
+               --  restored, so if the deallocation fails (because finalization
+               --  of the elements fails), we simply let it propagate.
+
                Free (X);
             end;
          end if;
@@ -1833,29 +2429,102 @@ package body Ada.Containers.Vectors is
          return;
       end if;
 
-      if Container.Elements = null then
-         declare
-            Last_As_Int : constant Int'Base :=
-                            Int (Index_Type'First) + Int (Capacity) - 1;
+      --  Reserve_Capacity can be used to expand the storage available for
+      --  elements, but we do not let the capacity grow beyond the number of
+      --  values in Index_Type'Range. (Were it otherwise, there would be no way
+      --  to refer to the elements with an index value greater than
+      --  Index_Type'Last, so that storage would be wasted.) Here we compute
+      --  the Last index value of the new internal array, in a way that avoids
+      --  any possibility of overflow.
 
-         begin
-            if Last_As_Int > Index_Type'Pos (Index_Type'Last) then
-               raise Constraint_Error with "new length is out of range";
-            end if;
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
 
-            declare
-               Last : constant Index_Type := Index_Type (Last_As_Int);
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
 
-            begin
-               Container.Elements := new Elements_Type (Last);
-            end;
-         end;
+         if Index_Type'Base'Last - Index_Type'Base (Capacity) < No_Index then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Capacity);
+
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
+
+         if Last > Index_Type'Last then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Capacity.
+
+         Index := Count_Type'Base (No_Index) + Capacity;  -- Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
+      else
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
+
+         Index := Count_Type'Base (Index_Type'Last) - Capacity;  -- No_Index
+
+         if Index < Count_Type'Base (No_Index) then
+            raise Constraint_Error with "Capacity is out of range";
+         end if;
+
+         --  We have determined that the value of Capacity would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Capacity);
+      end if;
+
+      --  The requested capacity is non-zero, but we don't know yet whether
+      --  this is a request for expansion or contraction of storage.
 
+      if Container.Elements = null then
+         --  The container is empty (it doesn't even have an internal array),
+         --  so this represents a request to allocate (expand) storage having
+         --  the given capacity.
+
+         Container.Elements := new Elements_Type (Last);
          return;
       end if;
 
       if Capacity <= N then
+         --  This is a request to trim back storage, but only to the limit of
+         --  what's already in the container. (Reserve_Capacity never deletes
+         --  active elements, it only reclaims excess storage.)
+
          if N < Container.Elements.EA'Length then
+            --  The container is not empty (because the requested capacity is
+            --  positive, and less than or equal to the container length), and
+            --  the current length is less than the current capacity, so
+            --  there's storage available to trim. In this case, we allocate a
+            --  new internal array having a length that exactly matches the
+            --  number of items in the container.
+
             if Container.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with elements (vector is busy)";
@@ -1871,63 +2540,99 @@ package body Ada.Containers.Vectors is
                X : Elements_Access := Container.Elements;
 
             begin
+               --  Although we have isolated the old internal array that we're
+               --  going to deallocate, we don't deallocate it until we have
+               --  successfully allocated a new one. If there is an exception
+               --  during allocation (either because there is not enough
+               --  storage, or because initialization of the elements fails),
+               --  we let it propagate without causing any side-effect.
+
                Container.Elements := new Elements_Type'(Container.Last, Src);
+
+               --  We have succesfully allocated a new internal array (with a
+               --  smaller length than the old one, and containing a copy of
+               --  just the active elements in the container), so it is now
+               --  safe to attempt to deallocate the old array. The old array
+               --  has been isolated, and container invariants have been
+               --  restored, so if the deallocation fails (because finalization
+               --  of the elements fails), we simply let it propagate.
+
                Free (X);
             end;
-
          end if;
 
          return;
       end if;
 
+      --  The requested capacity is larger than the container length (the
+      --  number of active elements). Whether this represents a request for
+      --  expansion or contraction of the current capacity depends on what the
+      --  current capacity is.
+
       if Capacity = Container.Elements.EA'Length then
+         --  The requested capacity matches the existing capacity, so there's
+         --  nothing to do here. We treat this case as a no-op, and simply
+         --  return without checking the busy bit.
+
          return;
       end if;
 
+      --  There is a change in the capacity of a non-empty container, so a new
+      --  internal array will be allocated. (The length of the new internal
+      --  array could be less or greater than the old internal array. We know
+      --  only that the length of the new internal array is greater than the
+      --  number of active elements in the container.) We must check whether
+      --  the container is busy before doing anything else.
+
       if Container.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with elements (vector is busy)";
       end if;
 
+      --  We now allocate a new internal array, having a length different from
+      --  its current value.
+
       declare
-         Last_As_Int : constant Int'Base :=
-                         Int (Index_Type'First) + Int (Capacity) - 1;
+         E : Elements_Access := new Elements_Type (Last);
 
       begin
-         if Last_As_Int > Index_Type'Pos (Index_Type'Last) then
-            raise Constraint_Error with "new length is out of range";
-         end if;
+         --  We have successfully allocated the new internal array. We first
+         --  attempt to copy the existing elements from the old internal array
+         --  ("src" elements) onto the new internal array ("tgt" elements).
 
          declare
-            Last : constant Index_Type := Index_Type (Last_As_Int);
+            subtype Index_Subtype is Index_Type'Base range
+              Index_Type'First .. Container.Last;
+
+            Src : Elements_Array renames
+                    Container.Elements.EA (Index_Subtype);
 
-            E : Elements_Access := new Elements_Type (Last);
+            Tgt : Elements_Array renames E.EA (Index_Subtype);
 
          begin
-            declare
-               subtype Index_Subtype is Index_Type'Base range
-                 Index_Type'First .. Container.Last;
+            Tgt := Src;
 
-               Src : Elements_Array renames
-                       Container.Elements.EA (Index_Subtype);
+         exception
+            when others =>
+               Free (E);
+               raise;
+         end;
 
-               Tgt : Elements_Array renames E.EA (Index_Subtype);
+         --  We have successfully copied the existing elements onto the new
+         --  internal array, so now we can attempt to deallocate the old one.
 
-            begin
-               Tgt := Src;
+         declare
+            X : Elements_Access := Container.Elements;
+         begin
+            --  First we isolate the old internal array, and replace it in the
+            --  container with the new internal array.
 
-            exception
-               when others =>
-                  Free (E);
-                  raise;
-            end;
+            Container.Elements := E;
 
-            declare
-               X : Elements_Access := Container.Elements;
-            begin
-               Container.Elements := E;
-               Free (X);
-            end;
+            --  Container invariants have been restored, so it is now safe to
+            --  attempt to deallocate the old internal array.
+
+            Free (X);
          end;
       end;
    end Reserve_Capacity;
@@ -2055,26 +2760,25 @@ package body Ada.Containers.Vectors is
    ----------------
 
    procedure Set_Length (Container : in out Vector; Length : Count_Type) is
+      Count : constant Count_Type'Base := Container.Length - Length;
+
    begin
-      if Length = Vectors.Length (Container) then
-         return;
-      end if;
+      --  Set_Length allows the user to set the length explicitly, instead of
+      --  implicitly as a side-effect of deletion or insertion. If the
+      --  requested length is less then the current length, this is equivalent
+      --  to deleting items from the back end of the vector. If the requested
+      --  length is greater than the current length, then this is equivalent to
+      --  inserting "space" (nonce items) at the end.
 
-      if Container.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with elements (vector is busy)";
-      end if;
+      if Count >= 0 then
+         Container.Delete_Last (Count);
 
-      if Length > Capacity (Container) then
-         Reserve_Capacity (Container, Capacity => Length);
-      end if;
+      elsif Container.Last >= Index_Type'Last then
+         raise Constraint_Error with "vector is already at its maximum length";
 
-      declare
-         Last_As_Int : constant Int'Base :=
-                         Int (Index_Type'First) + Int (Length) - 1;
-      begin
-         Container.Last := Index_Type'Base (Last_As_Int);
-      end;
+      else
+         Container.Insert_Space (Container.Last + 1, -Count);
+      end if;
    end Set_Length;
 
    ----------
@@ -2167,8 +2871,8 @@ package body Ada.Containers.Vectors is
    ---------------
 
    function To_Vector (Length : Count_Type) return Vector is
-      Index    : Int'Base;
-      Last     : Index_Type;
+      Index    : Count_Type'Base;
+      Last     : Index_Type'Base;
       Elements : Elements_Access;
 
    begin
@@ -2181,41 +2885,71 @@ package body Ada.Containers.Vectors is
       --  internal array) to exceed the number of values in Index_Type'Range
       --  (otherwise, there would be no way to refer to those components via an
       --  index).  We must therefore check whether the specified Length would
-      --  create a Last index value greater than Index_Type'Last. This
-      --  calculation requires care, because overflow can occur when
-      --  Index_Type'First is near the end of the range of Int.
-
-      if Index_Type'First <= 0 then
-         --  Compute the potential Last index value in the normal way, using
-         --  Int as the type in which to perform intermediate calculations. Int
-         --  is a 64-bit type, and Count_Type is a 32-bit type, so no overflow
-         --  can occur.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+      --  create a Last index value greater than Index_Type'Last.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (Length) < No_Index then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Length);
 
-         if Index > Int (Index_Type'Last) then
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
+
+         if Last > Index_Type'Last then
             raise Constraint_Error with "Length is out of range";
          end if;
 
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Length.
+
+         Index := Count_Type'Base (No_Index) + Length;  -- Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
       else
-         --  If Index_Type'First is within Length of Int'Last, then overflow
-         --  would occur if we simply computed Last directly. So instead of
-         --  computing Last, and then determining whether its value is greater
-         --  than Index_Type'Last, we work backwards by computing the potential
-         --  First index value, and then checking whether that value is less
-         --  than Index_Type'First.
-         Index := Int (Index_Type'Last) - Int (Length) + 1;
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
+
+         Index := Count_Type'Base (Index_Type'Last) - Length;  -- No_Index
 
-         if Index < Int (Index_Type'First) then
+         if Index < Count_Type'Base (No_Index) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
-         --  We have determined that Length would not create a Last index value
-         --  outside of the range of Index_Type, so we can now safely compute
-         --  its value.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+         --  We have determined that the value of Length would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Length);
       end if;
 
-      Last := Index_Type (Index);
       Elements := new Elements_Type (Last);
 
       return Vector'(Controlled with Elements, Last, 0, 0);
@@ -2225,8 +2959,8 @@ package body Ada.Containers.Vectors is
      (New_Item : Element_Type;
       Length   : Count_Type) return Vector
    is
-      Index    : Int'Base;
-      Last     : Index_Type;
+      Index    : Count_Type'Base;
+      Last     : Index_Type'Base;
       Elements : Elements_Access;
 
    begin
@@ -2239,41 +2973,71 @@ package body Ada.Containers.Vectors is
       --  internal array) to exceed the number of values in Index_Type'Range
       --  (otherwise, there would be no way to refer to those components via an
       --  index). We must therefore check whether the specified Length would
-      --  create a Last index value greater than Index_Type'Last. This
-      --  calculation requires care, because overflow can occur when
-      --  Index_Type'First is near the end of the range of Int.
-
-      if Index_Type'First <= 0 then
-         --  Compute the potential Last index value in the normal way, using
-         --  Int as the type in which to perform intermediate calculations. Int
-         --  is a 64-bit type, and Count_Type is a 32-bit type, so no overflow
-         --  can occur.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+      --  create a Last index value greater than Index_Type'Last.
+
+      if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
+         --  We perform a two-part test. First we determine whether the
+         --  computed Last value lies in the base range of the type, and then
+         --  determine whether it lies in the range of the index (sub)type.
+
+         --  Last must satisfy this relation:
+         --    First + Length - 1 <= Last
+         --  We regroup terms:
+         --    First - 1 <= Last - Length
+         --  Which can rewrite as:
+         --    No_Index <= Last - Length
+
+         if Index_Type'Base'Last - Index_Type'Base (Length) < No_Index then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We now know that the computed value of Last is within the base
+         --  range of the type, so it is safe to compute its value:
+
+         Last := No_Index + Index_Type'Base (Length);
+
+         --  Finally we test whether the value is within the range of the
+         --  generic actual index subtype:
 
-         if Index > Int (Index_Type'Last) then
+         if Last > Index_Type'Last then
             raise Constraint_Error with "Length is out of range";
          end if;
 
+      elsif Index_Type'First <= 0 then
+         --  Here we can compute Last directly, in the normal way. We know that
+         --  No_Index is less than 0, so there is no danger of overflow when
+         --  adding the (positive) value of Length.
+
+         Index := Count_Type'Base (No_Index) + Length;  -- same value as V.Last
+
+         if Index > Count_Type'Base (Index_Type'Last) then
+            raise Constraint_Error with "Length is out of range";
+         end if;
+
+         --  We know that the computed value (having type Count_Type) of Last
+         --  is within the range of the generic actual index subtype, so it is
+         --  safe to convert to Index_Type:
+
+         Last := Index_Type'Base (Index);
+
       else
-         --  If Index_Type'First is within Length of Int'Last, then overflow
-         --  would occur if we simply computed Last directly. So instead of
-         --  computing Last, and then determining whether its value is greater
-         --  than Index_Type'Last, we work backwards by computing the potential
-         --  First index value, and then checking whether that value is less
-         --  than Index_Type'First.
-         Index := Int (Index_Type'Last) - Int (Length) + 1;
+         --  Here Index_Type'First (and Index_Type'Last) is positive, so we
+         --  must test the length indirectly (by working backwards from the
+         --  largest possible value of Last), in order to prevent overflow.
+
+         Index := Count_Type'Base (Index_Type'Last) - Length;  -- No_Index
 
-         if Index < Int (Index_Type'First) then
+         if Index < Count_Type'Base (No_Index) then
             raise Constraint_Error with "Length is out of range";
          end if;
 
-         --  We have determined that Length would not create a Last index value
-         --  outside of the range of Index_Type, so we can now safely compute
-         --  its value.
-         Index := Int (Index_Type'First - 1) + Int (Length);
+         --  We have determined that the value of Length would not create a
+         --  Last index value outside of the range of Index_Type, so we can now
+         --  safely compute its value.
+
+         Last := Index_Type'Base (Count_Type'Base (No_Index) + Length);
       end if;
 
-      Last := Index_Type (Index);
       Elements := new Elements_Type'(Last, EA => (others => New_Item));
 
       return Vector'(Controlled with Elements, Last, 0, 0);
