[multiple changes]

2013-04-11  Matthew Heaney  <heaney@adacore.com>

	* a-cdlili.adb, a-cidlli.adb, a-cbdlli.adb ("="): Increment
	lock counts before entering loop.
	(Find): Ditto.
	(Is_Sorted, Merge, Sort): Ditto.
	(Reverse_Find): Ditto.
	(Splice_Internal): Internal operation to refactor splicing logic.
	(Splice): Some logic moved into Splice_Internal.

2013-04-11  Johannes Kanig  <kanig@adacore.com>

	* adabkend.adb (Scan_Compiler_Arguments): Do not call
	Set_Output_Object_File_Name in Alfa_Mode
	* gnat1drv.adb (Adjust_Global_Switches): Take Alfa_Mode into account.
	* opt.ads: Fix documentation.

From-SVN: r197771

7 files changed, 1056 insertions, 307 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 051a222..0d54e5e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2013-04-11  Matthew Heaney  <heaney@adacore.com>
+
+	* a-cdlili.adb, a-cidlli.adb, a-cbdlli.adb ("="): Increment
+	lock counts before entering loop.
+	(Find): Ditto.
+	(Is_Sorted, Merge, Sort): Ditto.
+	(Reverse_Find): Ditto.
+	(Splice_Internal): Internal operation to refactor splicing logic.
+	(Splice): Some logic moved into Splice_Internal.
+
+2013-04-11  Johannes Kanig  <kanig@adacore.com>
+
+	* adabkend.adb (Scan_Compiler_Arguments): Do not call
+	Set_Output_Object_File_Name in Alfa_Mode
+	* gnat1drv.adb (Adjust_Global_Switches): Take Alfa_Mode into account.
+	* opt.ads: Fix documentation.
+
 2013-04-11  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb: Minor code reorganization and comment fixes.
