[multiple changes]

2014-02-19  Matthew Heaney  <heaney@adacore.com>

	* a-chtgop.ads (Checked_Index): New operation.
	(Next): Changed mode of hash table.
	* a-chtgop.adb (Adjust, Delete_Node_Sans_Free): Detect tampering
	(Generic_Read, Reserve_Capacity): Ditto.
	(Generic_Equal): Detect tampering.
	(Next): Changed mode of hash table, detect tampering.
	* a-chtgke.ads (Checked_Index, Checked_Equivalent_Keys): New
	operation.
	(Find): Changed mode of hash table.
	* a-chtgke.adb (Checked_Equivalent_Keys): New operation
	(Delete_Key_Sans_Free, Generic_Conditional_Insert): Detect
	tampering.
	(Find): Changed mode of hash table, check for tampering.
	(Generic_Replace_Element): Check for tampering.
	* a-chtgbk.ads (Checked_Index, Checked_Equivalent_Keys): New operation.
	* a-chtgbk.adb (Checked_Index, Checked_Equivalent_Keys): New
	operation (Delete_Key_Sans_Free, Generic_Conditional_Insert):
	Detect tampering.
	(Find, Generic_Replace_Element): Check for tampering.
	* a-chtgbo.ads (Checked_Index): New operation.
	* a-chtgbo.adb (Checked_Index): New operation
	(Delete_Node_Sans_Free, Generic_Equal): Detect tampering.
	(Generic_Read, Next): Ditto.
	* a-cohase.adb, a-cihase.adb (Is_In): Changed mode of hash
	table (Difference, Intersection): Use variable view of
	source, detect tampering (Find, Is_Subset, Overlap): Use
	variable view of container (Symmetric_Difference, Union):
	Detect tampering (Vet): Use Checked_Index to detect tampering
	(Constant_Reference, Element, Find): Use variable view of
	container.
	(Update_Element_Preserving_Key): Detect tampering.
	* a-cbhase.adb (Difference, Find, Is_In): Use variable view
	of container.
	(Is_Subset): Ditto.
	(Equivalent_Sets, Overlap): Use Node's Next component.
	(Vet): Use Checked_Index to detect tampering.
	(Constant_Reference, Element, Find): Use variable view of container.
	(Update_Element_Preserving_Key): Detect tampering.
	* a-cohama.adb, a-cihama.adb, a-cbhama.adb (Constant_Reference,
	Element, Find): Use variable view of container.
	(Reference): Rename hash table component.
	(Vet): Use Checked_Index to detect tampering.

2014-02-19  Arnaud Charlet  <charlet@adacore.com>

	* adabkend.adb (Scan_Compiler_Arguments): Add missing handling
	of -nostdinc.

2014-02-19  Thomas Quinot  <quinot@adacore.com>

	* tbuild.adb (New_Occurrence_Of, New_Rerefence_To): Guard
	against calls without Def_Id.

2014-02-19  Claire Dross  <dross@adacore.com>

	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
	a-cofove.ads: Add global annotations to subprograms.

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): Remove
	constants Errors, Pack_Id and Pack_Init. Remove variable Vars.
	Initial_Condition no longer requires the presence of pragma
	Initialized. Do not try to diagnose whether all variables mentioned in
	pragma Initializes also appear in Initial_Condition.
	(Collect_Variables): Removed.
	(Match_Variable): Removed.
	(Match_Variables): Removed.
	(Report_Unused_Variables): Removed.

2014-02-19  Thomas Quinot  <quinot@adacore.com>

	* gnat_rm.texi (pragma Stream_Convert): Minor rewording.

From-SVN: r207905

gcc/ada/ChangeLog

+2014-02-19  Matthew Heaney  <heaney@adacore.com>
+
+	* a-chtgop.ads (Checked_Index): New operation.
+	(Next): Changed mode of hash table.
+	* a-chtgop.adb (Adjust, Delete_Node_Sans_Free): Detect tampering
+	(Generic_Read, Reserve_Capacity): Ditto.
+	(Generic_Equal): Detect tampering.
+	(Next): Changed mode of hash table, detect tampering.
+	* a-chtgke.ads (Checked_Index, Checked_Equivalent_Keys): New
+	operation.
+	(Find): Changed mode of hash table.
+	* a-chtgke.adb (Checked_Equivalent_Keys): New operation
+	(Delete_Key_Sans_Free, Generic_Conditional_Insert): Detect
+	tampering.
+	(Find): Changed mode of hash table, check for tampering.
+	(Generic_Replace_Element): Check for tampering.
+	* a-chtgbk.ads (Checked_Index, Checked_Equivalent_Keys): New operation.
+	* a-chtgbk.adb (Checked_Index, Checked_Equivalent_Keys): New
+	operation (Delete_Key_Sans_Free, Generic_Conditional_Insert):
+	Detect tampering.
+	(Find, Generic_Replace_Element): Check for tampering.
+	* a-chtgbo.ads (Checked_Index): New operation.
+	* a-chtgbo.adb (Checked_Index): New operation
+	(Delete_Node_Sans_Free, Generic_Equal): Detect tampering.
+	(Generic_Read, Next): Ditto.
+	* a-cohase.adb, a-cihase.adb (Is_In): Changed mode of hash
+	table (Difference, Intersection): Use variable view of
+	source, detect tampering (Find, Is_Subset, Overlap): Use
+	variable view of container (Symmetric_Difference, Union):
+	Detect tampering (Vet): Use Checked_Index to detect tampering
+	(Constant_Reference, Element, Find): Use variable view of
+	container.
+	(Update_Element_Preserving_Key): Detect tampering.
+	* a-cbhase.adb (Difference, Find, Is_In): Use variable view
+	of container.
+	(Is_Subset): Ditto.
+	(Equivalent_Sets, Overlap): Use Node's Next component.
+	(Vet): Use Checked_Index to detect tampering.
+	(Constant_Reference, Element, Find): Use variable view of container.
+	(Update_Element_Preserving_Key): Detect tampering.
+	* a-cohama.adb, a-cihama.adb, a-cbhama.adb (Constant_Reference,
+	Element, Find): Use variable view of container.
+	(Reference): Rename hash table component.
+	(Vet): Use Checked_Index to detect tampering.
+
+2014-02-19  Arnaud Charlet  <charlet@adacore.com>
+
+	* adabkend.adb (Scan_Compiler_Arguments): Add missing handling
+	of -nostdinc.
+
+2014-02-19  Thomas Quinot  <quinot@adacore.com>
+
+	* tbuild.adb (New_Occurrence_Of, New_Rerefence_To): Guard
+	against calls without Def_Id.
+
+2014-02-19  Claire Dross  <dross@adacore.com>
+
+	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
+	a-cofove.ads: Add global annotations to subprograms.
+
+2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): Remove
+	constants Errors, Pack_Id and Pack_Init. Remove variable Vars.
+	Initial_Condition no longer requires the presence of pragma
+	Initialized. Do not try to diagnose whether all variables mentioned in
+	pragma Initializes also appear in Initial_Condition.
+	(Collect_Variables): Removed.
+	(Match_Variable): Removed.
+	(Match_Variables): Removed.
+	(Report_Unused_Variables): Removed.
+
+2014-02-19  Thomas Quinot  <quinot@adacore.com>
+
+	* gnat_rm.texi (pragma Stream_Convert): Minor rewording.
+
 2014-02-19  Robert Dewar  <dewar@adacore.com>
 
 	* sem_util.adb, sem_util.ads, prj-conf.adb, s-os_lib.adb: Minor

gcc/ada/a-cbhama.adb

@@ -208,7 +208,8 @@ package body Ada.Containers.Bounded_Hashed_Maps is
      (Container : aliased Map;
       Key       : Key_Type) return Constant_Reference_Type
    is
-      Node : constant Count_Type := Key_Ops.Find (Container, Key);
+      Node : constant Count_Type :=
+               Key_Ops.Find (Container'Unrestricted_Access.all, Key);
 
    begin
       if Node = 0 then
@@ -321,7 +322,8 @@ package body Ada.Containers.Bounded_Hashed_Maps is
    -------------
 
    function Element (Container : Map; Key : Key_Type) return Element_Type is
-      Node : constant Count_Type := Key_Ops.Find (Container, Key);
+      Node : constant Count_Type :=
+               Key_Ops.Find (Container'Unrestricted_Access.all, Key);
 
    begin
       if Node = 0 then
@@ -449,7 +451,8 @@ package body Ada.Containers.Bounded_Hashed_Maps is
    ----------
 
    function Find (Container : Map; Key : Key_Type) return Cursor is
-      Node : constant Count_Type := Key_Ops.Find (Container, Key);
+      Node : constant Count_Type :=
+               Key_Ops.Find (Container'Unrestricted_Access.all, Key);
    begin
       if Node = 0 then
          return No_Element;
@@ -1160,7 +1163,8 @@ package body Ada.Containers.Bounded_Hashed_Maps is
             return False;
          end if;
 
-         X := M.Buckets (Key_Ops.Index (M, M.Nodes (Position.Node).Key));
+         X := M.Buckets (Key_Ops.Checked_Index
+                          (M, M.Nodes (Position.Node).Key));
 
          for J in 1 .. M.Length loop
             if X = Position.Node then

gcc/ada/a-cbhase.adb

@@ -328,6 +328,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
    is
       Tgt_Node, Src_Node : Count_Type;
 
+      Src : Set renames Source'Unrestricted_Access.all;
+
       TN : Nodes_Type renames Target.Nodes;
       SN : Nodes_Type renames Source.Nodes;
 
@@ -356,7 +358,7 @@ package body Ada.Containers.Bounded_Hashed_Sets is
                HT_Ops.Free (Target, Tgt_Node);
             end if;
 
-            Src_Node := HT_Ops.Next (Source, Src_Node);
+            Src_Node := HT_Ops.Next (Src, Src_Node);
          end loop;
 
       else
@@ -481,7 +483,7 @@ package body Ada.Containers.Bounded_Hashed_Sets is
                return True;
             end if;
 
-            R_Node := HT_Ops.Next (R_HT, R_Node);
+            R_Node := Next (R_HT.Nodes (R_Node));
          end loop;
       end Find_Equivalent_Key;
 
@@ -512,6 +514,20 @@ package body Ada.Containers.Bounded_Hashed_Sets is
       pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
       pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
 
+      --  AI05-0022 requires that a container implementation detect element
+      --  tampering by a generic actual subprogram. However, the following case
+      --  falls outside the scope of that AI. Randy Brukardt explained on the
+      --  ARG list on 2013/02/07 that:
+
+      --  (Begin Quote):
+      --  But for an operation like "<" [the ordered set analog of
+      --  Equivalent_Elements], there is no need to "dereference" a cursor
+      --  after the call to the generic formal parameter function, so nothing
+      --  bad could happen if tampering is undetected. And the operation can
+      --  safely return a result without a problem even if an element is
+      --  deleted from the container.
+      --  (End Quote).
+
       declare
          LN : Node_Type renames Left.Container.Nodes (Left.Node);
          RN : Node_Type renames Right.Container.Nodes (Right.Node);
@@ -609,7 +625,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
      (Container : Set;
       Item      : Element_Type) return Cursor
    is
-      Node : constant Count_Type := Element_Keys.Find (Container, Item);
+      Node : constant Count_Type :=
+               Element_Keys.Find (Container'Unrestricted_Access.all, Item);
    begin
       return (if Node = 0 then No_Element
               else Cursor'(Container'Unrestricted_Access, Node));
@@ -865,7 +882,7 @@ package body Ada.Containers.Bounded_Hashed_Sets is
 
    function Is_In (HT : Set; Key : Node_Type) return Boolean is
    begin
-      return Element_Keys.Find (HT, Key.Element) /= 0;
+      return Element_Keys.Find (HT'Unrestricted_Access.all, Key.Element) /= 0;
    end Is_In;
 
    ---------------
@@ -890,7 +907,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
          if not Is_In (Of_Set, SN (Subset_Node)) then
             return False;
          end if;
-         Subset_Node := HT_Ops.Next (Subset, Subset_Node);
+         Subset_Node := HT_Ops.Next
+                          (Subset'Unrestricted_Access.all, Subset_Node);
       end loop;
 
       return True;
@@ -1049,7 +1067,7 @@ package body Ada.Containers.Bounded_Hashed_Sets is
          if Is_In (Right, Left.Nodes (Left_Node)) then
             return True;
          end if;
-         Left_Node := HT_Ops.Next (Left, Left_Node);
+         Left_Node := HT_Ops.Next (Left'Unrestricted_Access.all, Left_Node);
       end loop;
 
       return False;
@@ -1481,7 +1499,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
             return False;
          end if;
 
-         X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element));
+         X := S.Buckets (Element_Keys.Checked_Index
+                           (S, N (Position.Node).Element));
 
          for J in 1 .. S.Length loop
             if X = Position.Node then
@@ -1585,7 +1604,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
         (Container : aliased Set;
          Key       : Key_Type) return Constant_Reference_Type
       is
-         Node : constant Count_Type := Key_Keys.Find (Container, Key);
+         Node : constant Count_Type :=
+                  Key_Keys.Find (Container'Unrestricted_Access.all, Key);
 
       begin
          if Node = 0 then
@@ -1639,11 +1659,12 @@ package body Ada.Containers.Bounded_Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Element_Type
       is
-         Node : constant Count_Type := Key_Keys.Find (Container, Key);
+         Node : constant Count_Type :=
+                  Key_Keys.Find (Container'Unrestricted_Access.all, Key);
 
       begin
          if Node = 0 then
-            raise Constraint_Error with "key not in map";  --  ??? "set"
+            raise Constraint_Error with "key not in set";
          end if;
 
          return Container.Nodes (Node).Element;
@@ -1683,7 +1704,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Cursor
       is
-         Node : constant Count_Type := Key_Keys.Find (Container, Key);
+         Node : constant Count_Type :=
+                  Key_Keys.Find (Container'Unrestricted_Access.all, Key);
       begin
          return (if Node = 0 then No_Element
                  else Cursor'(Container'Unrestricted_Access, Node));
@@ -1825,9 +1847,8 @@ package body Ada.Containers.Bounded_Hashed_Sets is
            (Vet (Position),
             "bad cursor in Update_Element_Preserving_Key");
 
-         --  Record bucket now, in case key is changed
-
-         Indx := HT_Ops.Index (Container.Buckets, N (Position.Node));
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
 
          declare
             E : Element_Type renames N (Position.Node).Element;
@@ -1836,12 +1857,19 @@ package body Ada.Containers.Bounded_Hashed_Sets is
             B : Natural renames Container.Busy;
             L : Natural renames Container.Lock;
 
+            Eq : Boolean;
+
          begin
             B := B + 1;
             L := L + 1;
 
             begin
+               --  Record bucket now, in case key is changed
+               Indx := HT_Ops.Index (Container.Buckets, N (Position.Node));
+
                Process (E);
+
+               Eq := Equivalent_Keys (K, Key (E));
             exception
                when others =>
                   L := L - 1;
@@ -1852,8 +1880,7 @@ package body Ada.Containers.Bounded_Hashed_Sets is
             L := L - 1;
             B := B - 1;
 
-            if Equivalent_Keys (K, Key (E)) then
-               pragma Assert (Hash (K) = Hash (E));
+            if Eq then
                return;
             end if;
          end;

gcc/ada/a-cfdlli.ads

@@ -77,24 +77,31 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : List) return Boolean;
+   function "=" (Left, Right : List) return Boolean with
+     Global => null;
 
-   function Length (Container : List) return Count_Type;
+   function Length (Container : List) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : List) return Boolean;
+   function Is_Empty (Container : List) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out List);
+   procedure Clear (Container : in out List) with
+     Global => null;
 
    procedure Assign (Target : in out List; Source : List) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    function Copy (Source : List; Capacity : Count_Type := 0) return List with
+     Global => null,
      Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
 
    function Element
      (Container : List;
       Position : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -102,9 +109,11 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out List; Source : in out List) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
@@ -113,6 +122,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -124,6 +134,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Position  : out Cursor;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -134,6 +145,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Position  : out Cursor;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -143,6 +155,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity;
 
    procedure Append
@@ -150,6 +163,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity;
 
    procedure Delete
@@ -157,28 +171,36 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Position  : in out Cursor;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Delete_First
      (Container : in out List;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Global => null;
 
    procedure Delete_Last
      (Container : in out List;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Global => null;
 
-   procedure Reverse_Elements (Container : in out List);
+   procedure Reverse_Elements (Container : in out List) with
+     Global => null;
 
    procedure Swap
      (Container : in out List;
       I, J      : Cursor)
    with
+     Global => null,
      Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
 
    procedure Swap_Links
      (Container : in out List;
       I, J      : Cursor)
    with
+     Global => null,
      Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
 
    procedure Splice
@@ -186,6 +208,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Before : Cursor;
       Source : in out List)
    with
+     Global => null,
      Pre    => Length (Source) + Length (Target) <= Target.Capacity
                  and then (Has_Element (Target, Before)
                             or else Before = No_Element);
@@ -196,6 +219,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Source   : in out List;
       Position : in out Cursor)
    with
+     Global => null,
      Pre    => Length (Source) + Length (Target) <= Target.Capacity
                  and then (Has_Element (Target, Before)
                             or else Before = No_Element)
@@ -206,31 +230,40 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Before    : Cursor;
       Position  : Cursor)
    with
+     Global => null,
      Pre    => 2 * Length (Container) <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element)
                  and then Has_Element (Container, Position);
 
-   function First (Container : List) return Cursor;
+   function First (Container : List) return Cursor with
+     Global => null;
 
    function First_Element (Container : List) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
-   function Last (Container : List) return Cursor;
+   function Last (Container : List) return Cursor with
+     Global => null;
 
    function Last_Element (Container : List) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Next (Container : List; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : List; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Previous (Container : List; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Previous (Container : List; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find
@@ -238,6 +271,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Item      : Element_Type;
       Position  : Cursor := No_Element) return Cursor
    with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Reverse_Find
@@ -245,34 +279,45 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
       Item      : Element_Type;
       Position  : Cursor := No_Element) return Cursor
    with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Contains
      (Container : List;
-      Item      : Element_Type) return Boolean;
+      Item      : Element_Type) return Boolean
+   with
+     Global => null;
 
-   function Has_Element (Container : List; Position : Cursor) return Boolean;
+   function Has_Element (Container : List; Position : Cursor) return Boolean
+   with
+     Global => null;
 
    generic
       with function "<" (Left, Right : Element_Type) return Boolean is <>;
    package Generic_Sorting is
 
-      function Is_Sorted (Container : List) return Boolean;
+      function Is_Sorted (Container : List) return Boolean with
+        Global => null;
 
-      procedure Sort (Container : in out List);
+      procedure Sort (Container : in out List) with
+        Global => null;
 
-      procedure Merge (Target, Source : in out List);
+      procedure Merge (Target, Source : in out List) with
+        Global => null;
 
    end Generic_Sorting;
 
-   function Strict_Equal (Left, Right : List) return Boolean;
+   function Strict_Equal (Left, Right : List) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : List; Position : Cursor) return List with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : List; Position : Cursor) return List with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all

