Patchwork [Ada] Replaced 64-bit index manipulation with more efficient integer types

login
register
mail settings
Submitter Arnaud Charlet
Date June 22, 2010, 4:36 p.m.
Message ID <20100622163624.GA11758@adacore.com>
Download mbox | patch
Permalink /patch/56527/
State New
Headers show

Comments

Arnaud Charlet - June 22, 2010, 4:36 p.m.
Formerly, the vector containers used the widest integer type available on the
machine to perform intermediate calculations; typically this was a 64-bit type.
This prevented overflow that could occur using a generic actual index type
whose base range was too narrow. However, using the wider machine type is not
as efficient as the native type that corresponds to the generic actual.

The wide types were replaced by the wider of Index_Type'Base and
Length_Type'Base.  Determining which type is wider is done by comparing
Index_Type'Base'Last to Count_Type'Pos (Count_Type'Last). There is no run-time
cost for this check, since the comparison is done when the generic
instantiation is expanded into code, and unused branches are automatically
removed by the compiler.

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

2010-06-22  Matthew Heaney  <heaney@adacore.com>

	* a-convec.adb, a-coinve.adb: Removed 64-bit types Int and UInt.

Patch

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);