diff --git a/gcc/ada/a-cbdlli.adb b/gcc/ada/a-cbdlli.adb
index 5db2d58..1c25022 100644
--- a/gcc/ada/a-cbdlli.adb
+++ b/gcc/ada/a-cbdlli.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2013, 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- --
@@ -80,6 +80,18 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
       Before    : Count_Type;
       New_Node  : Count_Type);
 
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Count_Type;
+      Source : in out List);
+
+   procedure Splice_Internal
+     (Target  : in out List;
+      Before  : Count_Type;
+      Source  : in out List;
+      Src_Pos : Count_Type;
+      Tgt_Pos : out Count_Type);
+
    function Vet (Position : Cursor) return Boolean;
    --  Checks invariants of the cursor and its designated container, as a
    --  simple way of detecting dangling references (see operation Free for a
@@ -92,10 +104,19 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
    ---------
 
    function "=" (Left, Right : List) return Boolean is
+      BL : Natural renames Left'Unrestricted_Access.Busy;
+      LL : Natural renames Left'Unrestricted_Access.Lock;
+
+      BR : Natural renames Right'Unrestricted_Access.Busy;
+      LR : Natural renames Right'Unrestricted_Access.Lock;
+
       LN : Node_Array renames Left.Nodes;
       RN : Node_Array renames Right.Nodes;
 
-      LI, RI : Count_Type;
+      LI : Count_Type;
+      RI : Count_Type;
+
+      Result : Boolean;
 
    begin
       if Left'Address = Right'Address then
@@ -106,18 +127,44 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
          return False;
       end if;
 
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      BL := BL + 1;
+      LL := LL + 1;
+
+      BR := BR + 1;
+      LR := LR + 1;
+
       LI := Left.First;
       RI := Right.First;
+      Result := True;
       for J in 1 .. Left.Length loop
          if LN (LI).Element /= RN (RI).Element then
-            return False;
+            Result := False;
+            exit;
          end if;
 
          LI := LN (LI).Next;
          RI := RN (RI).Next;
       end loop;
 
-      return True;
+      BL := BL - 1;
+      LL := LL - 1;
+
+      BR := BR - 1;
+      LR := LR - 1;
+
+      return Result;
+   exception
+      when others =>
+         BL := BL - 1;
+         LL := LL - 1;
+
+         BR := BR - 1;
+         LR := LR - 1;
+
+         raise;
    end "=";
 
    --------------
@@ -570,15 +617,43 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Find");
       end if;
 
-      while Node /= 0 loop
-         if Nodes (Node).Element = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Nodes (Node).Next;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Count_Type;
+
+      begin
+         B := B + 1;
+         L := L + 1;
 
-      return No_Element;
+         Result := 0;
+         while Node /= 0 loop
+            if Nodes (Node).Element = Item then
+               Result := Node;
+               exit;
+            end if;
+
+            Node := Nodes (Node).Next;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
+
+         if Result = 0 then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Find;
 
    -----------
@@ -753,19 +828,41 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
       ---------------
 
       function Is_Sorted (Container : List) return Boolean is
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
          Nodes : Node_Array renames Container.Nodes;
-         Node  : Count_Type := Container.First;
+         Node  : Count_Type;
+
+         Result : Boolean;
 
       begin
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         B := B + 1;
+         L := L + 1;
+
+         Node := Container.First;
+         Result := True;
          for J in 2 .. Container.Length loop
             if Nodes (Nodes (Node).Next).Element < Nodes (Node).Element then
-               return False;
+               Result := False;
+               exit;
             end if;
 
             Node := Nodes (Node).Next;
          end loop;
 
-         return True;
+         B := B - 1;
+         L := L - 1;
+
+         return Result;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
       end Is_Sorted;
 
       -----------
@@ -776,12 +873,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
         (Target : in out List;
          Source : in out List)
       is
-         LN     : Node_Array renames Target.Nodes;
-         RN     : Node_Array renames Source.Nodes;
-         LI, RI : Cursor;
-
       begin
-
          --  The semantics of Merge changed slightly per AI05-0021. It was
          --  originally the case that if Target and Source denoted the same
          --  container object, then the GNAT implementation of Merge did
@@ -799,6 +891,14 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
               "Target and Source denote same non-empty container";
          end if;
 
+         if Target.Length > Count_Type'Last - Source.Length then
+            raise Constraint_Error with "new length exceeds maximum";
+         end if;
+
+         if Target.Length + Source.Length > Target.Capacity then
+            raise Capacity_Error with "new length exceeds target capacity";
+         end if;
+
          if Target.Busy > 0 then
             raise Program_Error with
               "attempt to tamper with cursors of Target (list is busy)";
@@ -809,34 +909,69 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
               "attempt to tamper with cursors of Source (list is busy)";
          end if;
 
-         LI := First (Target);
-         RI := First (Source);
-         while RI.Node /= 0 loop
-            pragma Assert (RN (RI.Node).Next = 0
-                             or else not (RN (RN (RI.Node).Next).Element <
-                                          RN (RI.Node).Element));
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
 
-            if LI.Node = 0 then
-               Splice (Target, No_Element, Source);
-               return;
-            end if;
+         declare
+            TB : Natural renames Target.Busy;
+            TL : Natural renames Target.Lock;
 
-            pragma Assert (LN (LI.Node).Next = 0
-                             or else not (LN (LN (LI.Node).Next).Element <
-                                          LN (LI.Node).Element));
+            SB : Natural renames Source.Busy;
+            SL : Natural renames Source.Lock;
 
-            if RN (RI.Node).Element < LN (LI.Node).Element then
-               declare
-                  RJ : Cursor := RI;
-               begin
-                  RI.Node := RN (RI.Node).Next;
-                  Splice (Target, LI, Source, RJ);
-               end;
+            LN : Node_Array renames Target.Nodes;
+            RN : Node_Array renames Source.Nodes;
 
-            else
-               LI.Node := LN (LI.Node).Next;
-            end if;
-         end loop;
+            LI, LJ, RI, RJ : Count_Type;
+
+         begin
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            LI := Target.First;
+            RI := Source.First;
+            while RI /= 0 loop
+               pragma Assert (RN (RI).Next = 0
+                                or else not (RN (RN (RI).Next).Element <
+                                               RN (RI).Element));
+
+               if LI = 0 then
+                  Splice_Internal (Target, 0, Source);
+                  exit;
+               end if;
+
+               pragma Assert (LN (LI).Next = 0
+                                or else not (LN (LN (LI).Next).Element <
+                                               LN (LI).Element));
+
+               if RN (RI).Element < LN (LI).Element then
+                  RJ := RI;
+                  RI := RN (RI).Next;
+                  Splice_Internal (Target, LI, Source, RJ, LJ);
+
+               else
+                  LI := LN (LI).Next;
+               end if;
+            end loop;
+
+            TB := TB - 1;
+            TL := TL - 1;
+
+            SB := SB - 1;
+            SL := SL - 1;
+         exception
+            when others =>
+               TB := TB - 1;
+               TL := TL - 1;
+
+               SB := SB - 1;
+               SL := SL - 1;
+
+               raise;
+         end;
       end Merge;
 
       ----------
@@ -926,7 +1061,27 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
               "attempt to tamper with cursors (list is busy)";
          end if;
 
-         Sort (Front => 0, Back => 0);
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         declare
+            B : Natural renames Container.Busy;
+            L : Natural renames Container.Lock;
+
+         begin
+            B := B + 1;
+            L := L + 1;
+
+            Sort (Front => 0, Back => 0);
+
+            B := B - 1;
+            L := L - 1;
+         exception
+            when others =>
+               B := B - 1;
+               L := L - 1;
+               raise;
+         end;
 
          pragma Assert (N (Container.First).Prev = 0);
          pragma Assert (N (Container.Last).Next = 0);
@@ -1733,15 +1888,43 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
       end if;
 
-      while Node /= 0 loop
-         if Container.Nodes (Node).Element = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Container.Nodes (Node).Prev;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Count_Type;
 
-      return No_Element;
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Result := 0;
+         while Node /= 0 loop
+            if Container.Nodes (Node).Element = Item then
+               Result := Node;
+               exit;
+            end if;
+
+            Node := Container.Nodes (Node).Prev;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
+
+         if Result = 0 then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Reverse_Find;
 
    ---------------------
@@ -1800,9 +1983,6 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
          return;
       end if;
 
-      pragma Assert (Source.Nodes (Source.First).Prev = 0);
-      pragma Assert (Source.Nodes (Source.Last).Next = 0);
-
       if Target.Length > Count_Type'Last - Source.Length then
          raise Constraint_Error with "new length exceeds maximum";
       end if;
@@ -1821,10 +2001,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      while not Is_Empty (Source) loop
-         Insert (Target, Before, Source.Nodes (Source.First).Element);
-         Delete_First (Source);
-      end loop;
+      Splice_Internal (Target, Before.Node, Source);
    end Splice;
 
    procedure Splice
@@ -1937,7 +2114,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
       Source   : in out List;
       Position : in out Cursor)
    is
-      Target_Position : Cursor;
+      Target_Position : Count_Type;
 
    begin
       if Target'Address = Source'Address then
@@ -1979,16 +2156,139 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      Insert
-        (Container => Target,
-         Before    => Before,
-         New_Item  => Source.Nodes (Position.Node).Element,
-         Position  => Target_Position);
+      Splice_Internal
+        (Target  => Target,
+         Before  => Before.Node,
+         Source  => Source,
+         Src_Pos => Position.Node,
+         Tgt_Pos => Target_Position);
 