gcc/ada/a-cfhama.ads

@@ -81,29 +81,37 @@ package Ada.Containers.Formal_Hashed_Maps is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Map) return Boolean;
+   function "=" (Left, Right : Map) return Boolean with
+     Global => null;
 
-   function Capacity (Container : Map) return Count_Type;
+   function Capacity (Container : Map) return Count_Type with
+     Global => null;
 
    procedure Reserve_Capacity
      (Container : in out Map;
       Capacity  : Count_Type)
    with
+     Global => null,
      Pre    => Capacity <= Container.Capacity;
 
-   function Length (Container : Map) return Count_Type;
+   function Length (Container : Map) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : Map) return Boolean;
+   function Is_Empty (Container : Map) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Map);
+   procedure Clear (Container : in out Map) with
+     Global => null;
 
    procedure Assign (Target : in out Map; Source : Map) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    function Copy
      (Source   : Map;
       Capacity : Count_Type := 0) return Map
    with
+     Global => null,
      Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
    --  Copy returns a container stricty equal to Source. It must have
    --  the same cursors associated with each element. Therefore:
@@ -111,12 +119,14 @@ package Ada.Containers.Formal_Hashed_Maps is
    --  - the modulus cannot be changed.
 
    function Key (Container : Map; Position : Cursor) return Key_Type with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    function Element
      (Container : Map;
       Position  : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -124,9 +134,11 @@ package Ada.Containers.Formal_Hashed_Maps is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Map; Source : in out Map) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
@@ -136,6 +148,7 @@ package Ada.Containers.Formal_Hashed_Maps is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Insert
@@ -143,6 +156,7 @@ package Ada.Containers.Formal_Hashed_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (not Contains (Container, Key));
 
@@ -151,6 +165,7 @@ package Ada.Containers.Formal_Hashed_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Replace
@@ -158,59 +173,81 @@ package Ada.Containers.Formal_Hashed_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Contains (Container, Key);
 
-   procedure Exclude (Container : in out Map; Key : Key_Type);
+   procedure Exclude (Container : in out Map; Key : Key_Type) with
+     Global => null;
 
    procedure Delete (Container : in out Map; Key : Key_Type) with
+     Global => null,
      Pre    => Contains (Container, Key);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
-   function First (Container : Map) return Cursor;
+   function First (Container : Map) return Cursor with
+     Global => null;
 
    function Next (Container : Map; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Map; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Find (Container : Map; Key : Key_Type) return Cursor;
+   function Find (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
-   function Contains (Container : Map; Key : Key_Type) return Boolean;
+   function Contains (Container : Map; Key : Key_Type) return Boolean with
+     Global => null;
 
    function Element (Container : Map; Key : Key_Type) return Element_Type with
+     Global => null,
      Pre    => Contains (Container, Key);
 
-   function Has_Element (Container : Map; Position : Cursor) return Boolean;
+   function Has_Element (Container : Map; Position : Cursor) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Keys
      (Left   : Map;
       CLeft  : Cursor;
       Right  : Map;
-      CRight : Cursor) return Boolean;
+      CRight : Cursor) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Keys
      (Left  : Map;
       CLeft : Cursor;
-      Right : Key_Type) return Boolean;
+      Right : Key_Type) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Keys
      (Left   : Key_Type;
       Right  : Map;
-      CRight : Cursor) return Boolean;
+      CRight : Cursor) return Boolean
+   with
+     Global => null;
 
-   function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+   function Default_Modulus (Capacity : Count_Type) return Hash_Type with
+     Global => null;
 
-   function Strict_Equal (Left, Right : Map) return Boolean;
+   function Strict_Equal (Left, Right : Map) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : Map; Position : Cursor) return Map with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Map; Position : Cursor) return Map with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all
@@ -219,7 +256,8 @@ package Ada.Containers.Formal_Hashed_Maps is
    --  iterate over containers. Left returns the part of the container already
    --  scanned and Right the part not scanned yet.
 
-   function Overlap (Left, Right : Map) return Boolean;
+   function Overlap (Left, Right : Map) return Boolean with
+     Global => null;
    --  Overlap returns True if the containers have common keys
 
 private

gcc/ada/a-cfhase.ads

@@ -83,39 +83,50 @@ package Ada.Containers.Formal_Hashed_Sets is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Set) return Boolean;
+   function "=" (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function Equivalent_Sets (Left, Right : Set) return Boolean;
+   function Equivalent_Sets (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function To_Set (New_Item : Element_Type) return Set;
+   function To_Set (New_Item : Element_Type) return Set with
+     Global => null;
 
-   function Capacity (Container : Set) return Count_Type;
+   function Capacity (Container : Set) return Count_Type with
+     Global => null;
 
    procedure Reserve_Capacity
      (Container : in out Set;
       Capacity  : Count_Type)
    with
+     Global => null,
      Pre    => Capacity <= Container.Capacity;
 
-   function Length (Container : Set) return Count_Type;
+   function Length (Container : Set) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : Set) return Boolean;
+   function Is_Empty (Container : Set) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Set);
+   procedure Clear (Container : in out Set) with
+     Global => null;
 
    procedure Assign (Target : in out Set; Source : Set) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    function Copy
      (Source   : Set;
       Capacity : Count_Type := 0) return Set
    with
+     Global => null,
      Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
 
    function Element
      (Container : Set;
       Position  : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -123,9 +134,11 @@ package Ada.Containers.Formal_Hashed_Sets is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Set; Source : in out Set) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
@@ -134,85 +147,123 @@ package Ada.Containers.Formal_Hashed_Sets is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Insert  (Container : in out Set; New_Item : Element_Type) with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (not Contains (Container, New_Item));
 
    procedure Include (Container : in out Set; New_Item : Element_Type) with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Replace (Container : in out Set; New_Item : Element_Type) with
+     Global => null,
      Pre    => Contains (Container, New_Item);
 
-   procedure Exclude (Container : in out Set; Item     : Element_Type);
+   procedure Exclude (Container : in out Set; Item     : Element_Type) with
+     Global => null;
 
    procedure Delete  (Container : in out Set; Item     : Element_Type) with
+     Global => null,
      Pre    => Contains (Container, Item);
 
    procedure Delete (Container : in out Set; Position  : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Union (Target : in out Set; Source : Set) with
+     Global => null,
      Pre    => Length (Target) + Length (Source) -
                  Length (Intersection (Target, Source)) <= Target.Capacity;
 
-   function Union (Left, Right : Set) return Set;
+   function Union (Left, Right : Set) return Set with
+     Global => null,
+     Pre    => Length (Left) + Length (Right) -
+                 Length (Intersection (Left, Right)) <= Count_Type'Last;
 
    function "or" (Left, Right : Set) return Set renames Union;
 
-   procedure Intersection (Target : in out Set; Source : Set);
+   procedure Intersection (Target : in out Set; Source : Set) with
+     Global => null;
 
-   function Intersection (Left, Right : Set) return Set;
+   function Intersection (Left, Right : Set) return Set with
+     Global => null;
 
    function "and" (Left, Right : Set) return Set renames Intersection;
 
-   procedure Difference (Target : in out Set; Source : Set);
+   procedure Difference (Target : in out Set; Source : Set) with
+     Global => null;
 
-   function Difference (Left, Right : Set) return Set;
+   function Difference (Left, Right : Set) return Set with
+     Global => null;
 
    function "-" (Left, Right : Set) return Set renames Difference;
 
-   procedure Symmetric_Difference (Target : in out Set; Source : Set);
+   procedure Symmetric_Difference (Target : in out Set; Source : Set) with
+     Global => null,
+     Pre    => Length (Target) + Length (Source) -
+                 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
 
-   function Symmetric_Difference (Left, Right : Set) return Set;
+   function Symmetric_Difference (Left, Right : Set) return Set with
+     Global => null,
+     Pre    => Length (Left) + Length (Right) -
+                 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
 
    function "xor" (Left, Right : Set) return Set
      renames Symmetric_Difference;
 
-   function Overlap (Left, Right : Set) return Boolean;
+   function Overlap (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
+     Global => null;
 
-   function First (Container : Set) return Cursor;
+   function First (Container : Set) return Cursor with
+     Global => null;
 
    function Next (Container : Set; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Set; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find
      (Container : Set;
-      Item      : Element_Type) return Cursor;
+      Item      : Element_Type) return Cursor
+   with
+     Global => null;
 
-   function Contains (Container : Set; Item : Element_Type) return Boolean;
+   function Contains (Container : Set; Item : Element_Type) return Boolean with
+     Global => null;
 
-   function Has_Element (Container : Set; Position : Cursor) return Boolean;
+   function Has_Element (Container : Set; Position : Cursor) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Elements (Left  : Set; CLeft : Cursor;
-                                 Right : Set; CRight : Cursor) return Boolean;
+                                 Right : Set; CRight : Cursor) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Elements
      (Left  : Set; CLeft : Cursor;
-      Right : Element_Type) return Boolean;
+      Right : Element_Type) return Boolean
+   with
+     Global => null;
 
    function Equivalent_Elements
      (Left  : Element_Type;
-      Right : Set; CRight : Cursor) return Boolean;
+      Right : Set; CRight : Cursor) return Boolean
+   with
+     Global => null;
 
-   function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+   function Default_Modulus (Capacity : Count_Type) return Hash_Type with
+     Global => null;
 
    generic
       type Key_Type (<>) is private;
@@ -225,33 +276,45 @@ package Ada.Containers.Formal_Hashed_Sets is
 
    package Generic_Keys is
 
-      function Key (Container : Set; Position : Cursor) return Key_Type;
+      function Key (Container : Set; Position : Cursor) return Key_Type with
+        Global => null;
 
-      function Element (Container : Set; Key : Key_Type) return Element_Type;
+      function Element (Container : Set; Key : Key_Type) return Element_Type
+      with
+          Global => null;
 
       procedure Replace
         (Container : in out Set;
          Key       : Key_Type;
-         New_Item  : Element_Type);
+         New_Item  : Element_Type)
+      with
+          Global => null;
 
-      procedure Exclude (Container : in out Set; Key : Key_Type);
+      procedure Exclude (Container : in out Set; Key : Key_Type) with
+        Global => null;
 
-      procedure Delete (Container : in out Set; Key : Key_Type);
+      procedure Delete (Container : in out Set; Key : Key_Type) with
+        Global => null;
 
-      function Find (Container : Set; Key : Key_Type) return Cursor;
+      function Find (Container : Set; Key : Key_Type) return Cursor with
+        Global => null;
 
-      function Contains (Container : Set; Key : Key_Type) return Boolean;
+      function Contains (Container : Set; Key : Key_Type) return Boolean with
+        Global => null;
 
    end Generic_Keys;
 
-   function Strict_Equal (Left, Right : Set) return Boolean;
+   function Strict_Equal (Left, Right : Set) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : Set; Position : Cursor) return Set with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Set; Position : Cursor) return Set with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all

gcc/ada/a-cforma.ads

@@ -68,7 +68,8 @@ package Ada.Containers.Formal_Ordered_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
-   function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+   function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
+     Global => null;
 
    type Map (Capacity : Count_Type) is private with
      Iterable => (First       => First,
@@ -84,27 +85,35 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Map) return Boolean;
+   function "=" (Left, Right : Map) return Boolean with
+     Global => null;
 
-   function Length (Container : Map) return Count_Type;
+   function Length (Container : Map) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : Map) return Boolean;
+   function Is_Empty (Container : Map) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Map);
+   procedure Clear (Container : in out Map) with
+     Global => null;
 
    procedure Assign (Target : in out Map; Source : Map) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