-      Delete (Source, Position);
-      Position := Target_Position;
+      Position := Cursor'(Target'Unrestricted_Access, Target_Position);
    end Splice;
 
+   ---------------------
+   -- Splice_Internal --
+   ---------------------
+
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Count_Type;
+      Source : in out List)
+   is
+      N : Node_Array renames Source.Nodes;
+      X : Count_Type;
+
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted, and corner-cases disposed of.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= 0);
+      pragma Assert (N (Source.First).Prev = 0);
+      pragma Assert (Source.Last /= 0);
+      pragma Assert (N (Source.Last).Next = 0);
+      pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+      pragma Assert (Target.Length + Source.Length <= Target.Capacity);
+
+      while Source.Length > 1 loop
+         --  Copy first element of Source onto Target
+
+         Allocate (Target, N (Source.First).Element, New_Node => X);
+         Insert_Internal (Target, Before => Before, New_Node => X);
+
+         --  Unlink the first node from Source
+
+         X := Source.First;
+         pragma Assert (N (N (X).Next).Prev = X);
+
+         Source.First := N (X).Next;
+         N (Source.First).Prev := 0;
+
+         Source.Length := Source.Length - 1;
+
+         --  Return the Source node to its free store
+
+         Free (Source, X);
+      end loop;
+
+      --  Copy first (and only remaining) element of Source onto Target
+
+      Allocate (Target, N (Source.First).Element, New_Node => X);
+      Insert_Internal (Target, Before => Before, New_Node => X);
+
+      --  Unlink the node from Source
+
+      X := Source.First;
+      pragma Assert (X = Source.Last);
+
+      Source.First := 0;
+      Source.Last := 0;
+
+      Source.Length := 0;
+
+      --  Return the Source node to its free store
+
+      Free (Source, X);
+   end Splice_Internal;
+
+   procedure Splice_Internal
+     (Target  : in out List;
+      Before  : Count_Type;  -- node of Target
+      Source  : in out List;
+      Src_Pos : Count_Type;  -- node of Source
+      Tgt_Pos : out Count_Type)
+   is
+      N : Node_Array renames Source.Nodes;
+
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted, and corner-cases handled.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Target.Length < Target.Capacity);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= 0);
+      pragma Assert (N (Source.First).Prev = 0);
+      pragma Assert (Source.Last /= 0);
+      pragma Assert (N (Source.Last).Next = 0);
+      pragma Assert (Src_Pos /= 0);
+
+      Allocate (Target, N (Src_Pos).Element, New_Node => Tgt_Pos);
+      Insert_Internal (Target, Before => Before, New_Node => Tgt_Pos);
+
+      if Source.Length = 1 then
+         pragma Assert (Source.First = Source.Last);
+         pragma Assert (Src_Pos = Source.First);
+
+         Source.First := 0;
+         Source.Last := 0;
+
+      elsif Src_Pos = Source.First then
+         pragma Assert (N (N (Src_Pos).Next).Prev = Src_Pos);
+
+         Source.First := N (Src_Pos).Next;
+         N (Source.First).Prev := 0;
+
+      elsif Src_Pos = Source.Last then
+         pragma Assert (N (N (Src_Pos).Prev).Next = Src_Pos);
+
+         Source.Last := N (Src_Pos).Prev;
+         N (Source.Last).Next := 0;
+
+      else
+         pragma Assert (Source.Length >= 3);
+         pragma Assert (N (N (Src_Pos).Next).Prev = Src_Pos);
+         pragma Assert (N (N (Src_Pos).Prev).Next = Src_Pos);
+
+         N (N (Src_Pos).Next).Prev := N (Src_Pos).Prev;
+         N (N (Src_Pos).Prev).Next := N (Src_Pos).Next;
+      end if;
+
+      Source.Length := Source.Length - 1;
+      Free (Source, Src_Pos);
+   end Splice_Internal;
+
    ----------
    -- Swap --
    ----------
diff --git a/gcc/ada/a-cdlili.adb b/gcc/ada/a-cdlili.adb
index 8234f32..2fedd3c 100644
--- a/gcc/ada/a-cdlili.adb
+++ b/gcc/ada/a-cdlili.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2013, 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- --
@@ -64,6 +64,17 @@ package body Ada.Containers.Doubly_Linked_Lists is
       Before    : Node_Access;
       New_Node  : Node_Access);
 
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Node_Access;
+      Source : in out List);
+
+   procedure Splice_Internal
+     (Target   : in out List;
+      Before   : Node_Access;
+      Source   : in out List;
+      Position : Node_Access);
+
    function Vet (Position : Cursor) return Boolean;
    --  Checks invariants of the cursor and its designated container, as a
    --  simple way of detecting dangling references (see operation Free for a
@@ -76,8 +87,15 @@ package body Ada.Containers.Doubly_Linked_Lists is
    ---------
 
    function "=" (Left, Right : List) return Boolean is
-      L : Node_Access := Left.First;
-      R : Node_Access := Right.First;
+      BL : Natural renames Left'Unrestricted_Access.Busy;
+      LL : Natural renames Left'Unrestricted_Access.Lock;
+
+      BR : Natural renames Right'Unrestricted_Access.Busy;
+      LR : Natural renames Right'Unrestricted_Access.Lock;
+
+      L      : Node_Access;
+      R      : Node_Access;
+      Result : Boolean;
 
    begin
       if Left'Address = Right'Address then
@@ -88,16 +106,44 @@ package body Ada.Containers.Doubly_Linked_Lists is
          return False;
       end if;
 
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      BL := BL + 1;
+      LL := LL + 1;
+
+      BR := BR + 1;
+      LR := LR + 1;
+
+      L := Left.First;
+      R := Right.First;
+      Result := True;
       for J in 1 .. Left.Length loop
          if L.Element /= R.Element then
-            return False;
+            Result := False;
+            exit;
          end if;
 
          L := L.Next;
          R := R.Next;
       end loop;
 
-      return True;
+      BL := BL - 1;
+      LL := LL - 1;
+
+      BR := BR - 1;
+      LR := LR - 1;
+
+      return Result;
+   exception
+      when others =>
+         BL := BL - 1;
+         LL := LL - 1;
+
+         BR := BR - 1;
+         LR := LR - 1;
+
+         raise;
    end "=";
 
    ------------
@@ -508,15 +554,43 @@ package body Ada.Containers.Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Find");
       end if;
 
-      while Node /= null loop
-         if Node.Element = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Node.Next;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Node_Access;
+
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Result := null;
+         while Node /= null loop
+            if Node.Element = Item then
+               Result := Node;
+               exit;
+            end if;
+
+            Node := Node.Next;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
 
-      return No_Element;
+         if Result = null then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Find;
 
    -----------
@@ -606,18 +680,39 @@ package body Ada.Containers.Doubly_Linked_Lists is
       ---------------
 
       function Is_Sorted (Container : List) return Boolean is
-         Node : Node_Access := Container.First;
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Node   : Node_Access;
+         Result : Boolean;
 
       begin
-         for I in 2 .. Container.Length loop
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         B := B + 1;
+         L := L + 1;
+
+         Node := Container.First;
+         Result := True;
+         for Idx in 2 .. Container.Length loop
             if Node.Next.Element < Node.Element then
-               return False;
+               Result := False;
+               exit;
             end if;
 
             Node := Node.Next;
          end loop;
 
-         return True;
+         B := B - 1;
+         L := L - 1;
+
+         return Result;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
       end Is_Sorted;
 
       -----------
@@ -628,10 +723,7 @@ package body Ada.Containers.Doubly_Linked_Lists is
         (Target : in out List;
          Source : in out List)
       is
-         LI, RI : Cursor;
-
       begin
-
          --  The semantics of Merge changed slightly per AI05-0021. It was
          --  originally the case that if Target and Source denoted the same
          --  container object, then the GNAT implementation of Merge did
@@ -649,6 +741,10 @@ package body Ada.Containers.Doubly_Linked_Lists is
               "Target and Source denote same non-empty container";
          end if;
 
+         if Target.Length > Count_Type'Last - Source.Length then
+            raise Constraint_Error with "new length exceeds maximum";
+         end if;
+
          if Target.Busy > 0 then
             raise Program_Error with
               "attempt to tamper with cursors of Target (list is busy)";
@@ -659,35 +755,64 @@ package body Ada.Containers.Doubly_Linked_Lists is
               "attempt to tamper with cursors of Source (list is busy)";
          end if;
 
-         LI := First (Target);
-         RI := First (Source);
-         while RI.Node /= null loop
-            pragma Assert (RI.Node.Next = null
-                             or else not (RI.Node.Next.Element <
-                                          RI.Node.Element));
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
 
-            if LI.Node = null then
-               Splice (Target, No_Element, Source);
-               return;
-            end if;
+         declare
+            TB : Natural renames Target.Busy;
+            TL : Natural renames Target.Lock;
 
-            pragma Assert (LI.Node.Next = null
-                             or else not (LI.Node.Next.Element <
-                                          LI.Node.Element));
+            SB : Natural renames Source.Busy;
+            SL : Natural renames Source.Lock;
 
-            if RI.Node.Element < LI.Node.Element then
-               declare
-                  RJ : Cursor := RI;
-                  pragma Warnings (Off, RJ);
-               begin
-                  RI.Node := RI.Node.Next;
-                  Splice (Target, LI, Source, RJ);
-               end;
+            LI, RI, RJ : Node_Access;
 
-            else
-               LI.Node := LI.Node.Next;
-            end if;
-         end loop;
+         begin
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            LI := Target.First;
+            RI := Source.First;
+            while RI /= null loop
+               pragma Assert (RI.Next = null
+                                or else not (RI.Next.Element < RI.Element));
+
+               if LI = null then
+                  Splice_Internal (Target, null, Source);
+                  exit;
+               end if;
+
+               pragma Assert (LI.Next = null
+                                or else not (LI.Next.Element < LI.Element));
+
+               if RI.Element < LI.Element then
+                  RJ := RI;
+                  RI := RI.Next;
+                  Splice_Internal (Target, LI, Source, RJ);
+
+               else
+                  LI := LI.Next;
+               end if;
+            end loop;
+
+            TB := TB - 1;
+            TL := TL - 1;
+
+            SB := SB - 1;
+            SL := SL - 1;
+         exception
+            when others =>
+               TB := TB - 1;
+               TL := TL - 1;
+
+               SB := SB - 1;
+               SL := SL - 1;
+
+               raise;
+         end;
       end Merge;
 
       ----------
@@ -773,7 +898,27 @@ package body Ada.Containers.Doubly_Linked_Lists is
               "attempt to tamper with cursors (list is busy)";
          end if;
 
-         Sort (Front => null, Back => null);
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         declare
+            B : Natural renames Container.Busy;
+            L : Natural renames Container.Lock;
+
+         begin
+            B := B + 1;
+            L := L + 1;
+
+            Sort (Front => null, Back => null);
+
+            B := B - 1;
+            L := L - 1;
+         exception
+            when others =>
+               B := B - 1;
+               L := L - 1;
+               raise;
+         end;
 
          pragma Assert (Container.First.Prev = null);
          pragma Assert (Container.Last.Next = null);
@@ -1533,15 +1678,43 @@ package body Ada.Containers.Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
       end if;
 
-      while Node /= null loop
-         if Node.Element = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Node.Prev;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Node_Access;
+
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Result := null;
+         while Node /= null loop
+            if Node.Element = Item then
+               Result := Node;
+               exit;
+            end if;
 
-      return No_Element;
+            Node := Node.Prev;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
+
+         if Result = null then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Reverse_Find;
 
    ---------------------
@@ -1600,9 +1773,6 @@ package body Ada.Containers.Doubly_Linked_Lists is
          return;
       end if;
 
-      pragma Assert (Source.First.Prev = null);
-      pragma Assert (Source.Last.Next = null);
-
       if Target.Length > Count_Type'Last - Source.Length then
          raise Constraint_Error with "new length exceeds maximum";
       end if;
@@ -1617,45 +1787,7 @@ package body Ada.Containers.Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      if Target.Length = 0 then
-         pragma Assert (Target.First = null);
-         pragma Assert (Target.Last = null);
-         pragma Assert (Before = No_Element);
-
-         Target.First := Source.First;
-         Target.Last := Source.Last;
-
-      elsif Before.Node = null then
-         pragma Assert (Target.Last.Next = null);
-
-         Target.Last.Next := Source.First;
-         Source.First.Prev := Target.Last;
-
-         Target.Last := Source.Last;
-
-      elsif Before.Node = Target.First then
-         pragma Assert (Target.First.Prev = null);
-
-         Source.Last.Next := Target.First;
-         Target.First.Prev := Source.Last;
-
-         Target.First := Source.First;
-
-      else
-         pragma Assert (Target.Length >= 2);
-
-         Before.Node.Prev.Next := Source.First;
-         Source.First.Prev := Before.Node.Prev;
-
-         Before.Node.Prev := Source.Last;
-         Source.Last.Next := Before.Node;
-      end if;
-
-      Source.First := null;
-      Source.Last := null;
-
-      Target.Length := Target.Length + Source.Length;
-      Source.Length := 0;
+      Splice_Internal (Target, Before.Node, Source);
    end Splice;
 
    procedure Splice
@@ -1806,10 +1938,95 @@ package body Ada.Containers.Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      if Position.Node = Source.First then
-         Source.First := Position.Node.Next;
+      Splice_Internal (Target, Before.Node, Source, Position.Node);
+      Position.Container := Target'Unchecked_Access;
+   end Splice;
+
+   ---------------------
+   -- Splice_Internal --
+   ---------------------
+
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Node_Access;
+      Source : in out List)
+   is
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted, and corner-cases disposed of.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= null);
+      pragma Assert (Source.First.Prev = null);
+      pragma Assert (Source.Last /= null);
+      pragma Assert (Source.Last.Next = null);
+      pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+
+      if Target.Length = 0 then
+         pragma Assert (Target.First = null);
+         pragma Assert (Target.Last = null);
+         pragma Assert (Before = null);
+
+         Target.First := Source.First;
+         Target.Last := Source.Last;
+
+      elsif Before = null then
+         pragma Assert (Target.Last.Next = null);
+
+         Target.Last.Next := Source.First;
+         Source.First.Prev := Target.Last;
+
+         Target.Last := Source.Last;
+
+      elsif Before = Target.First then
+         pragma Assert (Target.First.Prev = null);
+
+         Source.Last.Next := Target.First;
+         Target.First.Prev := Source.Last;
+
+         Target.First := Source.First;
+
+      else
+         pragma Assert (Target.Length >= 2);
+
+         Before.Prev.Next := Source.First;
+         Source.First.Prev := Before.Prev;
+
+         Before.Prev := Source.Last;
+         Source.Last.Next := Before;
+      end if;
+
+      Source.First := null;
+      Source.Last := null;
+
+      Target.Length := Target.Length + Source.Length;
+      Source.Length := 0;
+   end Splice_Internal;
+
+   procedure Splice_Internal
+     (Target   : in out List;
+      Before   : Node_Access;  -- node of Target
+      Source   : in out List;
+      Position : Node_Access)  -- node of Source
+   is
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Target.Length < Count_Type'Last);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= null);
+      pragma Assert (Source.First.Prev = null);
+      pragma Assert (Source.Last /= null);
+      pragma Assert (Source.Last.Next = null);
+      pragma Assert (Position /= null);
+
+      if Position = Source.First then
+         Source.First := Position.Next;
 