+     Global => null,
      Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
 
    function Key (Container : Map; Position : Cursor) return Key_Type with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    function Element
      (Container : Map;
       Position  : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -112,9 +121,11 @@ package Ada.Containers.Formal_Ordered_Maps is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Map; Source : in out Map) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
@@ -124,6 +135,7 @@ package Ada.Containers.Formal_Ordered_Maps is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Insert
@@ -131,6 +143,7 @@ package Ada.Containers.Formal_Ordered_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (not Contains (Container, Key));
 
@@ -139,6 +152,7 @@ package Ada.Containers.Formal_Ordered_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Replace
@@ -146,69 +160,95 @@ package Ada.Containers.Formal_Ordered_Maps is
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Contains (Container, Key);
 
-   procedure Exclude (Container : in out Map; Key : Key_Type);
+   procedure Exclude (Container : in out Map; Key : Key_Type) with
+     Global => null;
 
    procedure Delete (Container : in out Map; Key : Key_Type) with
+     Global => null,
      Pre    => Contains (Container, Key);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
-   procedure Delete_First (Container : in out Map);
+   procedure Delete_First (Container : in out Map) with
+     Global => null;
 
-   procedure Delete_Last (Container : in out Map);
+   procedure Delete_Last (Container : in out Map) with
+     Global => null;
 
-   function First (Container : Map) return Cursor;
+   function First (Container : Map) return Cursor with
+     Global => null;
 
    function First_Element (Container : Map) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function First_Key (Container : Map) return Key_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