-         if Position.Node = Source.Last then
+         if Position = Source.Last then
             pragma Assert (Source.First = null);
             pragma Assert (Source.Length = 1);
             Source.Last := null;
@@ -1818,58 +2035,56 @@ package body Ada.Containers.Doubly_Linked_Lists is
             Source.First.Prev := null;
          end if;
 
-      elsif Position.Node = Source.Last then
+      elsif Position = Source.Last then
          pragma Assert (Source.Length >= 2);
-         Source.Last := Position.Node.Prev;
+         Source.Last := Position.Prev;
          Source.Last.Next := null;
 
       else
          pragma Assert (Source.Length >= 3);
-         Position.Node.Prev.Next := Position.Node.Next;
-         Position.Node.Next.Prev := Position.Node.Prev;
+         Position.Prev.Next := Position.Next;
+         Position.Next.Prev := Position.Prev;
       end if;
 
       if Target.Length = 0 then
          pragma Assert (Target.First = null);
          pragma Assert (Target.Last = null);
-         pragma Assert (Before = No_Element);
+         pragma Assert (Before = null);
 
-         Target.First := Position.Node;
-         Target.Last := Position.Node;
+         Target.First := Position;
+         Target.Last := Position;
 
          Target.First.Prev := null;
          Target.Last.Next := null;
 
-      elsif Before.Node = null then
+      elsif Before = null then
          pragma Assert (Target.Last.Next = null);
-         Target.Last.Next := Position.Node;
-         Position.Node.Prev := Target.Last;
+         Target.Last.Next := Position;
+         Position.Prev := Target.Last;
 
-         Target.Last := Position.Node;
+         Target.Last := Position;
          Target.Last.Next := null;
 
-      elsif Before.Node = Target.First then
+      elsif Before = Target.First then
          pragma Assert (Target.First.Prev = null);
-         Target.First.Prev := Position.Node;
-         Position.Node.Next := Target.First;
+         Target.First.Prev := Position;
+         Position.Next := Target.First;
 
-         Target.First := Position.Node;
+         Target.First := Position;
          Target.First.Prev := null;
 
       else
          pragma Assert (Target.Length >= 2);
-         Before.Node.Prev.Next := Position.Node;
-         Position.Node.Prev := Before.Node.Prev;
+         Before.Prev.Next := Position;
+         Position.Prev := Before.Prev;
 
-         Before.Node.Prev := Position.Node;
-         Position.Node.Next := Before.Node;
+         Before.Prev := Position;
+         Position.Next := Before;
       end if;
 
       Target.Length := Target.Length + 1;
       Source.Length := Source.Length - 1;
-
-      Position.Container := Target'Unchecked_Access;
-   end Splice;
+   end Splice_Internal;
 
    ----------
    -- Swap --
diff --git a/gcc/ada/a-cidlli.adb b/gcc/ada/a-cidlli.adb
index 7d5e22e..458df26 100644
--- a/gcc/ada/a-cidlli.adb
+++ b/gcc/ada/a-cidlli.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2013, 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- --
@@ -67,6 +67,17 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
       Before    : Node_Access;
       New_Node  : Node_Access);
 
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Node_Access;
+      Source : in out List);
+
+   procedure Splice_Internal
+     (Target   : in out List;
+      Before   : Node_Access;
+      Source   : in out List;
+      Position : Node_Access);
+
    function Vet (Position : Cursor) return Boolean;
    --  Checks invariants of the cursor and its designated container, as a
    --  simple way of detecting dangling references (see operation Free for a
@@ -79,8 +90,15 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
    ---------
 
    function "=" (Left, Right : List) return Boolean is
-      L : Node_Access;
-      R : Node_Access;
+      BL : Natural renames Left'Unrestricted_Access.Busy;
+      LL : Natural renames Left'Unrestricted_Access.Lock;
+
+      BR : Natural renames Right'Unrestricted_Access.Busy;
+      LR : Natural renames Right'Unrestricted_Access.Lock;
+
+      L      : Node_Access;
+      R      : Node_Access;
+      Result : Boolean;
 
    begin
       if Left'Address = Right'Address then
@@ -91,18 +109,44 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
          return False;
       end if;
 
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      BL := BL + 1;
+      LL := LL + 1;
+
+      BR := BR + 1;
+      LR := LR + 1;
+
       L := Left.First;
       R := Right.First;
+      Result := True;
       for J in 1 .. Left.Length loop
          if L.Element.all /= R.Element.all then
-            return False;
+            Result := False;
+            exit;
          end if;
 
          L := L.Next;
          R := R.Next;
       end loop;
 
-      return True;
+      BL := BL - 1;
+      LL := LL - 1;
+
+      BR := BR - 1;
+      LR := LR - 1;
+
+      return Result;
+   exception
+      when others =>
+         BL := BL - 1;
+         LL := LL - 1;
+
+         BR := BR - 1;
+         LR := LR - 1;
+
+         raise;
    end "=";
 
    ------------
@@ -549,15 +593,43 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Find");
       end if;
 
-      while Node /= null loop
-         if Node.Element.all = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Node.Next;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Node_Access;
+
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Result := null;
+         while Node /= null loop
+            if Node.Element.all = Item then
+               Result := Node;
+               exit;
+            end if;
 
-      return No_Element;
+            Node := Node.Next;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
+
+         if Result = null then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Find;
 
    -----------
@@ -660,18 +732,39 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
       ---------------
 
       function Is_Sorted (Container : List) return Boolean is
-         Node : Node_Access := Container.First;
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Node   : Node_Access;
+         Result : Boolean;
 
       begin
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         B := B + 1;
+         L := L + 1;
+
+         Node := Container.First;
+         Result := True;
          for I in 2 .. Container.Length loop
             if Node.Next.Element.all < Node.Element.all then
-               return False;
+               Result := False;
+               exit;
             end if;
 
             Node := Node.Next;
          end loop;
 
-         return True;
+         B := B - 1;
+         L := L - 1;
+
+         return Result;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
       end Is_Sorted;
 
       -----------
@@ -682,10 +775,7 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
         (Target : in out List;
          Source : in out List)
       is
-         LI, RI : Cursor;
-
       begin
-
          --  The semantics of Merge changed slightly per AI05-0021. It was
          --  originally the case that if Target and Source denoted the same
          --  container object, then the GNAT implementation of Merge did
@@ -703,6 +793,10 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
               "Target and Source denote same non-empty container";
          end if;
 
+         if Target.Length > Count_Type'Last - Source.Length then
+            raise Constraint_Error with "new length exceeds maximum";
+         end if;
+
          if Target.Busy > 0 then
             raise Program_Error with
               "attempt to tamper with cursors of Target (list is busy)";
@@ -713,35 +807,63 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
               "attempt to tamper with cursors of Source (list is busy)";
          end if;
 
-         LI := First (Target);
-         RI := First (Source);
-         while RI.Node /= null loop
-            pragma Assert (RI.Node.Next = null
-                             or else not (RI.Node.Next.Element.all <
-                                          RI.Node.Element.all));
+         declare
+            TB : Natural renames Target.Busy;
+            TL : Natural renames Target.Lock;
 
-            if LI.Node = null then
-               Splice (Target, No_Element, Source);
-               return;
-            end if;
+            SB : Natural renames Source.Busy;
+            SL : Natural renames Source.Lock;
 
-            pragma Assert (LI.Node.Next = null
-                             or else not (LI.Node.Next.Element.all <
-                                          LI.Node.Element.all));
-
-            if RI.Node.Element.all < LI.Node.Element.all then
-               declare
-                  RJ : Cursor := RI;
-                  pragma Warnings (Off, RJ);
-               begin
-                  RI.Node := RI.Node.Next;
-                  Splice (Target, LI, Source, RJ);
-               end;
-
-            else
-               LI.Node := LI.Node.Next;
-            end if;
-         end loop;
+            LI, RI, RJ : Node_Access;
+
+         begin
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            LI := Target.First;
+            RI := Source.First;
+            while RI /= null loop
+               pragma Assert (RI.Next = null
+                                or else not (RI.Next.Element.all <
+                                               RI.Element.all));
+
+               if LI = null then
+                  Splice_Internal (Target, null, Source);
+                  exit;
+               end if;
+
+               pragma Assert (LI.Next = null
+                                or else not (LI.Next.Element.all <
+                                               LI.Element.all));
+
+               if RI.Element.all < LI.Element.all then
+                  RJ := RI;
+                  RI := RI.Next;
+                  Splice_Internal (Target, LI, Source, RJ);
+
+               else
+                  LI := LI.Next;
+               end if;
+            end loop;
+
+            TB := TB - 1;
+            TL := TL - 1;
+
+            SB := SB - 1;
+            SL := SL - 1;
+         exception
+            when others =>
+               TB := TB - 1;
+               TL := TL - 1;
+
+               SB := SB - 1;
+               SL := SL - 1;
+
+               raise;
+         end;
       end Merge;
 
       ----------
@@ -825,7 +947,27 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
               "attempt to tamper with cursors (list is busy)";
          end if;
 
-         Sort (Front => null, Back => null);
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
+
+         declare
+            B : Natural renames Container.Busy;
+            L : Natural renames Container.Lock;
+
+         begin
+            B := B + 1;
+            L := L + 1;
+
+            Sort (Front => null, Back => null);
+
+            B := B - 1;
+            L := L - 1;
+         exception
+            when others =>
+               B := B - 1;
+               L := L - 1;
+               raise;
+         end;
 
          pragma Assert (Container.First.Prev = null);
          pragma Assert (Container.Last.Next = null);
@@ -1600,15 +1742,43 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
          pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
       end if;
 
-      while Node /= null loop
-         if Node.Element.all = Item then
-            return Cursor'(Container'Unrestricted_Access, Node);
-         end if;
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
 