-   function Last (Container : Map) return Cursor;
+   function Last (Container : Map) return Cursor with
+     Global => null;
 
    function Last_Element (Container : Map) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Last_Key (Container : Map) return Key_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Next (Container : Map; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Map; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Previous (Container : Map; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Previous (Container : Map; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Find (Container : Map; Key : Key_Type) return Cursor;
+   function Find (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
    function Element (Container : Map; Key : Key_Type) return Element_Type with
+     Global => null,
      Pre    => Contains (Container, Key);
 
-   function Floor (Container : Map; Key : Key_Type) return Cursor;
+   function Floor (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
-   function Ceiling (Container : Map; Key : Key_Type) return Cursor;
+   function Ceiling (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
-   function Contains (Container : Map; Key : Key_Type) return Boolean;
+   function Contains (Container : Map; Key : Key_Type) return Boolean with
+     Global => null;
 
-   function Has_Element (Container : Map; Position : Cursor) return Boolean;
+   function Has_Element (Container : Map; Position : Cursor) return Boolean
+   with
+     Global => null;
 
-   function Strict_Equal (Left, Right : Map) return Boolean;
+   function Strict_Equal (Left, Right : Map) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : Map; Position : Cursor) return Map with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Map; Position : Cursor) return Map with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all
@@ -217,7 +257,8 @@ package Ada.Containers.Formal_Ordered_Maps is
    --  iterate over containers. Left returns the part of the container already
    --  scanned and Right the part not scanned yet.
 
-   function Overlap (Left, Right : Map) return Boolean;
+   function Overlap (Left, Right : Map) return Boolean with
+     Global => null;
    --  Overlap returns True if the containers have common keys
 private
 

gcc/ada/a-cforse.ads

@@ -66,7 +66,9 @@ package Ada.Containers.Formal_Ordered_Sets is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
-   function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
+   function Equivalent_Elements (Left, Right : Element_Type) return Boolean
+   with
+     Global => null;
 
    type Set (Capacity : Count_Type) is private with
      Iterable => (First       => First,
@@ -82,28 +84,36 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Set) return Boolean;
+   function "=" (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function Equivalent_Sets (Left, Right : Set) return Boolean;
+   function Equivalent_Sets (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function To_Set (New_Item : Element_Type) return Set;
+   function To_Set (New_Item : Element_Type) return Set with
+     Global => null;
 
-   function Length (Container : Set) return Count_Type;
+   function Length (Container : Set) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : Set) return Boolean;
+   function Is_Empty (Container : Set) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Set);
+   procedure Clear (Container : in out Set) with
+     Global => null;
 
    procedure Assign (Target : in out Set; Source : Set) with
      Pre => Target.Capacity >= Length (Source);
 
    function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
+     Global => null,
      Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
 
    function Element
      (Container : Set;
       Position  : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -111,9 +121,11 @@ package Ada.Containers.Formal_Ordered_Sets is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Set; Source : in out Set) with
+     Global => null,
      Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
@@ -122,12 +134,14 @@ package Ada.Containers.Formal_Ordered_Sets is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Set;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (not Contains (Container, New_Item));
 
@@ -135,95 +149,132 @@ package Ada.Containers.Formal_Ordered_Sets is
      (Container : in out Set;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Replace
      (Container : in out Set;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Contains (Container, New_Item);
 
    procedure Exclude
      (Container : in out Set;
-      Item      : Element_Type);
+      Item      : Element_Type)
+   with
+     Global => null;
 
    procedure Delete
      (Container : in out Set;
       Item      : Element_Type)
    with
+     Global => null,
      Pre    => Contains (Container, Item);
 
    procedure Delete
      (Container : in out Set;
       Position  : in out Cursor)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
-   procedure Delete_First (Container : in out Set);
+   procedure Delete_First (Container : in out Set) with
+     Global => null;
 
-   procedure Delete_Last (Container : in out Set);
+   procedure Delete_Last (Container : in out Set) with
+     Global => null;
 
    procedure Union (Target : in out Set; Source : Set) with
+     Global => null,
      Pre    => Length (Target) + Length (Source) -
                  Length (Intersection (Target, Source)) <= Target.Capacity;
 
-   function Union (Left, Right : Set) return Set;
+   function Union (Left, Right : Set) return Set with
+     Global => null,
+     Pre    => Length (Left) + Length (Right) -
+                 Length (Intersection (Left, Right)) <= Count_Type'Last;
 
    function "or" (Left, Right : Set) return Set renames Union;
 
-   procedure Intersection (Target : in out Set; Source : Set);
+   procedure Intersection (Target : in out Set; Source : Set) with
+     Global => null;
 
-   function Intersection (Left, Right : Set) return Set;
+   function Intersection (Left, Right : Set) return Set with
+     Global => null;
 
    function "and" (Left, Right : Set) return Set renames Intersection;
 
-   procedure Difference (Target : in out Set; Source : Set);
+   procedure Difference (Target : in out Set; Source : Set) with
+     Global => null;
 
-   function Difference (Left, Right : Set) return Set;
+   function Difference (Left, Right : Set) return Set with
+     Global => null;
 
    function "-" (Left, Right : Set) return Set renames Difference;
 
-   procedure Symmetric_Difference (Target : in out Set; Source : Set);
+   procedure Symmetric_Difference (Target : in out Set; Source : Set) with
+     Global => null,
+     Pre    => Length (Target) + Length (Source) -
+                 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
 
-   function Symmetric_Difference (Left, Right : Set) return Set;
+   function Symmetric_Difference (Left, Right : Set) return Set with
+     Global => null,
+     Pre    => Length (Left) + Length (Right) -
+                 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
 
    function "xor" (Left, Right : Set) return Set renames Symmetric_Difference;
 
-   function Overlap (Left, Right : Set) return Boolean;
+   function Overlap (Left, Right : Set) return Boolean with
+     Global => null;
 
-   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
+     Global => null;
 
-   function First (Container : Set) return Cursor;
+   function First (Container : Set) return Cursor with
+     Global => null;
 
    function First_Element (Container : Set) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Last (Container : Set) return Cursor;
 
    function Last_Element (Container : Set) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Next (Container : Set; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Set; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Previous (Container : Set; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Previous (Container : Set; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Find (Container : Set; Item : Element_Type) return Cursor;
+   function Find (Container : Set; Item : Element_Type) return Cursor with
+     Global => null;
 
-   function Floor (Container : Set; Item : Element_Type) return Cursor;
+   function Floor (Container : Set; Item : Element_Type) return Cursor with
+     Global => null;
 
-   function Ceiling (Container : Set; Item : Element_Type) return Cursor;
+   function Ceiling (Container : Set; Item : Element_Type) return Cursor with
+     Global => null;
 
-   function Contains (Container : Set; Item : Element_Type) return Boolean;
+   function Contains (Container : Set; Item : Element_Type) return Boolean with
+     Global => null;
 
-   function Has_Element (Container : Set; Position : Cursor) return Boolean;
+   function Has_Element (Container : Set; Position : Cursor) return Boolean
+   with
+     Global => null;
 
    generic
       type Key_Type (<>) is private;
@@ -234,39 +285,54 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    package Generic_Keys is
 
-      function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+      function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
+        Global => null;
 
-      function Key (Container : Set; Position : Cursor) return Key_Type;
+      function Key (Container : Set; Position : Cursor) return Key_Type with
+        Global => null;
 
-      function Element (Container : Set; Key : Key_Type) return Element_Type;
+      function Element (Container : Set; Key : Key_Type) return Element_Type
+      with
+        Global => null;
 
       procedure Replace
         (Container : in out Set;
          Key       : Key_Type;
-         New_Item  : Element_Type);
+         New_Item  : Element_Type)
+      with
+        Global => null;
 
-      procedure Exclude (Container : in out Set; Key : Key_Type);
+      procedure Exclude (Container : in out Set; Key : Key_Type) with
+        Global => null;
 
-      procedure Delete (Container : in out Set; Key : Key_Type);
+      procedure Delete (Container : in out Set; Key : Key_Type) with
+        Global => null;
 
-      function Find (Container : Set; Key : Key_Type) return Cursor;
+      function Find (Container : Set; Key : Key_Type) return Cursor with
+        Global => null;
 
-      function Floor (Container : Set; Key : Key_Type) return Cursor;
+      function Floor (Container : Set; Key : Key_Type) return Cursor with
+        Global => null;
 
-      function Ceiling (Container : Set; Key : Key_Type) return Cursor;
+      function Ceiling (Container : Set; Key : Key_Type) return Cursor with
+        Global => null;
 
-      function Contains (Container : Set; Key : Key_Type) return Boolean;
+      function Contains (Container : Set; Key : Key_Type) return Boolean with
+        Global => null;
 
    end Generic_Keys;
 
-   function Strict_Equal (Left, Right : Set) return Boolean;
+   function Strict_Equal (Left, Right : Set) return Boolean with
+        Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : Set; Position : Cursor) return Set with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Set; Position : Cursor) return Set with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all

gcc/ada/a-chtgbk.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2010, 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- --
@@ -29,6 +29,69 @@
 
 package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
 
+   -----------------------------
+   -- Checked_Equivalent_Keys --
+   -----------------------------
+
+   function Checked_Equivalent_Keys
+     (HT   : aliased in out Hash_Table_Type'Class;
+      Key  : Key_Type;
+      Node : Count_Type) return Boolean
+   is
+      Result : Boolean;
+
+      B : Natural renames HT.Busy;
+      L : Natural renames HT.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := Equivalent_Keys (Key, HT.Nodes (Node));
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Equivalent_Keys;
+
+   -------------------
+   -- Checked_Index --
+   -------------------
+
+   function Checked_Index
+     (HT  : aliased in out Hash_Table_Type'Class;
+      Key : Key_Type) return Hash_Type
+   is
+      Result : Hash_Type;
+
+      B : Natural renames HT.Busy;
+      L : Natural renames HT.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Index;
+
    --------------------------
    -- Delete_Key_Sans_Free --
    --------------------------
@@ -47,14 +110,22 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
          return;
       end if;
 
-      Indx := Index (HT, Key);
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      if HT.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with cursors (container is busy)";
+      end if;
+
+      Indx := Checked_Index (HT, Key);
       X := HT.Buckets (Indx);
 
       if X = 0 then
          return;
       end if;
 
-      if Equivalent_Keys (Key, HT.Nodes (X)) then
+      if Checked_Equivalent_Keys (HT, Key, X) then
          if HT.Busy > 0 then
             raise Program_Error with
               "attempt to tamper with cursors (container is busy)";
@@ -72,7 +143,7 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
             return;
          end if;
 
-         if Equivalent_Keys (Key, HT.Nodes (X)) then
+         if Checked_Equivalent_Keys (HT, Key, X) then
             if HT.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with cursors (container is busy)";
@@ -100,11 +171,13 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
          return 0;
       end if;
 
-      Indx := Index (HT, Key);
+      Indx := Checked_Index (HT'Unrestricted_Access.all, Key);
 
       Node := HT.Buckets (Indx);
       while Node /= 0 loop
-         if Equivalent_Keys (Key, HT.Nodes (Node)) then
+         if Checked_Equivalent_Keys
+           (HT'Unrestricted_Access.all, Key, Node)
+         then
             return Node;
          end if;
          Node := Next (HT.Nodes (Node));
@@ -123,16 +196,21 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
       Node     : out Count_Type;
       Inserted : out Boolean)
    is
-      Indx : constant Hash_Type := Index (HT, Key);
-      B    : Count_Type renames HT.Buckets (Indx);
+      Indx : Hash_Type;
 
    begin
-      if B = 0 then
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
       if HT.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with cursors (container is busy)";
       end if;
 
+      Indx := Checked_Index (HT, Key);
+      Node := HT.Buckets (Indx);
+
+      if Node = 0 then
          if HT.Length = HT.Capacity then
             raise Capacity_Error with "no more capacity for insertion";
          end if;
@@ -142,15 +220,14 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
 
          Inserted := True;
 
-         B := Node;
+         HT.Buckets (Indx) := Node;
          HT.Length := HT.Length + 1;
 
          return;
       end if;
 
-      Node := B;
       loop
-         if Equivalent_Keys (Key, HT.Nodes (Node)) then
+         if Checked_Equivalent_Keys (HT, Key, Node) then
             Inserted := False;
             return;
          end if;
@@ -160,35 +237,19 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
          exit when Node = 0;
       end loop;
 
-      if HT.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with cursors (container is busy)";
-      end if;
-
       if HT.Length = HT.Capacity then
          raise Capacity_Error with "no more capacity for insertion";
       end if;
 
       Node := New_Node;
-      Set_Next (HT.Nodes (Node), Next => B);
+      Set_Next (HT.Nodes (Node), Next => HT.Buckets (Indx));
 
       Inserted := True;
 
-      B := Node;
+      HT.Buckets (Indx) := Node;
       HT.Length := HT.Length + 1;
    end Generic_Conditional_Insert;
 
-   -----------
-   -- Index --
-   -----------
-
-   function Index
-     (HT  : Hash_Table_Type'Class;
-      Key : Key_Type) return Hash_Type is
-   begin
-      return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
-   end Index;
-
    -----------------------------
    -- Generic_Replace_Element --
    -----------------------------
@@ -204,24 +265,41 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
       BB : Buckets_Type renames HT.Buckets;
       NN : Nodes_Type renames HT.Nodes;
 
-      Old_Hash : constant Hash_Type := Hash (NN (Node));
-      Old_Indx : constant Hash_Type := BB'First + Old_Hash mod BB'Length;
-
-      New_Hash : constant Hash_Type := Hash (Key);
-      New_Indx : constant Hash_Type := BB'First + New_Hash mod BB'Length;
+      Old_Indx : Hash_Type;
+      New_Indx : constant Hash_Type := Checked_Index (HT, Key);
 
       New_Bucket : Count_Type renames BB (New_Indx);
       N, M       : Count_Type;
 
    begin
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      declare
+         B : Natural renames HT.Busy;
+         L : Natural renames HT.Lock;
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Old_Indx := Hash (NN (Node)) mod HT.Buckets'Length;
+
+         B := B - 1;
+         L := L - 1;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
+
+            raise;
+      end;
+
       --  Replace_Element is allowed to change a node's key to Key
       --  (generic formal operation Assign provides the mechanism), but
       --  only if Key is not already in the hash table. (In a unique-key
       --  hash table as this one, a key is mapped to exactly one node.)
 
-      if Equivalent_Keys (Key, NN (Node)) then
-         pragma Assert (New_Hash = Old_Hash);
-
+      if Checked_Equivalent_Keys (HT, Key, Node) then
          if HT.Lock > 0 then
             raise Program_Error with
               "attempt to tamper with elements (container is locked)";
@@ -231,8 +309,6 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
          --  stays in the same bucket.
 
          Assign (NN (Node), Key);
-         pragma Assert (Hash (NN (Node)) = New_Hash);
-         pragma Assert (Equivalent_Keys (Key, NN (Node)));
          return;
       end if;
 
@@ -243,7 +319,7 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
 
       N := New_Bucket;
       while N /= 0 loop
-         if Equivalent_Keys (Key, NN (N)) then
+         if Checked_Equivalent_Keys (HT, Key, N) then
             pragma Assert (N /= Node);
             raise Program_Error with
               "attempt to replace existing element";
@@ -269,8 +345,6 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
          end if;
 
          Assign (NN (Node), Key);
-         pragma Assert (Hash (NN (Node)) = New_Hash);
-         pragma Assert (Equivalent_Keys (Key, NN (Node)));
          return;
       end if;
 
@@ -286,8 +360,6 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
       --  modified (except for any possible side-effect Assign had on Node).
 
       Assign (NN (Node), Key);
-      pragma Assert (Hash (NN (Node)) = New_Hash);
-      pragma Assert (Equivalent_Keys (Key, NN (Node)));
 
       --  Now we can safely remove the node from its current bucket
 
@@ -319,4 +391,15 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
       New_Bucket := Node;
    end Generic_Replace_Element;
 
+   -----------
+   -- Index --
+   -----------
+
+   function Index
+     (HT  : Hash_Table_Type'Class;
+      Key : Key_Type) return Hash_Type is
+   begin
+      return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
+   end Index;
+
 end Ada.Containers.Hash_Tables.Generic_Bounded_Keys;

gcc/ada/a-chtgbk.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2010, 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- --
@@ -59,6 +59,20 @@ package Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
    pragma Inline (Index);
    --  Returns the bucket number (array index value) for the given key
 
+   function Checked_Index
+     (HT  : aliased in out Hash_Table_Type'Class;
+      Key : Key_Type) return Hash_Type;
+   pragma Inline (Checked_Index);
+   --  Calls Index, but also locks and unlocks the container, per AI05-0022, in
+   --  order to detect element tampering by the generic actual Hash function.
+
+   function Checked_Equivalent_Keys
+     (HT   : aliased in out Hash_Table_Type'Class;
+      Key  : Key_Type;
+      Node : Count_Type) return Boolean;
+   --  Calls Equivalent_Keys, but locks and unlocks the container, per
+   --  AI05-0022, in order to detect element tampering by that generic actual.
+
    procedure Delete_Key_Sans_Free
      (HT  : in out Hash_Table_Type'Class;
       Key : Key_Type;

gcc/ada/a-chtgbo.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2011, 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- --
@@ -31,6 +31,37 @@ with System;  use type System.Address;
 
 package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
 
+   -------------------
+   -- Checked_Index --
+   -------------------
+
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type'Class;
+      Node       : Count_Type) return Hash_Type
+   is
+      Result : Hash_Type;
+
+      B : Natural renames Hash_Table.Busy;
+      L : Natural renames Hash_Table.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := Index (Hash_Table, Hash_Table.Nodes (Node));
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Index;
+
    -----------
    -- Clear --
    -----------
@@ -69,7 +100,7 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
            "attempt to delete node from empty hashed container";
       end if;
 
-      Indx := Index (HT, HT.Nodes (X));
+      Indx := Checked_Index (HT, X);
       Prev := HT.Buckets (Indx);
 
       if Prev = 0 then
@@ -288,6 +319,14 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
    function Generic_Equal
      (L, R : Hash_Table_Type'Class) return Boolean
    is
+      BL : Natural renames L'Unrestricted_Access.Busy;
+      LL : Natural renames L'Unrestricted_Access.Lock;
+
+      BR : Natural renames R'Unrestricted_Access.Busy;
+      LR : Natural renames R'Unrestricted_Access.Lock;
+
+      Result : Boolean;
+
       L_Index : Hash_Type;
       L_Node  : Count_Type;
 
@@ -315,13 +354,23 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
          L_Index := L_Index + 1;
       end loop;
 
+      --  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;
+
       --  For each node of hash table L, search for an equivalent node in hash
       --  table R.
 
       N := L.Length;
       loop
          if not Find (HT => R, Key => L.Nodes (L_Node)) then
-            return False;
+            Result := False;
+            exit;
          end if;
 
          N := N - 1;
@@ -332,7 +381,8 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
             --  We have exhausted the nodes in this bucket
 
             if N = 0 then
-               return True;
+               Result := True;
+               exit;
             end if;
 
             --  Find the next bucket
@@ -344,6 +394,23 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
             end loop;
          end if;
       end loop;
+
+      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 Generic_Equal;
 
    -----------------------
@@ -397,7 +464,7 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
       for J in 1 .. N loop
          declare
             Node : constant Count_Type := New_Node (Stream);
-            Indx : constant Hash_Type := Index (HT, HT.Nodes (Node));
+            Indx : constant Hash_Type := Checked_Index (HT, Node);
             B    : Count_Type renames HT.Buckets (Indx);
          begin
             Set_Next (HT.Nodes (Node), Next => B);
@@ -461,9 +528,12 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
      (HT   : Hash_Table_Type'Class;
       Node : Count_Type) return Count_Type
    is
-      Result : Count_Type := Next (HT.Nodes (Node));
+      Result : Count_Type;
+      First  : Hash_Type;
 
    begin
+      Result := Next (HT.Nodes (Node));
+
       if Result /= 0 then  -- another node in same bucket
          return Result;
       end if;
@@ -471,7 +541,8 @@ package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
       --  This was the last node in the bucket, so move to the next
       --  bucket, and start searching for next node from there.
 
-      for Indx in Index (HT, HT.Nodes (Node)) + 1 .. HT.Buckets'Last loop
+      First := Checked_Index (HT'Unrestricted_Access.all, Node) + 1;
+      for Indx in First .. HT.Buckets'Last loop
          Result := HT.Buckets (Indx);
 
          if Result /= 0 then  -- bucket is not empty

gcc/ada/a-chtgbo.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2010, 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- --
@@ -62,6 +62,12 @@ package Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
    --  Uses the hash value of Node to compute its Hash_Table buckets array
    --  index.
 
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type'Class;
+      Node       : Count_Type) return Hash_Type;
+   --  Calls Index, but also locks and unlocks the container, per AI05-0022, in
+   --  order to detect element tampering by the generic actual Hash function.
+
    generic
       with function Find
         (HT  : Hash_Table_Type'Class;

gcc/ada/a-chtgke.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2010, 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- --
@@ -29,6 +29,69 @@
 
 package body Ada.Containers.Hash_Tables.Generic_Keys is
 
+   -----------------------------
+   -- Checked_Equivalent_Keys --
+   -----------------------------
+
+   function Checked_Equivalent_Keys
+     (HT   : aliased in out Hash_Table_Type;
+      Key  : Key_Type;
+      Node : Node_Access) return Boolean
+   is
+      Result : Boolean;
+
+      B : Natural renames HT.Busy;
+      L : Natural renames HT.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := Equivalent_Keys (Key, Node);
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Equivalent_Keys;
+
+   -------------------
+   -- Checked_Index --
+   -------------------
+
+   function Checked_Index
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Key_Type) return Hash_Type
+   is
+      Result : Hash_Type;
+
+      B : Natural renames HT.Busy;
+      L : Natural renames HT.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := Hash (Key) mod HT.Buckets'Length;
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Index;
+
    --------------------------
    -- Delete_Key_Sans_Free --
    --------------------------
@@ -47,14 +110,22 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          return;
       end if;
 
-      Indx := Index (HT, Key);
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      if HT.Busy > 0 then
+         raise Program_Error with
+           "attempt to tamper with cursors (container is busy)";
+      end if;
+
+      Indx := Checked_Index (HT, Key);
       X := HT.Buckets (Indx);
 
       if X = null then
          return;
       end if;
 
-      if Equivalent_Keys (Key, X) then
+      if Checked_Equivalent_Keys (HT, Key, X) then
          if HT.Busy > 0 then
             raise Program_Error with
               "attempt to tamper with cursors (container is busy)";
@@ -72,7 +143,7 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
             return;
          end if;
 
-         if Equivalent_Keys (Key, X) then
+         if Checked_Equivalent_Keys (HT, Key, X) then
             if HT.Busy > 0 then
                raise Program_Error with
                  "attempt to tamper with cursors (container is busy)";
@@ -89,9 +160,9 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
    ----------
 
    function Find
-     (HT  : Hash_Table_Type;
-      Key : Key_Type) return Node_Access is
-
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Key_Type) return Node_Access
+   is
       Indx : Hash_Type;
       Node : Node_Access;
 
@@ -100,11 +171,11 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          return null;
       end if;
 
-      Indx := Index (HT, Key);
+      Indx := Checked_Index (HT, Key);
 
       Node := HT.Buckets (Indx);
       while Node /= null loop
-         if Equivalent_Keys (Key, Node) then
+         if Checked_Equivalent_Keys (HT, Key, Node) then
             return Node;
          end if;
          Node := Next (Node);
@@ -123,16 +194,21 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
       Node     : out Node_Access;
       Inserted : out Boolean)
    is
-      Indx : constant Hash_Type := Index (HT, Key);
-      B    : Node_Access renames HT.Buckets (Indx);
+      Indx : Hash_Type;
 
    begin
-      if B = null then
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
       if HT.Busy > 0 then
          raise Program_Error with
            "attempt to tamper with cursors (container is busy)";
       end if;
 
+      Indx := Checked_Index (HT, Key);
+      Node := HT.Buckets (Indx);
+
+      if Node = null then
          if HT.Length = Count_Type'Last then
             raise Constraint_Error;
          end if;
@@ -140,15 +216,14 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          Node := New_Node (Next => null);
          Inserted := True;
 
-         B := Node;
+         HT.Buckets (Indx) := Node;
          HT.Length := HT.Length + 1;
 
          return;
       end if;
 
-      Node := B;
       loop
-         if Equivalent_Keys (Key, Node) then
+         if Checked_Equivalent_Keys (HT, Key, Node) then
             Inserted := False;
             return;
          end if;
@@ -158,33 +233,17 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          exit when Node = null;
       end loop;
 
-      if HT.Busy > 0 then
-         raise Program_Error with
-           "attempt to tamper with cursors (container is busy)";
-      end if;
-
       if HT.Length = Count_Type'Last then
          raise Constraint_Error;
       end if;
 
-      Node := New_Node (Next => B);
+      Node := New_Node (Next => HT.Buckets (Indx));
       Inserted := True;
 
-      B := Node;
+      HT.Buckets (Indx) := Node;
       HT.Length := HT.Length + 1;
    end Generic_Conditional_Insert;
 
-   -----------
-   -- Index --
-   -----------
-
-   function Index
-     (HT  : Hash_Table_Type;
-      Key : Key_Type) return Hash_Type is
-   begin
-      return Hash (Key) mod HT.Buckets'Length;
-   end Index;
-
    -----------------------------
    -- Generic_Replace_Element --
    -----------------------------
@@ -197,19 +256,36 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
       pragma Assert (HT.Length > 0);
       pragma Assert (Node /= null);
 
-      Old_Hash : constant Hash_Type := Hash (Node);
-      Old_Indx : constant Hash_Type := Old_Hash mod HT.Buckets'Length;
-
-      New_Hash : constant Hash_Type := Hash (Key);
-      New_Indx : constant Hash_Type := New_Hash mod HT.Buckets'Length;
+      Old_Indx : Hash_Type;
+      New_Indx : constant Hash_Type := Checked_Index (HT, Key);
 
       New_Bucket : Node_Access renames HT.Buckets (New_Indx);
       N, M       : Node_Access;
 
    begin
-      if Equivalent_Keys (Key, Node) then
-         pragma Assert (New_Hash = Old_Hash);
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      declare
+         B : Natural renames HT.Busy;
+         L : Natural renames HT.Lock;
+      begin
+         B := B + 1;
+         L := L + 1;
+
+         Old_Indx := Hash (Node) mod HT.Buckets'Length;
+
+         B := B - 1;
+         L := L - 1;
+      exception
+         when others =>
+            B := B - 1;
+            L := L - 1;
 
+            raise;
+      end;
+
+      if Checked_Equivalent_Keys (HT, Key, Node) then
          if HT.Lock > 0 then
             raise Program_Error with
               "attempt to tamper with elements (container is locked)";
@@ -222,8 +298,6 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          --  change is allowed.
 
          Assign (Node, Key);
-         pragma Assert (Hash (Node) = New_Hash);
-         pragma Assert (Equivalent_Keys (Key, Node));
          return;
       end if;
 
@@ -234,7 +308,7 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
 
       N := New_Bucket;
       while N /= null loop
-         if Equivalent_Keys (Key, N) then
+         if Checked_Equivalent_Keys (HT, Key, N) then
             pragma Assert (N /= Node);
             raise Program_Error with
               "attempt to replace existing element";
@@ -260,8 +334,6 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
          end if;
 
          Assign (Node, Key);
-         pragma Assert (Hash (Node) = New_Hash);
-         pragma Assert (Equivalent_Keys (Key, Node));
          return;
       end if;
 
@@ -277,8 +349,6 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
       --  modified (except for any possible side-effect Assign had on Node).
 
       Assign (Node, Key);
-      pragma Assert (Hash (Node) = New_Hash);
-      pragma Assert (Equivalent_Keys (Key, Node));
 
       --  Now we can safely remove the node from its current bucket
 
@@ -310,4 +380,16 @@ package body Ada.Containers.Hash_Tables.Generic_Keys is
       New_Bucket := Node;
    end Generic_Replace_Element;
 
+   -----------
+   -- Index --
+   -----------
+
+   function Index
+     (HT  : Hash_Table_Type;
+      Key : Key_Type) return Hash_Type
+   is
+   begin
+      return Hash (Key) mod HT.Buckets'Length;
+   end Index;
+
 end Ada.Containers.Hash_Tables.Generic_Keys;

gcc/ada/a-chtgke.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2009, 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- --
@@ -59,6 +59,20 @@ package Ada.Containers.Hash_Tables.Generic_Keys is
    pragma Inline (Index);
    --  Returns the bucket number (array index value) for the given key
 
+   function Checked_Index
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Key_Type) return Hash_Type;
+   pragma Inline (Checked_Index);
+   --  Calls Index, but also locks and unlocks the container, per AI05-0022, in
+   --  order to detect element tampering by the generic actual Hash function.
+
+   function Checked_Equivalent_Keys
+     (HT   : aliased in out Hash_Table_Type;
+      Key  : Key_Type;
+      Node : Node_Access) return Boolean;
+   --  Calls Equivalent_Keys, but locks and unlocks the container, per
+   --  AI05-0022, in order to detect element tampering by that generic actual.
+
    procedure Delete_Key_Sans_Free
      (HT  : in out Hash_Table_Type;
       Key : Key_Type;
@@ -67,7 +81,9 @@ package Ada.Containers.Hash_Tables.Generic_Keys is
    --  without deallocating it. Program_Error is raised if the hash
    --  table is busy.
 
-   function Find (HT : Hash_Table_Type; Key : Key_Type) return Node_Access;
+   function Find
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Key_Type) return Node_Access;
    --  Returns the node (if any) corresponding to the given key
 
    generic

gcc/ada/a-chtgop.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2010, 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- --
@@ -75,7 +75,7 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
 
                --  See note above
 
-               pragma Assert (Index (HT, Dst_Node) = Src_Index);
+               pragma Assert (Checked_Index (HT, Dst_Node) = Src_Index);
 
             begin
                HT.Buckets (Src_Index) := Dst_Node;
@@ -91,7 +91,7 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
 
                   --  See note above
 
-                  pragma Assert (Index (HT, Dst_Node) = Src_Index);
+                  pragma Assert (Checked_Index (HT, Dst_Node) = Src_Index);
 
                begin
                   Set_Next (Node => Dst_Prev, Next => Dst_Node);
@@ -121,6 +121,46 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
       return HT.Buckets'Length;
    end Capacity;
 
+   -------------------
+   -- Checked_Index --
+   -------------------
+
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type;
+      Buckets    : Buckets_Type;
+      Node       : Node_Access) return Hash_Type
+   is
+      Result : Hash_Type;
+
+      B : Natural renames Hash_Table.Busy;
+      L : Natural renames Hash_Table.Lock;
+
+   begin
+      B := B + 1;
+      L := L + 1;
+
+      Result := Index (Buckets, Node);
+
+      B := B - 1;
+      L := L - 1;
+
+      return Result;
+   exception
+      when others =>
+         B := B - 1;
+         L := L - 1;
+
+         raise;
+   end Checked_Index;
+
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type;
+      Node       : Node_Access) return Hash_Type
+   is
+   begin
+      return Checked_Index (Hash_Table, Hash_Table.Buckets.all, Node);
+   end Checked_Index;
+
    -----------
    -- Clear --
    -----------
@@ -174,7 +214,7 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
            "attempt to delete node from empty hashed container";
       end if;
 
-      Indx := Index (HT, X);
+      Indx := Checked_Index (HT, X);
       Prev := HT.Buckets (Indx);
 
       if Prev = null then
@@ -288,6 +328,14 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
    function Generic_Equal
      (L, R : Hash_Table_Type) return Boolean
    is
+      BL : Natural renames L'Unrestricted_Access.Busy;
+      LL : Natural renames L'Unrestricted_Access.Lock;
+
+      BR : Natural renames R'Unrestricted_Access.Busy;
+      LR : Natural renames R'Unrestricted_Access.Lock;
+
+      Result : Boolean;
+
       L_Index : Hash_Type;
       L_Node  : Node_Access;
 
@@ -315,13 +363,23 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
          L_Index := L_Index + 1;
       end loop;
 
+      --  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;
+
       --  For each node of hash table L, search for an equivalent node in hash
       --  table R.
 
       N := L.Length;
       loop
          if not Find (HT => R, Key => L_Node) then
-            return False;
+            Result := False;
+            exit;
          end if;
 
          N := N - 1;
@@ -332,7 +390,8 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
             --  We have exhausted the nodes in this bucket
 
             if N = 0 then
-               return True;
+               Result := True;
+               exit;
             end if;
 
             --  Find the next bucket
@@ -344,6 +403,23 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
             end loop;
          end if;
       end loop;
+
+      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 Generic_Equal;
 
    -----------------------
@@ -407,7 +483,7 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
       for J in 1 .. N loop
          declare
             Node : constant Node_Access := New_Node (Stream);
-            Indx : constant Hash_Type := Index (HT, Node);
+            Indx : constant Hash_Type := Checked_Index (HT, Node);
             B    : Node_Access renames HT.Buckets (Indx);
          begin
             Set_Next (Node => Node, Next => B);
@@ -513,17 +589,21 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
    ----------
 
    function Next
-     (HT   : Hash_Table_Type;
+     (HT   : aliased in out Hash_Table_Type;
       Node : Node_Access) return Node_Access
    is
-      Result : Node_Access := Next (Node);
+      Result : Node_Access;
+      First  : Hash_Type;
 
    begin
+      Result := Next (Node);
+
       if Result /= null then
          return Result;
       end if;
 
-      for Indx in Index (HT, Node) + 1 .. HT.Buckets'Last loop
+      First := Checked_Index (HT, Node) + 1;
+      for Indx in First .. HT.Buckets'Last loop
          Result := HT.Buckets (Indx);
 
          if Result /= null then
@@ -643,7 +723,7 @@ package body Ada.Containers.Hash_Tables.Generic_Operations is
                      Src_Node : constant Node_Access := Src_Bucket;
 
                      Dst_Index : constant Hash_Type :=
-                       Index (Dst_Buckets.all, Src_Node);
+                       Checked_Index (HT, Dst_Buckets.all, Src_Node);
 
                      Dst_Bucket : Node_Access renames Dst_Buckets (Dst_Index);
 

gcc/ada/a-chtgop.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2009, 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- --
@@ -71,6 +71,18 @@ package Ada.Containers.Hash_Tables.Generic_Operations is
    --  Uses the hash value of Node to compute its Hash_Table buckets array
    --  index.
 
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type;
+      Buckets    : Buckets_Type;
+      Node       : Node_Access) return Hash_Type;
+   --  Calls Index, but also locks and unlocks the container, per AI05-0022, in
+   --  order to detect element tampering by the generic actual Hash function.
+
+   function Checked_Index
+     (Hash_Table : aliased in out Hash_Table_Type;
+      Node       : Node_Access) return Hash_Type;
+   --  Calls Checked_Index using Hash_Table's buckets array.
+
    procedure Adjust (HT : in out Hash_Table_Type);
    --  Used to implement controlled Adjust. It is assumed that HT has the value
    --  of the bit-wise copy that immediately follows controlled Finalize.
@@ -126,7 +138,7 @@ package Ada.Containers.Hash_Tables.Generic_Operations is
    --  bucket.
 
    function Next
-     (HT   : Hash_Table_Type;
+     (HT   : aliased in out Hash_Table_Type;
       Node : Node_Access) return Node_Access;
    --  Returns the node that immediately follows Node. This corresponds to
    --  either the next node in the same bucket, or (if Node is the last node in

gcc/ada/a-cihama.adb

@@ -238,7 +238,8 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
      (Container : aliased Map;
       Key       : Key_Type) return Constant_Reference_Type
    is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -250,8 +251,6 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
       end if;
 
       declare
-         M : Map renames Container'Unrestricted_Access.all;
-         HT : Hash_Table_Type renames M.HT'Unrestricted_Access.all;
          B : Natural renames HT.Busy;
          L : Natural renames HT.Lock;
       begin
@@ -368,7 +367,8 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
    -------------
 
    function Element (Container : Map; Key : Key_Type) return Element_Type is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -533,7 +533,8 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
    ----------
 
    function Find (Container : Map; Key : Key_Type) return Cursor is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -1106,7 +1107,8 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
      (Container : aliased in out Map;
       Key       : Key_Type) return Reference_Type
    is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -1118,8 +1120,6 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
       end if;
 
       declare
-         M : Map renames Container'Unrestricted_Access.all;
-         HT : Hash_Table_Type renames M.HT'Unrestricted_Access.all;
          B : Natural renames HT.Busy;
          L : Natural renames HT.Lock;
       begin
@@ -1353,7 +1353,7 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
             return False;
          end if;
 
-         X := HT.Buckets (Key_Ops.Index (HT, Position.Node.Key.all));
+         X := HT.Buckets (Key_Ops.Checked_Index (HT, Position.Node.Key.all));
 
          for J in 1 .. HT.Length loop
             if X = Position.Node then

gcc/ada/a-cihase.adb

@@ -75,7 +75,9 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
       Node     : out Node_Access;
       Inserted : out Boolean);
 
-   function Is_In (HT  : Hash_Table_Type; Key : Node_Access) return Boolean;
+   function Is_In
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Node_Access) return Boolean;
    pragma Inline (Is_In);
 
    function Next (Node : Node_Access) return Node_Access;
@@ -359,6 +361,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
      (Target : in out Set;
       Source : Set)
    is
+      Src_HT   : Hash_Table_Type renames Source'Unrestricted_Access.HT;
       Tgt_Node : Node_Access;
 
    begin
@@ -367,7 +370,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          return;
       end if;
 
-      if Source.HT.Length = 0 then
+      if Src_HT.Length = 0 then
          return;
       end if;
 
@@ -376,12 +379,12 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
            "attempt to tamper with cursors (set is busy)";
       end if;
 
-      if Source.HT.Length < Target.HT.Length then
+      if Src_HT.Length < Target.HT.Length then
          declare
             Src_Node : Node_Access;
 
          begin
-            Src_Node := HT_Ops.First (Source.HT);
+            Src_Node := HT_Ops.First (Src_HT);
             while Src_Node /= null loop
                Tgt_Node := Element_Keys.Find (Target.HT, Src_Node.Element.all);
 
@@ -390,14 +393,14 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
                   Free (Tgt_Node);
                end if;
 
-               Src_Node := HT_Ops.Next (Source.HT, Src_Node);
+               Src_Node := HT_Ops.Next (Src_HT, Src_Node);
             end loop;
          end;
 
       else
          Tgt_Node := HT_Ops.First (Target.HT);
          while Tgt_Node /= null loop
-            if Is_In (Source.HT, Tgt_Node) then
+            if Is_In (Src_HT, Tgt_Node) then
                declare
                   X : Node_Access := Tgt_Node;
                begin
@@ -414,6 +417,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
    end Difference;
 
    function Difference (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -450,12 +455,20 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if not Is_In (Right.HT, L_Node) then
+            if not Is_In (Right_HT, L_Node) then
                declare
-                  Src    : Element_Type renames L_Node.Element.all;
-                  Indx   : constant Hash_Type := Hash (Src) mod Buckets'Length;
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
+                  Indx   : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
+
                   Bucket : Node_Access renames Buckets (Indx);
+                  Src    : Element_Type renames L_Node.Element.all;
                   Tgt    : Element_Access := new Element_Type'(Src);
+
                begin
                   Bucket := new Node_Type'(Tgt, Bucket);
                exception
@@ -538,6 +551,20 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
       pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
       pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
 
+      --  AI05-0022 requires that a container implementation detect element
+      --  tampering by a generic actual subprogram. However, the following case
+      --  falls outside the scope of that AI. Randy Brukardt explained on the
+      --  ARG list on 2013/02/07 that:
+
+      --  (Begin Quote):
+      --  But for an operation like "<" [the ordered set analog of
+      --  Equivalent_Elements], there is no need to "dereference" a cursor
+      --  after the call to the generic formal parameter function, so nothing
+      --  bad could happen if tampering is undetected. And the operation can
+      --  safely return a result without a problem even if an element is
+      --  deleted from the container.
+      --  (End Quote).
+
       return Equivalent_Elements
                (Left.Node.Element.all,
                 Right.Node.Element.all);
@@ -653,7 +680,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
      (Container : Set;
       Item      : Element_Type) return Cursor
    is
-      Node : constant Node_Access := Element_Keys.Find (Container.HT, Item);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Element_Keys.Find (HT, Item);
    begin
       return (if Node = null then No_Element
               else Cursor'(Container'Unrestricted_Access, Node));
@@ -904,6 +932,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
      (Target : in out Set;
       Source : Set)
    is
+      Src_HT   : Hash_Table_Type renames Source'Unrestricted_Access.HT;
       Tgt_Node : Node_Access;
 
    begin
@@ -923,7 +952,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
       Tgt_Node := HT_Ops.First (Target.HT);
       while Tgt_Node /= null loop
-         if Is_In (Source.HT, Tgt_Node) then
+         if Is_In (Src_HT, Tgt_Node) then
             Tgt_Node := HT_Ops.Next (Target.HT, Tgt_Node);
 
          else
@@ -939,6 +968,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
    end Intersection;
 
    function Intersection (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -973,14 +1004,19 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if Is_In (Right.HT, L_Node) then
+            if Is_In (Right_HT, L_Node) then
                declare
-                  Src : Element_Type renames L_Node.Element.all;
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
 
-                  Indx : constant Hash_Type := Hash (Src) mod Buckets'Length;
+                  Indx : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
 
                   Bucket : Node_Access renames Buckets (Indx);
 
+                  Src : Element_Type renames L_Node.Element.all;
                   Tgt : Element_Access := new Element_Type'(Src);
 
                begin
@@ -1021,7 +1057,10 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
    -- Is_In --
    -----------
 
-   function Is_In (HT  : Hash_Table_Type; Key : Node_Access) return Boolean is
+   function Is_In
+     (HT  : aliased in out Hash_Table_Type;
+      Key : Node_Access) return Boolean
+   is
    begin
       return Element_Keys.Find (HT, Key.Element.all) /= null;
    end Is_In;
@@ -1034,6 +1073,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
      (Subset : Set;
       Of_Set : Set) return Boolean
    is
+      Subset_HT   : Hash_Table_Type renames Subset'Unrestricted_Access.HT;
+      Of_Set_HT   : Hash_Table_Type renames Of_Set'Unrestricted_Access.HT;
       Subset_Node : Node_Access;
 
    begin
@@ -1045,13 +1086,13 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          return False;
       end if;
 
-      Subset_Node := HT_Ops.First (Subset.HT);
+      Subset_Node := HT_Ops.First (Subset_HT);
       while Subset_Node /= null loop
-         if not Is_In (Of_Set.HT, Subset_Node) then
+         if not Is_In (Of_Set_HT, Subset_Node) then
             return False;
          end if;
 
-         Subset_Node := HT_Ops.Next (Subset.HT, Subset_Node);
+         Subset_Node := HT_Ops.Next (Subset_HT, Subset_Node);
       end loop;
 
       return True;
@@ -1186,6 +1227,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
    -------------
 
    function Overlap (Left, Right : Set) return Boolean is
+      Left_HT   : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT  : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Left_Node : Node_Access;
 
    begin
@@ -1197,13 +1240,13 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          return True;
       end if;
 
-      Left_Node := HT_Ops.First (Left.HT);
+      Left_Node := HT_Ops.First (Left_HT);
       while Left_Node /= null loop
-         if Is_In (Right.HT, Left_Node) then
+         if Is_In (Right_HT, Left_Node) then
             return True;
          end if;
 
-         Left_Node := HT_Ops.Next (Left.HT, Left_Node);
+         Left_Node := HT_Ops.Next (Left_HT, Left_Node);
       end loop;
 
       return False;
@@ -1396,13 +1439,25 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
      (Target : in out Set;
       Source : Set)
    is
+      Tgt_HT : Hash_Table_Type renames Target.HT;
+      Src_HT : Hash_Table_Type renames Source.HT'Unrestricted_Access.all;
+
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      TB : Natural renames Tgt_HT.Busy;
+      TL : Natural renames Tgt_HT.Lock;
+
+      SB : Natural renames Src_HT.Busy;
+      SL : Natural renames Src_HT.Lock;
+
    begin
       if Target'Address = Source'Address then
          Clear (Target);
          return;
       end if;
 
-      if Target.HT.Busy > 0 then
+      if TB > 0 then
          raise Program_Error with
            "attempt to tamper with cursors (set is busy)";
       end if;
@@ -1410,8 +1465,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
       declare
          N : constant Count_Type := Target.Length + Source.Length;
       begin
-         if N > HT_Ops.Capacity (Target.HT) then
-            HT_Ops.Reserve_Capacity (Target.HT, N);
+         if N > HT_Ops.Capacity (Tgt_HT) then
+            HT_Ops.Reserve_Capacity (Tgt_HT, N);
          end if;
       end;
 
@@ -1427,9 +1482,9 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
             procedure Process (Src_Node : Node_Access) is
                E : Element_Type renames Src_Node.Element.all;
-               B : Buckets_Type renames Target.HT.Buckets.all;
+               B : Buckets_Type renames Tgt_HT.Buckets.all;
                J : constant Hash_Type := Hash (E) mod B'Length;
-               N : Count_Type renames Target.HT.Length;
+               N : Count_Type renames Tgt_HT.Length;
 
             begin
                declare
@@ -1448,7 +1503,29 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          --  Start of processing for Iterate_Source_When_Empty_Target
 
          begin
-            Iterate (Source.HT);
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            Iterate (Src_HT);
+
+            SL := SL - 1;
+            SB := SB - 1;
+
+            TL := TL - 1;
+            TB := TB - 1;
+
+         exception
+            when others =>
+               SL := SL - 1;
+               SB := SB - 1;
+
+               TL := TL - 1;
+               TB := TB - 1;
+
+               raise;
          end Iterate_Source_When_Empty_Target;
 
       else
@@ -1464,9 +1541,9 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
             procedure Process (Src_Node : Node_Access) is
                E : Element_Type renames Src_Node.Element.all;
-               B : Buckets_Type renames Target.HT.Buckets.all;
+               B : Buckets_Type renames Tgt_HT.Buckets.all;
                J : constant Hash_Type := Hash (E) mod B'Length;
-               N : Count_Type renames Target.HT.Length;
+               N : Count_Type renames Tgt_HT.Length;
 
             begin
                if B (J) = null then
@@ -1527,12 +1604,36 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          --  Start of processing for Iterate_Source
 
          begin
-            Iterate (Source.HT);
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            Iterate (Src_HT);
+
+            SL := SL - 1;
+            SB := SB - 1;
+
+            TL := TL - 1;
+            TB := TB - 1;
+
+         exception
+            when others =>
+               SL := SL - 1;
+               SB := SB - 1;
+
+               TL := TL - 1;
+               TB := TB - 1;
+
+               raise;
          end Iterate_Source;
       end if;
    end Symmetric_Difference;
 
    function Symmetric_Difference (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -1570,10 +1671,17 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if not Is_In (Right.HT, L_Node) then
+            if not Is_In (Right_HT, L_Node) then
                declare
                   E : Element_Type renames L_Node.Element.all;
-                  J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
+                  J : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
 
                begin
                   declare
@@ -1594,7 +1702,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
       --  Start of processing for Iterate_Left
 
       begin
-         Iterate (Left.HT);
+         Iterate (Left_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -1613,10 +1721,17 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
 
          procedure Process (R_Node : Node_Access) is
          begin
-            if not Is_In (Left.HT, R_Node) then
+            if not Is_In (Left_HT, R_Node) then
                declare
                   E : Element_Type renames R_Node.Element.all;
-                  J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
+                  J : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Right_HT, Buckets.all, R_Node);
 
                begin
                   declare
@@ -1637,7 +1752,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
       --  Start of processing for Iterate_Right
 
       begin
-         Iterate (Right.HT);
+         Iterate (Right_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -1735,6 +1850,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
    end Union;
 
    function Union (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left.HT'Unrestricted_Access.all;
+      Right_HT : Hash_Table_Type renames Right.HT'Unrestricted_Access.all;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -1781,12 +1898,29 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
                raise;
          end Process;
 
-      --  Start of processing for Process
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram, hence the use of
+         --  Checked_Index instead of a simple invocation of generic formal
+         --  Hash.
+
+         B : Integer renames Left_HT.Busy;
+         L : Integer renames Left_HT.Lock;
+
+      --  Start of processing for Iterate_Left
 
       begin
+         B := B + 1;
+         L := L + 1;
+
          Iterate (Left.HT);
+
+         L := L - 1;
+         B := B - 1;
       exception
          when others =>
+            L := L - 1;
+            B := B - 1;
+
             HT_Ops.Free_Hash_Table (Buckets);
             raise;
       end Iterate_Left;
@@ -1830,12 +1964,41 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
             Length := Length + 1;
          end Process;
 
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram, hence the use of
+         --  Checked_Index instead of a simple invocation of generic formal
+         --  Hash.
+
+         LB : Integer renames Left_HT.Busy;
+         LL : Integer renames Left_HT.Lock;
+
+         RB : Integer renames Right_HT.Busy;
+         RL : Integer renames Right_HT.Lock;
+
       --  Start of processing for Iterate_Right
 
       begin
+         LB := LB + 1;
+         LL := LL + 1;
+
+         RB := RB + 1;
+         RL := RL + 1;
+
          Iterate (Right.HT);
+
+         RL := RL - 1;
+         RB := RB - 1;
+
+         LL := LL - 1;
+         LB := LB - 1;
       exception
          when others =>
+            RL := RL - 1;
+            RB := RB - 1;
+
+            LL := LL - 1;
+            LB := LB - 1;
+
             HT_Ops.Free_Hash_Table (Buckets);
             raise;
       end Iterate_Right;
@@ -1880,7 +2043,9 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
             return False;
          end if;
 
-         X := HT.Buckets (Element_Keys.Index (HT, Position.Node.Element.all));
+         X := HT.Buckets (Element_Keys.Checked_Index
+                            (HT,
+                             Position.Node.Element.all));
 
          for J in 1 .. HT.Length loop
             if X = Position.Node then
@@ -1974,8 +2139,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
         (Container : aliased Set;
          Key       : Key_Type) return Constant_Reference_Type
       is
-         Node : constant Node_Access :=
-           Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
 
       begin
          if Node = null then
@@ -1987,7 +2152,6 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          end if;
 
          declare
-            HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
             B : Natural renames HT.Busy;
             L : Natural renames HT.Lock;
          begin
@@ -2027,7 +2191,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
          Key_Keys.Delete_Key_Sans_Free (Container.HT, Key, X);
 
          if X = null then
-            raise Constraint_Error with "key not in map";  --  ??? "set"
+            raise Constraint_Error with "key not in set";
          end if;
 
          Free (X);
@@ -2041,11 +2205,12 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Element_Type
       is
-         Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
 
       begin
          if Node = null then
-            raise Constraint_Error with "key not in map";  --  ??? "set"
+            raise Constraint_Error with "key not in set";
          end if;
 
          return Node.Element.all;
@@ -2084,7 +2249,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Cursor
       is
-         Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
       begin
          return (if Node = null then No_Element
                  else Cursor'(Container'Unrestricted_Access, Node));
@@ -2240,7 +2406,8 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
            (Vet (Position),
             "bad cursor in Update_Element_Preserving_Key");
 
-         Indx := HT_Ops.Index (HT, Position.Node);
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
 
          declare
             E : Element_Type renames Position.Node.Element.all;
@@ -2249,12 +2416,16 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
             B : Natural renames HT.Busy;
             L : Natural renames HT.Lock;
 
+            Eq : Boolean;
+
          begin
             B := B + 1;
             L := L + 1;
 
             begin
+               Indx := HT_Ops.Index (HT, Position.Node);
                Process (E);
+               Eq := Equivalent_Keys (K, Key (E));
             exception
                when others =>
                   L := L - 1;
@@ -2265,8 +2436,7 @@ package body Ada.Containers.Indefinite_Hashed_Sets is
             L := L - 1;
             B := B - 1;
 
-            if Equivalent_Keys (K, Key (E)) then
-               pragma Assert (Hash (K) = Hash (E));
+            if Eq then
                return;
             end if;
          end;

gcc/ada/a-cofove.ads

@@ -88,59 +88,82 @@ package Ada.Containers.Formal_Vectors is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Vector) return Boolean;
+   function "=" (Left, Right : Vector) return Boolean with
+     Global => null;
 
    function To_Vector
      (New_Item : Element_Type;
-      Length   : Count_Type) return Vector;
+      Length   : Count_Type) return Vector
+   with
+     Global => null;
 
-   function "&" (Left, Right : Vector) return Vector;
+   function "&" (Left, Right : Vector) return Vector with
+     Global => null,
+     Pre    => Capacity_Range'Last - Length (Left) >= Length (Right);
 
-   function "&" (Left : Vector; Right : Element_Type) return Vector;
+   function "&" (Left : Vector; Right : Element_Type) return Vector with
+     Global => null,
+     Pre    => Length (Left) < Capacity_Range'Last;
 
-   function "&" (Left : Element_Type; Right : Vector) return Vector;
+   function "&" (Left : Element_Type; Right : Vector) return Vector with
+     Global => null,
+     Pre    => Length (Right) < Capacity_Range'Last;
 
-   function "&" (Left, Right : Element_Type) return Vector;
+   function "&" (Left, Right : Element_Type) return Vector with
+     Global => null,
+     Pre    => Capacity_Range'Last >= 2;
 
-   function Capacity (Container : Vector) return Count_Type;
+   function Capacity (Container : Vector) return Count_Type with
+     Global => null;
 
    procedure Reserve_Capacity
      (Container : in out Vector;
       Capacity  : Count_Type)
    with
+     Global => null,
      Pre    => Capacity <= Container.Capacity;
 
-   function Length (Container : Vector) return Count_Type;
+   function Length (Container : Vector) return Count_Type with
+     Global => null;
 
    procedure Set_Length
      (Container : in out Vector;
       New_Length    : Count_Type)
    with
+     Global => null,
      Pre    => New_Length <= Length (Container);
 
-   function Is_Empty (Container : Vector) return Boolean;
+   function Is_Empty (Container : Vector) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Vector);
+   procedure Clear (Container : in out Vector) with
+     Global => null;
 
    procedure Assign (Target : in out Vector; Source : Vector) with
+     Global => null,
      Pre    => Length (Source) <= Target.Capacity;
 
    function Copy
      (Source   : Vector;
       Capacity : Count_Type := 0) return Vector
    with
+     Global => null,
      Pre    => Length (Source) <= Capacity and then Capacity in Capacity_Range;
 
    function To_Cursor
      (Container : Vector;
-      Index     : Extended_Index) return Cursor;
+      Index     : Extended_Index) return Cursor
+   with
+     Global => null;
 
-   function To_Index (Position : Cursor) return Extended_Index;
+   function To_Index (Position : Cursor) return Extended_Index with
+     Global => null;
 
    function Element
      (Container : Vector;
       Index     : Index_Type) return Element_Type
    with
+     Global => null,
      Pre    => First_Index (Container) <= Index
                  and then Index <= Last_Index (Container);
 
@@ -148,6 +171,7 @@ package Ada.Containers.Formal_Vectors is
      (Container : Vector;
       Position  : Cursor) return Element_Type
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
@@ -155,6 +179,7 @@ package Ada.Containers.Formal_Vectors is
       Index     : Index_Type;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => First_Index (Container) <= Index
                  and then Index <= Last_Index (Container);
 
@@ -163,9 +188,11 @@ package Ada.Containers.Formal_Vectors is
       Position  : Cursor;
       New_Item  : Element_Type)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Vector; Source : in out Vector) with