-         Node := Node.Prev;
-      end loop;
+      declare
+         B : Natural renames Container'Unrestricted_Access.Busy;
+         L : Natural renames Container'Unrestricted_Access.Lock;
+
+         Result : Node_Access;
+
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Result := null;
+         while Node /= null loop
+            if Node.Element.all = Item then
+               Result := Node;
+               exit;
+            end if;
 
-      return No_Element;
+            Node := Node.Prev;
+         end loop;
+
+         B := B - 1;
+         L := L - 1;
+
+         if Result = null then
+            return No_Element;
+         else
+            return Cursor'(Container'Unrestricted_Access, Result);
+         end if;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+            raise;
+      end;
    end Reverse_Find;
 
    ---------------------
@@ -1673,9 +1843,6 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
          return;
       end if;
 
-      pragma Assert (Source.First.Prev = null);
-      pragma Assert (Source.Last.Next = null);
-
       if Target.Length > Count_Type'Last - Source.Length then
          raise Constraint_Error with "new length exceeds maximum";
       end if;
@@ -1690,44 +1857,7 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      if Target.Length = 0 then
-         pragma Assert (Before = No_Element);
-         pragma Assert (Target.First = null);
-         pragma Assert (Target.Last = null);
-
-         Target.First := Source.First;
-         Target.Last := Source.Last;
-
-      elsif Before.Node = null then
-         pragma Assert (Target.Last.Next = null);
-
-         Target.Last.Next := Source.First;
-         Source.First.Prev := Target.Last;
-
-         Target.Last := Source.Last;
-
-      elsif Before.Node = Target.First then
-         pragma Assert (Target.First.Prev = null);
-
-         Source.Last.Next := Target.First;
-         Target.First.Prev := Source.Last;
-
-         Target.First := Source.First;
-
-      else
-         pragma Assert (Target.Length >= 2);
-         Before.Node.Prev.Next := Source.First;
-         Source.First.Prev := Before.Node.Prev;
-
-         Before.Node.Prev := Source.Last;
-         Source.Last.Next := Before.Node;
-      end if;
-
-      Source.First := null;
-      Source.Last := null;
-
-      Target.Length := Target.Length + Source.Length;
-      Source.Length := 0;
+      Splice_Internal (Target, Before.Node, Source);
    end Splice;
 
    procedure Splice