+     Global => null,
      Pre    => Length (Source) <= Target.Capacity;
 
    procedure Insert
@@ -173,6 +200,7 @@ package Ada.Containers.Formal_Vectors is
       Before    : Extended_Index;
       New_Item  : Vector)
    with
+     Global => null,
      Pre    => First_Index (Container) <= Before
                  and then Before <= Last_Index (Container) + 1
                  and then Length (Container) < Container.Capacity;
@@ -182,6 +210,7 @@ package Ada.Containers.Formal_Vectors is
       Before    : Cursor;
       New_Item  : Vector)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -192,6 +221,7 @@ package Ada.Containers.Formal_Vectors is
       New_Item  : Vector;
       Position  : out Cursor)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -202,6 +232,7 @@ package Ada.Containers.Formal_Vectors is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => First_Index (Container) <= Before
                  and then Before <= Last_Index (Container) + 1
                  and then Length (Container) + Count <= Container.Capacity;
@@ -212,6 +243,7 @@ package Ada.Containers.Formal_Vectors is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -223,6 +255,7 @@ package Ada.Containers.Formal_Vectors is
       Position  : out Cursor;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity
                  and then (Has_Element (Container, Before)
                             or else Before = No_Element);
@@ -231,6 +264,7 @@ package Ada.Containers.Formal_Vectors is
      (Container : in out Vector;
       New_Item  : Vector)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Prepend
@@ -238,12 +272,14 @@ package Ada.Containers.Formal_Vectors is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity;
 
    procedure Append
      (Container : in out Vector;
       New_Item  : Vector)
    with
+     Global => null,
      Pre    => Length (Container) < Container.Capacity;
 
    procedure Append
@@ -251,6 +287,7 @@ package Ada.Containers.Formal_Vectors is
       New_Item  : Element_Type;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Length (Container) + Count <= Container.Capacity;
 
    procedure Delete
@@ -258,6 +295,7 @@ package Ada.Containers.Formal_Vectors is
       Index     : Extended_Index;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => First_Index (Container) <= Index
                  and then Index <= Last_Index (Container) + 1;
 
@@ -266,102 +304,137 @@ package Ada.Containers.Formal_Vectors is
       Position  : in out Cursor;
       Count     : Count_Type := 1)
    with
+     Global => null,
      Pre    => Has_Element (Container, Position);
 
    procedure Delete_First
      (Container : in out Vector;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Global => null;
 
    procedure Delete_Last
      (Container : in out Vector;
-      Count     : Count_Type := 1);
+      Count     : Count_Type := 1)
+   with
+     Global => null;
 
-   procedure Reverse_Elements (Container : in out Vector);
+   procedure Reverse_Elements (Container : in out Vector) with
+     Global => null;
 
    procedure Swap (Container : in out Vector; I, J : Index_Type) with