@@ -1901,10 +2031,94 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      if Position.Node = Source.First then
-         Source.First := Position.Node.Next;
+      Splice_Internal (Target, Before.Node, Source, Position.Node);
+      Position.Container := Target'Unchecked_Access;
+   end Splice;
+
+   ---------------------
+   -- Splice_Internal --
+   ---------------------
+
+   procedure Splice_Internal
+     (Target : in out List;
+      Before : Node_Access;
+      Source : in out List)
+   is
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted, and corner-cases disposed of.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= null);
+      pragma Assert (Source.First.Prev = null);
+      pragma Assert (Source.Last /= null);
+      pragma Assert (Source.Last.Next = null);
+      pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+
+      if Target.Length = 0 then
+         pragma Assert (Before = null);
+         pragma Assert (Target.First = null);
+         pragma Assert (Target.Last = null);
+
+         Target.First := Source.First;
+         Target.Last := Source.Last;
+
+      elsif Before = null then
+         pragma Assert (Target.Last.Next = null);
+
+         Target.Last.Next := Source.First;
+         Source.First.Prev := Target.Last;
+
+         Target.Last := Source.Last;
+
+      elsif Before = Target.First then
+         pragma Assert (Target.First.Prev = null);
+
+         Source.Last.Next := Target.First;
+         Target.First.Prev := Source.Last;
+
+         Target.First := Source.First;
+
+      else
+         pragma Assert (Target.Length >= 2);
+         Before.Prev.Next := Source.First;
+         Source.First.Prev := Before.Prev;
+
+         Before.Prev := Source.Last;
+         Source.Last.Next := Before;
+      end if;
+
+      Source.First := null;
+      Source.Last := null;
+
+      Target.Length := Target.Length + Source.Length;
+      Source.Length := 0;
+   end Splice_Internal;
+
+   procedure Splice_Internal
+     (Target   : in out List;
+      Before   : Node_Access;  -- node of Target
+      Source   : in out List;
+      Position : Node_Access)  -- node of Source
+   is
+   begin
+      --  This implements the corresponding Splice operation, after the
+      --  parameters have been vetted.
+
+      pragma Assert (Target'Address /= Source'Address);
+      pragma Assert (Target.Length < Count_Type'Last);
+      pragma Assert (Source.Length > 0);
+      pragma Assert (Source.First /= null);
+      pragma Assert (Source.First.Prev = null);
+      pragma Assert (Source.Last /= null);
+      pragma Assert (Source.Last.Next = null);
+      pragma Assert (Position /= null);
+
+      if Position = Source.First then
+         Source.First := Position.Next;
 
-         if Position.Node = Source.Last then
+         if Position = Source.Last then
             pragma Assert (Source.First = null);
             pragma Assert (Source.Length = 1);
             Source.Last := null;
@@ -1913,58 +2127,56 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
             Source.First.Prev := null;
          end if;
 
-      elsif Position.Node = Source.Last then
+      elsif Position = Source.Last then
          pragma Assert (Source.Length >= 2);
-         Source.Last := Position.Node.Prev;
+         Source.Last := Position.Prev;
          Source.Last.Next := null;
 
       else
          pragma Assert (Source.Length >= 3);
-         Position.Node.Prev.Next := Position.Node.Next;
-         Position.Node.Next.Prev := Position.Node.Prev;
+         Position.Prev.Next := Position.Next;
+         Position.Next.Prev := Position.Prev;
       end if;
 
       if Target.Length = 0 then
-         pragma Assert (Before = No_Element);
+         pragma Assert (Before = null);
          pragma Assert (Target.First = null);
          pragma Assert (Target.Last = null);
 
-         Target.First := Position.Node;
-         Target.Last := Position.Node;
+         Target.First := Position;
+         Target.Last := Position;
 
          Target.First.Prev := null;
          Target.Last.Next := null;
 
-      elsif Before.Node = null then
+      elsif Before = null then
          pragma Assert (Target.Last.Next = null);
-         Target.Last.Next := Position.Node;
-         Position.Node.Prev := Target.Last;
+         Target.Last.Next := Position;
+         Position.Prev := Target.Last;
 
-         Target.Last := Position.Node;
+         Target.Last := Position;
          Target.Last.Next := null;
 
-      elsif Before.Node = Target.First then
+      elsif Before = Target.First then
          pragma Assert (Target.First.Prev = null);
-         Target.First.Prev := Position.Node;
-         Position.Node.Next := Target.First;
+         Target.First.Prev := Position;
+         Position.Next := Target.First;
 
-         Target.First := Position.Node;
+         Target.First := Position;
          Target.First.Prev := null;
 
       else
          pragma Assert (Target.Length >= 2);
-         Before.Node.Prev.Next := Position.Node;
-         Position.Node.Prev := Before.Node.Prev;
+         Before.Prev.Next := Position;
+         Position.Prev := Before.Prev;
 
-         Before.Node.Prev := Position.Node;
-         Position.Node.Next := Before.Node;
+         Before.Prev := Position;
+         Position.Next := Before;
       end if;
 
       Target.Length := Target.Length + 1;
       Source.Length := Source.Length - 1;
-
-      Position.Container := Target'Unchecked_Access;
-   end Splice;
+   end Splice_Internal;
 
    ----------
    -- Swap --
diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb
index 96bd00d..e808762 100644
--- a/gcc/ada/adabkend.adb
+++ b/gcc/ada/adabkend.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2001-2011, AdaCore                     --
+--                     Copyright (C) 2001-2013, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -234,6 +234,8 @@ package body Adabkend is
             then
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
+               elsif Alfa_Mode then
+                  Output_File_Name_Seen := True;
                else
                   Set_Output_Object_File_Name (Argv);
                   Output_File_Name_Seen := True;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index cd0d650..69d37ad 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -293,7 +293,10 @@ procedure Gnat1drv is
          Formal_Extensions := True;
       end if;
 
-      if Debug_Flag_Dot_FF then
+      --  Alfa_Mode is activated by default in the gnat2why executable, but
+      --  can also be activated using the -gnatd.F switch.
+
+      if Debug_Flag_Dot_FF or else Alfa_Mode then
          Alfa_Mode := True;
 
          --  Set strict standard interpretation of compiler permissions
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 5e80dc7..5653c76 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1982,7 +1982,7 @@ package Opt is
    Alfa_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification through the
    --  generation of Why code for those parts of the input code that belong to
-   --  the Alfa subset of Ada. Set by debug flag -gnatd.F.
+   --  the Alfa subset of Ada. Set by the gnat2why executable.
 
    Frame_Condition_Mode : Boolean := False;
    --  Specific mode to be used in combination with Alfa_Mode. If set to