-     Pre => First_Index (Container) <= I and then I <= Last_Index (Container)
+     Global => null,
+     Pre    => First_Index (Container) <= I
+                 and then I <= Last_Index (Container)
                  and then First_Index (Container) <= J
                  and then J <= Last_Index (Container);
 
    procedure Swap (Container : in out Vector; I, J : Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
 
-   function First_Index (Container : Vector) return Index_Type;
+   function First_Index (Container : Vector) return Index_Type with
+     Global => null;
 
-   function First (Container : Vector) return Cursor;
+   function First (Container : Vector) return Cursor with
+     Global => null;
 
    function First_Element (Container : Vector) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
-   function Last_Index (Container : Vector) return Extended_Index;
+   function Last_Index (Container : Vector) return Extended_Index with
+     Global => null;
 
-   function Last (Container : Vector) return Cursor;
+   function Last (Container : Vector) return Cursor with
+     Global => null;
 
    function Last_Element (Container : Vector) return Element_Type with
+     Global => null,
      Pre    => not Is_Empty (Container);
 
    function Next (Container : Vector; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Vector; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Previous (Container : Vector; Position : Cursor) return Cursor with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Previous (Container : Vector; Position : in out Cursor) with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Find_Index
      (Container : Vector;
       Item      : Element_Type;
-      Index     : Index_Type := Index_Type'First) return Extended_Index;
+      Index     : Index_Type := Index_Type'First) return Extended_Index
+   with
+     Global => null;
 
    function Find
      (Container : Vector;
       Item      : Element_Type;
       Position  : Cursor := No_Element) return Cursor
    with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Reverse_Find_Index
      (Container : Vector;
       Item      : Element_Type;
-      Index     : Index_Type := Index_Type'Last) return Extended_Index;
+      Index     : Index_Type := Index_Type'Last) return Extended_Index
+   with
+     Global => null;
 
    function Reverse_Find
      (Container : Vector;
       Item      : Element_Type;
       Position  : Cursor := No_Element) return Cursor
    with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Contains
      (Container : Vector;
-      Item      : Element_Type) return Boolean;
+      Item      : Element_Type) return Boolean
+   with
+     Global => null;
 
-   function Has_Element (Container : Vector; Position : Cursor) return Boolean;
+   function Has_Element (Container : Vector; Position : Cursor) return Boolean
+   with
+     Global => null;
 
    generic
       with function "<" (Left, Right : Element_Type) return Boolean is <>;
    package Generic_Sorting is
 
-      function Is_Sorted (Container : Vector) return Boolean;
+      function Is_Sorted (Container : Vector) return Boolean with
+        Global => null;
 
-      procedure Sort (Container : in out Vector);
+      procedure Sort (Container : in out Vector) with
+        Global => null;
 
-      procedure Merge (Target : in out Vector; Source : in out Vector);
+      procedure Merge (Target : in out Vector; Source : in out Vector) with
+        Global => null;
 
    end Generic_Sorting;
 
-   function Strict_Equal (Left, Right : Vector) return Boolean;
+   function Strict_Equal (Left, Right : Vector) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left (Container : Vector; Position : Cursor) return Vector with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Vector; Position : Cursor) return Vector with
+     Global => null,
      Pre    => Has_Element (Container, Position) or else Position = No_Element;
    --  Left returns a container containing all elements preceding Position
    --  (excluded) in Container. Right returns a container containing all

gcc/ada/a-cohama.adb

@@ -230,7 +230,8 @@ package body Ada.Containers.Hashed_Maps is
      (Container : aliased Map;
       Key       : Key_Type) return Constant_Reference_Type
    is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -238,7 +239,6 @@ package body Ada.Containers.Hashed_Maps is
       end if;
 
       declare
-         HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
          B  : Natural renames HT.Busy;
          L  : Natural renames HT.Lock;
       begin
@@ -351,7 +351,8 @@ package body Ada.Containers.Hashed_Maps is
    -------------
 
    function Element (Container : Map; Key : Key_Type) return Element_Type is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -484,7 +485,8 @@ package body Ada.Containers.Hashed_Maps is
    ----------
 
    function Find (Container : Map; Key : Key_Type) return Cursor is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -978,7 +980,8 @@ package body Ada.Containers.Hashed_Maps is
      (Container : aliased in out Map;
       Key       : Key_Type) return Reference_Type
    is
-      Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+      HT   : Hash_Table_Type renames Container.HT;
+      Node : constant Node_Access := Key_Ops.Find (HT, Key);
 
    begin
       if Node = null then
@@ -986,7 +989,6 @@ package body Ada.Containers.Hashed_Maps is
       end if;
 
       declare
-         HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
          B  : Natural renames HT.Busy;
          L  : Natural renames HT.Lock;
       begin
@@ -1181,7 +1183,7 @@ package body Ada.Containers.Hashed_Maps is
             return False;
          end if;
 
-         X := HT.Buckets (Key_Ops.Index (HT, Position.Node.Key));
+         X := HT.Buckets (Key_Ops.Checked_Index (HT, Position.Node.Key));
 
          for J in 1 .. HT.Length loop
             if X = Position.Node then

gcc/ada/a-cohase.adb

@@ -76,7 +76,7 @@ package body Ada.Containers.Hashed_Sets is
       Inserted : out Boolean);
 
    function Is_In
-     (HT  : Hash_Table_Type;
+     (HT  : aliased in out Hash_Table_Type;
       Key : Node_Access) return Boolean;
    pragma Inline (Is_In);
 
@@ -337,6 +337,7 @@ package body Ada.Containers.Hashed_Sets is
       Source : Set)
    is
       Tgt_Node : Node_Access;
+      Src_HT   : Hash_Table_Type renames Source'Unrestricted_Access.HT;
 
    begin
       if Target'Address = Source'Address then
@@ -344,7 +345,7 @@ package body Ada.Containers.Hashed_Sets is
          return;
       end if;
 
-      if Source.HT.Length = 0 then
+      if Src_HT.Length = 0 then
          return;
       end if;
 
@@ -353,12 +354,12 @@ package body Ada.Containers.Hashed_Sets is
            "attempt to tamper with cursors (set is busy)";
       end if;
 
-      if Source.HT.Length < Target.HT.Length then
+      if Src_HT.Length < Target.HT.Length then
          declare
             Src_Node : Node_Access;
 
          begin
-            Src_Node := HT_Ops.First (Source.HT);
+            Src_Node := HT_Ops.First (Src_HT);
             while Src_Node /= null loop
                Tgt_Node := Element_Keys.Find (Target.HT, Src_Node.Element);
 
@@ -367,14 +368,14 @@ package body Ada.Containers.Hashed_Sets is
                   Free (Tgt_Node);
                end if;
 
-               Src_Node := HT_Ops.Next (Source.HT, Src_Node);
+               Src_Node := HT_Ops.Next (Src_HT, Src_Node);
             end loop;
          end;
 
       else
          Tgt_Node := HT_Ops.First (Target.HT);
          while Tgt_Node /= null loop
-            if Is_In (Source.HT, Tgt_Node) then
+            if Is_In (Src_HT, Tgt_Node) then
                declare
                   X : Node_Access := Tgt_Node;
                begin
@@ -391,6 +392,8 @@ package body Ada.Containers.Hashed_Sets is
    end Difference;
 
    function Difference (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -399,11 +402,11 @@ package body Ada.Containers.Hashed_Sets is
          return Empty_Set;
       end if;
 
-      if Left.HT.Length = 0 then
+      if Left_HT.Length = 0 then
          return Empty_Set;
       end if;
 
-      if Right.HT.Length = 0 then
+      if Right_HT.Length = 0 then
          return Left;
       end if;
 
@@ -427,10 +430,15 @@ package body Ada.Containers.Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if not Is_In (Right.HT, L_Node) then
+            if not Is_In (Right_HT, L_Node) then
                declare
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
                   J : constant Hash_Type :=
-                    Hash (L_Node.Element) mod Buckets'Length;
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
 
                   Bucket : Node_Access renames Buckets (J);
 
@@ -445,7 +453,7 @@ package body Ada.Containers.Hashed_Sets is
       --  Start of processing for Iterate_Left
 
       begin
-         Iterate (Left.HT);
+         Iterate (Left_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -499,6 +507,20 @@ package body Ada.Containers.Hashed_Sets is
       pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
       pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
 
+      --  AI05-0022 requires that a container implementation detect element
+      --  tampering by a generic actual subprogram. However, the following case
+      --  falls outside the scope of that AI. Randy Brukardt explained on the
+      --  ARG list on 2013/02/07 that:
+
+      --  (Begin Quote):
+      --  But for an operation like "<" [the ordered set analog of
+      --  Equivalent_Elements], there is no need to "dereference" a cursor
+      --  after the call to the generic formal parameter function, so nothing
+      --  bad could happen if tampering is undetected. And the operation can
+      --  safely return a result without a problem even if an element is
+      --  deleted from the container.
+      --  (End Quote).
+
       return Equivalent_Elements (Left.Node.Element, Right.Node.Element);
    end Equivalent_Elements;
 
@@ -587,7 +609,8 @@ package body Ada.Containers.Hashed_Sets is
      (Container : Set;
       Item      : Element_Type) return Cursor
    is
-      Node : constant Node_Access := Element_Keys.Find (Container.HT, Item);
+      HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+      Node : constant Node_Access := Element_Keys.Find (HT, Item);
 
    begin
       if Node = null then
@@ -807,6 +830,7 @@ package body Ada.Containers.Hashed_Sets is
      (Target : in out Set;
       Source : Set)
    is
+      Src_HT   : Hash_Table_Type renames Source'Unrestricted_Access.HT;
       Tgt_Node : Node_Access;
 
    begin
@@ -826,7 +850,7 @@ package body Ada.Containers.Hashed_Sets is
 
       Tgt_Node := HT_Ops.First (Target.HT);
       while Tgt_Node /= null loop
-         if Is_In (Source.HT, Tgt_Node) then
+         if Is_In (Src_HT, Tgt_Node) then
             Tgt_Node := HT_Ops.Next (Target.HT, Tgt_Node);
 
          else
@@ -842,6 +866,8 @@ package body Ada.Containers.Hashed_Sets is
    end Intersection;
 
    function Intersection (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -876,10 +902,15 @@ package body Ada.Containers.Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if Is_In (Right.HT, L_Node) then
+            if Is_In (Right_HT, L_Node) then
                declare
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
                   J : constant Hash_Type :=
-                    Hash (L_Node.Element) mod Buckets'Length;
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
 
                   Bucket : Node_Access renames Buckets (J);
 
@@ -894,7 +925,7 @@ package body Ada.Containers.Hashed_Sets is
       --  Start of processing for Iterate_Left
 
       begin
-         Iterate (Left.HT);
+         Iterate (Left_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -917,7 +948,10 @@ package body Ada.Containers.Hashed_Sets is
    -- Is_In --
    -----------
 
-   function Is_In (HT : Hash_Table_Type; Key : Node_Access) return Boolean is
+   function Is_In
+     (HT : aliased in out Hash_Table_Type;
+      Key : Node_Access) return Boolean
+   is
    begin
       return Element_Keys.Find (HT, Key.Element) /= null;
    end Is_In;
@@ -927,6 +961,8 @@ package body Ada.Containers.Hashed_Sets is
    ---------------
 
    function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
+      Subset_HT   : Hash_Table_Type renames Subset'Unrestricted_Access.HT;
+      Of_Set_HT   : Hash_Table_Type renames Of_Set'Unrestricted_Access.HT;
       Subset_Node : Node_Access;
 
    begin
@@ -938,12 +974,12 @@ package body Ada.Containers.Hashed_Sets is
          return False;
       end if;
 
-      Subset_Node := HT_Ops.First (Subset.HT);
+      Subset_Node := HT_Ops.First (Subset_HT);
       while Subset_Node /= null loop
-         if not Is_In (Of_Set.HT, Subset_Node) then
+         if not Is_In (Of_Set_HT, Subset_Node) then
             return False;
          end if;
-         Subset_Node := HT_Ops.Next (Subset.HT, Subset_Node);
+         Subset_Node := HT_Ops.Next (Subset_HT, Subset_Node);
       end loop;
 
       return True;
@@ -1072,6 +1108,8 @@ package body Ada.Containers.Hashed_Sets is
    -------------
 
    function Overlap (Left, Right : Set) return Boolean is
+      Left_HT   : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT  : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Left_Node : Node_Access;
 
    begin
@@ -1083,12 +1121,12 @@ package body Ada.Containers.Hashed_Sets is
          return True;
       end if;
 
-      Left_Node := HT_Ops.First (Left.HT);
+      Left_Node := HT_Ops.First (Left_HT);
       while Left_Node /= null loop
-         if Is_In (Right.HT, Left_Node) then
+         if Is_In (Right_HT, Left_Node) then
             return True;
          end if;
-         Left_Node := HT_Ops.Next (Left.HT, Left_Node);
+         Left_Node := HT_Ops.Next (Left_HT, Left_Node);
       end loop;
 
       return False;
@@ -1255,13 +1293,25 @@ package body Ada.Containers.Hashed_Sets is
      (Target : in out Set;
       Source : Set)
    is
+      Tgt_HT : Hash_Table_Type renames Target.HT;
+      Src_HT : Hash_Table_Type renames Source.HT'Unrestricted_Access.all;
+
+      --  Per AI05-0022, the container implementation is required to detect
+      --  element tampering by a generic actual subprogram.
+
+      TB : Natural renames Tgt_HT.Busy;
+      TL : Natural renames Tgt_HT.Lock;
+
+      SB : Natural renames Src_HT.Busy;
+      SL : Natural renames Src_HT.Lock;
+
    begin
       if Target'Address = Source'Address then
          Clear (Target);
          return;
       end if;
 
-      if Target.HT.Busy > 0 then
+      if TB > 0 then
          raise Program_Error with
            "attempt to tamper with cursors (set is busy)";
       end if;
@@ -1269,8 +1319,8 @@ package body Ada.Containers.Hashed_Sets is
       declare
          N : constant Count_Type := Target.Length + Source.Length;
       begin
-         if N > HT_Ops.Capacity (Target.HT) then
-            HT_Ops.Reserve_Capacity (Target.HT, N);
+         if N > HT_Ops.Capacity (Tgt_HT) then
+            HT_Ops.Reserve_Capacity (Tgt_HT, N);
          end if;
       end;
 
@@ -1287,9 +1337,9 @@ package body Ada.Containers.Hashed_Sets is
 
             procedure Process (Src_Node : Node_Access) is
                E : Element_Type renames Src_Node.Element;
-               B : Buckets_Type renames Target.HT.Buckets.all;
+               B : Buckets_Type renames Tgt_HT.Buckets.all;
                J : constant Hash_Type := Hash (E) mod B'Length;
-               N : Count_Type renames Target.HT.Length;
+               N : Count_Type renames Tgt_HT.Length;
 
             begin
                B (J) := new Node_Type'(E, B (J));
@@ -1299,7 +1349,29 @@ package body Ada.Containers.Hashed_Sets is
          --  Start of processing for Iterate_Source_When_Empty_Target
 
          begin
-            Iterate (Source.HT);
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            Iterate (Src_HT);
+
+            SL := SL - 1;
+            SB := SB - 1;
+
+            TL := TL - 1;
+            TB := TB - 1;
+
+         exception
+            when others =>
+               SL := SL - 1;
+               SB := SB - 1;
+
+               TL := TL - 1;
+               TB := TB - 1;
+
+               raise;
          end Iterate_Source_When_Empty_Target;
 
       else
@@ -1315,9 +1387,9 @@ package body Ada.Containers.Hashed_Sets is
 
             procedure Process (Src_Node : Node_Access) is
                E : Element_Type renames Src_Node.Element;
-               B : Buckets_Type renames Target.HT.Buckets.all;
+               B : Buckets_Type renames Tgt_HT.Buckets.all;
                J : constant Hash_Type := Hash (E) mod B'Length;
-               N : Count_Type renames Target.HT.Length;
+               N : Count_Type renames Tgt_HT.Length;
 
             begin
                if B (J) = null then
@@ -1360,12 +1432,36 @@ package body Ada.Containers.Hashed_Sets is
          --  Start of processing for Iterate_Source
 
          begin
-            Iterate (Source.HT);
+            TB := TB + 1;
+            TL := TL + 1;
+
+            SB := SB + 1;
+            SL := SL + 1;
+
+            Iterate (Src_HT);
+
+            SL := SL - 1;
+            SB := SB - 1;
+
+            TL := TL - 1;
+            TB := TB - 1;
+
+         exception
+            when others =>
+               SL := SL - 1;
+               SB := SB - 1;
+
+               TL := TL - 1;
+               TB := TB - 1;
+
+               raise;
          end Iterate_Source;
       end if;
    end Symmetric_Difference;
 
    function Symmetric_Difference (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+      Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -1403,10 +1499,17 @@ package body Ada.Containers.Hashed_Sets is
 
          procedure Process (L_Node : Node_Access) is
          begin
-            if not Is_In (Right.HT, L_Node) then
+            if not Is_In (Right_HT, L_Node) then
                declare
                   E : Element_Type renames L_Node.Element;
-                  J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
+                  J : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
 
                begin
                   Buckets (J) := new Node_Type'(E, Buckets (J));
@@ -1418,7 +1521,7 @@ package body Ada.Containers.Hashed_Sets is
       --  Start of processing for Iterate_Left
 
       begin
-         Iterate (Left.HT);
+         Iterate (Left_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -1437,10 +1540,17 @@ package body Ada.Containers.Hashed_Sets is
 
          procedure Process (R_Node : Node_Access) is
          begin
-            if not Is_In (Left.HT, R_Node) then
+            if not Is_In (Left_HT, R_Node) then
                declare
                   E : Element_Type renames R_Node.Element;
-                  J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+                  --  Per AI05-0022, the container implementation is required
+                  --  to detect element tampering by a generic actual
+                  --  subprogram, hence the use of Checked_Index instead of a
+                  --  simple invocation of generic formal Hash.
+
+                  J : constant Hash_Type :=
+                    HT_Ops.Checked_Index (Right_HT, Buckets.all, R_Node);
 
                begin
                   Buckets (J) := new Node_Type'(E, Buckets (J));
@@ -1452,7 +1562,7 @@ package body Ada.Containers.Hashed_Sets is
       --  Start of processing for Iterate_Right
 
       begin
-         Iterate (Right.HT);
+         Iterate (Right_HT);
       exception
          when others =>
             HT_Ops.Free_Hash_Table (Buckets);
@@ -1547,6 +1657,8 @@ package body Ada.Containers.Hashed_Sets is
    end Union;
 
    function Union (Left, Right : Set) return Set is
+      Left_HT  : Hash_Table_Type renames Left.HT'Unrestricted_Access.all;
+      Right_HT : Hash_Table_Type renames Right.HT'Unrestricted_Access.all;
       Buckets  : HT_Types.Buckets_Access;
       Length   : Count_Type;
 
@@ -1588,12 +1700,29 @@ package body Ada.Containers.Hashed_Sets is
             Buckets (J) := new Node_Type'(L_Node.Element, Buckets (J));
          end Process;
 
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram, hence the use of
+         --  Checked_Index instead of a simple invocation of generic formal
+         --  Hash.
+
+         B : Integer renames Left_HT.Busy;
+         L : Integer renames Left_HT.Lock;
+
       --  Start of processing for Iterate_Left
 
       begin
-         Iterate (Left.HT);
+         B := B + 1;
+         L := L + 1;
+
+         Iterate (Left_HT);
+
+         L := L - 1;
+         B := B - 1;
       exception
          when others =>
+            L := L - 1;
+            B := B - 1;
+
             HT_Ops.Free_Hash_Table (Buckets);
             raise;
       end Iterate_Left;
@@ -1629,12 +1758,41 @@ package body Ada.Containers.Hashed_Sets is
             Length := Length + 1;
          end Process;
 
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram, hence the use of
+         --  Checked_Index instead of a simple invocation of generic formal
+         --  Hash.
+
+         LB : Integer renames Left_HT.Busy;
+         LL : Integer renames Left_HT.Lock;
+
+         RB : Integer renames Right_HT.Busy;
+         RL : Integer renames Right_HT.Lock;
+
       --  Start of processing for Iterate_Right
 
       begin
-         Iterate (Right.HT);
+         LB := LB + 1;
+         LL := LL + 1;
+
+         RB := RB + 1;
+         RL := RL + 1;
+
+         Iterate (Right_HT);
+
+         RL := RL - 1;
+         RB := RB - 1;
+
+         LL := LL - 1;
+         LB := LB - 1;
       exception
          when others =>
+            RL := RL - 1;
+            RB := RB - 1;
+
+            LL := LL - 1;
+            LB := LB - 1;
+
             HT_Ops.Free_Hash_Table (Buckets);
             raise;
       end Iterate_Right;
@@ -1675,7 +1833,9 @@ package body Ada.Containers.Hashed_Sets is
             return False;
          end if;
 
-         X := HT.Buckets (Element_Keys.Index (HT, Position.Node.Element));
+         X := HT.Buckets (Element_Keys.Checked_Index
+                            (HT,
+                             Position.Node.Element));
 
          for J in 1 .. HT.Length loop
             if X = Position.Node then
@@ -1769,7 +1929,8 @@ package body Ada.Containers.Hashed_Sets is
         (Container : aliased Set;
          Key       : Key_Type) return Constant_Reference_Type
       is
-         Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
 
       begin
          if Node = null then
@@ -1777,7 +1938,6 @@ package body Ada.Containers.Hashed_Sets is
          end if;
 
          declare
-            HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
             B : Natural renames HT.Busy;
             L : Natural renames HT.Lock;
          begin
@@ -1831,11 +1991,12 @@ package body Ada.Containers.Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Element_Type
       is
-         Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
 
       begin
          if Node = null then
-            raise Constraint_Error with "key not in map";  -- ??? "set"
+            raise Constraint_Error with "key not in set";
          end if;
 
          return Node.Element;
@@ -1875,7 +2036,8 @@ package body Ada.Containers.Hashed_Sets is
         (Container : Set;
          Key       : Key_Type) return Cursor
       is
-         Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+         HT   : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+         Node : constant Node_Access := Key_Keys.Find (HT, Key);
 
       begin
          if Node = null then
@@ -2016,7 +2178,8 @@ package body Ada.Containers.Hashed_Sets is
            (Vet (Position),
             "bad cursor in Update_Element_Preserving_Key");
 
-         Indx := HT_Ops.Index (HT, Position.Node);
+         --  Per AI05-0022, the container implementation is required to detect
+         --  element tampering by a generic actual subprogram.
 
          declare
             E : Element_Type renames Position.Node.Element;
@@ -2025,12 +2188,16 @@ package body Ada.Containers.Hashed_Sets is
             B : Natural renames HT.Busy;
             L : Natural renames HT.Lock;
 
+            Eq : Boolean;
+
          begin
             B := B + 1;
             L := L + 1;
 
             begin
+               Indx := HT_Ops.Index (HT, Position.Node);
                Process (E);
+               Eq := Equivalent_Keys (K, Key (E));
             exception
                when others =>
                   L := L - 1;
@@ -2041,8 +2208,7 @@ package body Ada.Containers.Hashed_Sets is
             L := L - 1;
             B := B - 1;
 
-            if Equivalent_Keys (K, Key (E)) then
-               pragma Assert (Hash (K) = Hash (E));
+            if Eq then
                return;
             end if;
          end;

gcc/ada/adabkend.adb

@@ -272,6 +272,12 @@ package body Adabkend is
             elsif not Is_Switch (Argv) then
                Add_File (Argv);
 
+            --  We must recognize -nostdinc to suppress visibility on the
+            --  standard GNAT RTL sources.
+
+            elsif Argv (Argv'First + 1 .. Argv'Last) = "nostdinc" then
+               Opt.No_Stdinc := True;
+
             --  Front end switch
 
             elsif Is_Front_End_Switch (Argv) then

gcc/ada/gnat_rm.texi

@@ -6454,11 +6454,11 @@ pragma Stream_Convert (
 @end smallexample
 
 @noindent
-This pragma provides an efficient way of providing stream functions for
-types defined in packages.  Not only is it simpler to use than declaring
-the necessary functions with attribute representation clauses, but more
-significantly, it allows the declaration to made in such a way that the
-stream packages are not loaded unless they are needed.  The use of
+This pragma provides an efficient way of providing user-defined stream
+attributes.  Not only is it simpler to use than specifying the attributes
+directly, but more importantly, it allows the specification to be made in such
+a way that the predefined unit Ada.Streams is not loaded unless it is actually
+needed (i.e. unless the stream attributes are actually used); the use of
 the Stream_Convert pragma adds no overhead at all, unless the stream
 attributes are actually used on the designated type.
 

gcc/ada/sem_prag.adb

@@ -2333,187 +2333,17 @@ package body Sem_Prag is
    --------------------------------------------
 
    procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
-      Pack_Id   : constant Entity_Id := Defining_Entity (Parent (Parent (N)));
-      Prag_Init : constant Node_Id   :=
-                    Get_Pragma (Pack_Id, Pragma_Initializes);
-      --  The related pragma Initializes
-
-      Vars : Elist_Id := No_Elist;
-      --  A list of all variables declared in pragma Initializes
-
-      procedure Collect_Variables;
-      --  Inspect the initialization list of pragma Initializes and collect the
-      --  entities of all variables declared within the related package.
-
-      function Match_Variable (N : Node_Id) return Traverse_Result;
-      --  Determine whether arbitrary node N denotes a variable declared in the
-      --  visible declarations of the related package.
-
-      procedure Report_Unused_Variables;
-      --  Emit errors for all variables found in list Vars
-
-      -----------------------
-      -- Collect_Variables --
-      -----------------------
-
-      procedure Collect_Variables is
-         procedure Collect_Variable (Item : Node_Id);
-         --  Determine whether Item denotes a variable that appears in the
-         --  related package and if it does, add it to list Vars.
-
-         ----------------------
-         -- Collect_Variable --
-         ----------------------
-
-         procedure Collect_Variable (Item : Node_Id) is
-            Item_Id : Entity_Id;
-
-         begin
-            if Is_Entity_Name (Item) and then Present (Entity (Item)) then
-               Item_Id := Entity (Item);
-
-               --  The item is a variable declared in the related package
-
-               if Ekind (Item_Id) = E_Variable
-                 and then Scope (Item_Id) = Pack_Id
-               then
-                  Add_Item (Item_Id, Vars);
-               end if;
-            end if;
-         end Collect_Variable;
-
-         --  Local variables
-
-         Inits : constant Node_Id :=
-                   Get_Pragma_Arg
-                     (First (Pragma_Argument_Associations (Prag_Init)));
-         Init  : Node_Id;
-
-      --  Start of processing for Collect_Variables
-
-      begin
-         --  Multiple initialization items appear as an aggregate
-
-         if Nkind (Inits) = N_Aggregate
-           and then Present (Expressions (Inits))
-         then
-            Init := First (Expressions (Inits));
-            while Present (Init) loop
-               Collect_Variable (Init);
-
-               Next (Init);
-            end loop;
-
-         --  Single initialization item
-
-         else
-            Collect_Variable (Inits);
-         end if;
-      end Collect_Variables;
-
-      --------------------
-      -- Match_Variable --
-      --------------------
-
-      function Match_Variable (N : Node_Id) return Traverse_Result is
-         Var_Id : Entity_Id;
-
-      begin
-         --  Find a variable declared within the related package and try to
-         --  remove it from the list of collected variables found in pragma
-         --  Initializes.
-
-         if Is_Entity_Name (N)
-           and then Present (Entity (N))
-         then
-            Var_Id := Entity (N);
-
-            if Ekind (Var_Id) = E_Variable
-              and then Scope (Var_Id) = Pack_Id
-            then
-               Remove (Vars, Var_Id);
-            end if;
-         end if;
-
-         return OK;
-      end Match_Variable;
-
-      procedure Match_Variables is new Traverse_Proc (Match_Variable);
-
-      -----------------------------
-      -- Report_Unused_Variables --
-      -----------------------------
-
-      procedure Report_Unused_Variables is
-         Posted   : Boolean := False;
-         Var_Elmt : Elmt_Id;
-         Var_Id   : Entity_Id;
-
-      begin
-         if Present (Vars) then
-            Var_Elmt := First_Elmt (Vars);
-            while Present (Var_Elmt) loop
-               Var_Id := Node (Var_Elmt);
-
-               if not Posted then
-                  Posted := True;
-                  Error_Msg_Name_1 := Name_Initial_Condition;
-                  Error_Msg_N
-                    ("expression of % must mention the following variables",
-                     N);
-               end if;
-
-               Error_Msg_Sloc := Sloc (Var_Id);
-               Error_Msg_NE ("\  & declared #", N, Var_Id);
-
-               Next_Elmt (Var_Elmt);
-            end loop;
-         end if;
-      end Report_Unused_Variables;
-
       Expr : constant Node_Id :=
                Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-      Errors : constant Nat     := Serious_Errors_Detected;
-
-   --  Start of processing for Analyze_Initial_Condition_In_Decl_Part
 
    begin
       Set_Analyzed (N);
 
-      --  Pragma Initial_Condition depends on the names enumerated in pragma
-      --  Initializes. Without those, the analysis cannot take place.
-
-      if No (Prag_Init) then
-         Error_Msg_Name_1 := Name_Initial_Condition;
-         Error_Msg_Name_2 := Name_Initializes;
-
-         Error_Msg_N ("% requires the presence of aspect or pragma %", N);
-         return;
-      end if;
-
       --  The expression is preanalyzed because it has not been moved to its
       --  final place yet. A direct analysis may generate side effects and this
       --  is not desired at this point.
 
       Preanalyze_And_Resolve (Expr, Standard_Boolean);
-
-      --  Perform variable matching only when the expression is legal
-
-      if Serious_Errors_Detected = Errors then
-         Collect_Variables;
-
-         --  Verify that all variables mentioned in pragma Initializes are used
-         --  in the expression of pragma Initial_Condition.
-
-         Match_Variables (Expr);
-      end if;
-
-      --  Emit errors for all variables that should participate in the
-      --  expression of pragma Initial_Condition.
-
-      if Serious_Errors_Detected = Errors then
-         Report_Unused_Variables;
-      end if;
    end Analyze_Initial_Condition_In_Decl_Part;
 
    --------------------------------------

gcc/ada/tbuild.adb

@@ -649,6 +649,7 @@ package body Tbuild is
      (Def_Id : Entity_Id;
       Loc    : Source_Ptr) return Node_Id
    is
+      pragma Assert (Present (Def_Id) and then Nkind (Def_Id) in N_Entity);
       Occurrence : Node_Id;
 
    begin
@@ -725,7 +726,7 @@ package body Tbuild is
      (Def_Id : Entity_Id;
       Loc    : Source_Ptr) return Node_Id
    is
-      pragma Assert (Nkind (Def_Id) in N_Entity);
+      pragma Assert (Present (Def_Id) and then Nkind (Def_Id) in N_Entity);
       Occurrence : Node_Id;
    begin
       Occurrence := New_Node (N_Identifier, Loc);