[Ada] Add Reference and Constant_Reference functions to formal containers

gcc/ada/

	* libgnat/a-cfdlli.ads, libgnat/a-cfdlli.adb
	libgnat/a-cfinve.ads, libgnat/a-cfinve.adb,
	libgnat/a-cofove.ads, libgnat/a-cofove.adb,
	libgnat/a-coboho.ads, libgnat/a-coboho.adb (Constant_Reference):
	Get a read-only access to an element of the container.
	(At_End): Ghost functions used to express pledges in the
	postcondition of Reference.
	(Reference): Get a read-write access to an element of the
	container.
	* libgnat/a-cfhama.ads, libgnat/a-cfhama.adb,
	libgnat/a-cforma.ads, libgnat/a-cforma.adb: The full view of the
	Map type is no longer a tagged type, but a wrapper over this
	tagged type. This is to avoid issues with dispatching result in
	At_End functions.
	(Constant_Reference): Get a read-only access to an element of
	the container.
	(At_End): Ghost functions used to express pledges in the
	postcondition of Reference.
	(Reference): Get a read-write access to an element of the
	container.

	* libgnat/a-cfhase.ads, libgnat/a-cfhase.adb,
	libgnat/a-cforse.ads, libgnat/a-cforse.adb: The full view of the
	Map type is no longer a tagged type, but a wrapper over this
	tagged type.
	(Constant_Reference): Get a read-only access to an element of
	the container.
	* libgnat/a-cofuse.ads, libgnat/a-cofuve.ads (Copy_Element):
	Expression function used to cause SPARK to make sure
	Element_Type is copiable.
	* libgnat/a-cofuma.ads (Copy_Key): Expression function used to
	cause SPARK to make sure Key_Type is copiable.
	(Copy_Element): Expression function used to cause SPARK to make
	sure Element_Type is copiable.

19 files changed, 1073 insertions, 370 deletions

diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb
index d96a8f6..b289def 100644
--- a/gcc/ada/libgnat/a-cfdlli.adb
+++ b/gcc/ada/libgnat/a-cfdlli.adb
@@ -188,6 +188,22 @@ is
       Free (Container, X);
    end Clear;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased List;
+      Position  : Cursor) return not null access constant Element_Type
+   is
+   begin
+      if not Has_Element (Container => Container, Position  => Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      return Container.Nodes (Position.Node).Element'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -1376,6 +1392,22 @@ is
       return (Node => Container.Nodes (Position.Node).Prev);
    end Previous;
 
+   ---------------
+   -- Reference --
+   ---------------
+
+   function Reference
+     (Container : not null access List;
+      Position  : Cursor) return not null access Element_Type
+   is
+   begin
+      if not Has_Element (Container.all, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      return Container.Nodes (Position.Node).Element'Access;
+   end Reference;
+
    ---------------------
    -- Replace_Element --
    ---------------------
diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
index e3a2de6..8713d33 100644
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -387,6 +387,53 @@ is
                 Model (Container),
                 P.Get (Positions (Container), Position));
 
+   function At_End (E : access constant List) return access constant List
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased List;
+      Position  : Cursor) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Constant_Reference'Result.all =
+         Element (Model (Container), P.Get (Positions (Container), Position));
+
+   function Reference
+     (Container : not null access List;
+      Position  : Cursor) return not null access Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container.all, Position),
+     Post   =>
+      Length (Container.all) = Length (At_End (Container).all)
+
+         --  Cursors are preserved
+
+         and Positions (Container.all) = Positions (At_End (Container).all)
+
+         --  Container will have Result.all at position Position
+
+         and At_End (Reference'Result).all =
+           Element (Model (At_End (Container).all),
+                    P.Get (Positions (At_End (Container).all), Position))
+
+         --  All other elements are preserved
+
+         and M.Equal_Except
+               (Model (Container.all),
+                Model (At_End (Container).all),
+                P.Get (Positions (At_End (Container).all), Position));
+
    procedure Move (Target : in out List; Source : in out List) with
      Global => null,
      Pre    => Target.Capacity >= Length (Source),
@@ -1609,7 +1656,7 @@ private
    type Node_Type is record
       Prev    : Count_Type'Base := -1;
       Next    : Count_Type;
-      Element : Element_Type;
+      Element : aliased Element_Type;
    end record;
 
    function "=" (L, R : Node_Type) return Boolean is abstract;
diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb
index 17971b2..179b400 100644
--- a/gcc/ada/libgnat/a-cfhama.adb
+++ b/gcc/ada/libgnat/a-cfhama.adb
@@ -109,20 +109,21 @@ is
          ENode : Count_Type;
 
       begin
-         Node := Left.First.Node;
+         Node := First (Left).Node;
          while Node /= 0 loop
             ENode :=
               Find
                 (Container => Right,
-                 Key       => Left.Nodes (Node).Key).Node;
+                 Key       => Left.Content.Nodes (Node).Key).Node;
 
             if ENode = 0 or else
-              Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+              Right.Content.Nodes (ENode).Element /=
+              Left.Content.Nodes (Node).Element
             then
                return False;
             end if;
 
-            Node := HT_Ops.Next (Left, Node);
+            Node := HT_Ops.Next (Left.Content, Node);
          end loop;
 
          return True;
@@ -145,7 +146,7 @@ is
       --------------------
 
       procedure Insert_Element (Source_Node : Count_Type) is
-         N : Node_Type renames Source.Nodes (Source_Node);
+         N : Node_Type renames Source.Content.Nodes (Source_Node);
       begin
          Insert (Target, N.Key, N.Element);
       end Insert_Element;
@@ -164,7 +165,7 @@ is
 
       Clear (Target);
 
-      Insert_Elements (Source);
+      Insert_Elements (Source.Content);
    end Assign;
 
    --------------
@@ -173,7 +174,7 @@ is
 
    function Capacity (Container : Map) return Count_Type is
    begin
-      return Container.Nodes'Length;
+      return Container.Content.Nodes'Length;
    end Capacity;
 
    -----------
@@ -182,9 +183,44 @@ is
 
    procedure Clear (Container : in out Map) is
    begin
-      HT_Ops.Clear (Container);
+      HT_Ops.Clear (Container.Content);
    end Clear;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Position  : Cursor) return not null access constant Element_Type
+   is
+   begin
+      if not Has_Element (Container, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      pragma Assert
+        (Vet (Container, Position),
+         "bad cursor in function Constant_Reference");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Constant_Reference;
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Key       : Key_Type) return not null access constant Element_Type
+   is
+      Node : constant Count_Type := Find (Container, Key).Node;
+
+   begin
+      if Node = 0 then
+         raise Constraint_Error with
+           "no element available because key not in map";
+      end if;
+
+      return Container.Content.Nodes (Node).Element'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -214,18 +250,18 @@ is
          raise Capacity_Error;
       end if;
 
-      Target.Length := Source.Length;
-      Target.Free := Source.Free;
+      Target.Content.Length := Source.Content.Length;
+      Target.Content.Free := Source.Content.Free;
 
       H := 1;
       while H <= Source.Modulus loop
-         Target.Buckets (H) := Source.Buckets (H);
+         Target.Content.Buckets (H) := Source.Content.Buckets (H);
          H := H + 1;
       end loop;
 
       N := 1;
       while N <= Source.Capacity loop
-         Target.Nodes (N) := Source.Nodes (N);
+         Target.Content.Nodes (N) := Source.Content.Nodes (N);
          N := N + 1;
       end loop;
 
@@ -255,7 +291,7 @@ is
       X : Count_Type;
 
    begin
-      Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
+      Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
 
       if X = 0 then
          raise Constraint_Error with "attempt to delete key not in map";
@@ -273,7 +309,7 @@ is
 
       pragma Assert (Vet (Container, Position), "bad cursor in Delete");
 
-      HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
+      HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node);
 
       Free (Container, Position.Node);
       Position := No_Element;
@@ -292,7 +328,7 @@ is
            "no element available because key not in map";
       end if;
 
-      return Container.Nodes (Node).Element;
+      return Container.Content.Nodes (Node).Element;
    end Element;
 
    function Element (Container : Map; Position : Cursor) return Element_Type is
@@ -304,7 +340,7 @@ is
       pragma Assert
         (Vet (Container, Position), "bad cursor in function Element");
 
-      return Container.Nodes (Position.Node).Element;
+      return Container.Content.Nodes (Position.Node).Element;
    end Element;
 
    ---------------------
@@ -326,7 +362,7 @@ is
    procedure Exclude (Container : in out Map; Key : Key_Type) is
       X : Count_Type;
    begin
-      Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
+      Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
       Free (Container, X);
    end Exclude;
 
@@ -335,7 +371,7 @@ 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.Content, Key);
 
    begin
       if Node = 0 then
@@ -350,7 +386,7 @@ is
    -----------
 
    function First (Container : Map) return Cursor is
-      Node : constant Count_Type := HT_Ops.First (Container);
+      Node : constant Count_Type := HT_Ops.First (Container.Content);
 
    begin
       if Node = 0 then
@@ -407,7 +443,7 @@ is
       ----------
 
       function Keys (Container : Map) return K.Sequence is
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : K.Sequence;
 
       begin
@@ -415,8 +451,8 @@ is
          --  for their postconditions.
 
          while Position /= 0 loop
-            R := K.Add (R, Container.Nodes (Position).Key);
-            Position := HT_Ops.Next (Container, Position);
+            R := K.Add (R, Container.Content.Nodes (Position).Key);
+            Position := HT_Ops.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -458,7 +494,7 @@ is
       -----------
 
       function Model (Container : Map) return M.Map is
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : M.Map;
 
       begin
@@ -469,10 +505,10 @@ is
             R :=
               M.Add
                 (Container => R,
-                 New_Key   => Container.Nodes (Position).Key,
-                 New_Item  => Container.Nodes (Position).Element);
+                 New_Key   => Container.Content.Nodes (Position).Key,
+                 New_Item  => Container.Content.Nodes (Position).Element);
 
-            Position := HT_Ops.Next (Container, Position);
+            Position := HT_Ops.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -484,7 +520,7 @@ is
 
       function Positions (Container : Map) return P.Map is
          I        : Count_Type := 1;
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : P.Map;
 
       begin
@@ -494,7 +530,7 @@ is
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
             pragma Assert (P.Length (R) = I);
-            Position := HT_Ops.Next (Container, Position);
+            Position := HT_Ops.Next (Container.Content, Position);
             I := I + 1;
          end loop;
 
@@ -511,8 +547,8 @@ is
    begin
       if X /= 0 then
          pragma Assert (X <= HT.Capacity);
-         HT.Nodes (X).Has_Element := False;
-         HT_Ops.Free (HT, X);
+         HT.Content.Nodes (X).Has_Element := False;
+         HT_Ops.Free (HT.Content, X);
       end if;
    end Free;
 
@@ -525,8 +561,8 @@ is
         new HT_Ops.Generic_Allocate (Set_Element);
 
    begin
-      Allocate (HT, Node);
-      HT.Nodes (Node).Has_Element := True;
+      Allocate (HT.Content, Node);
+      HT.Content.Nodes (Node).Has_Element := True;
    end Generic_Allocate;
 
    -----------------
@@ -536,7 +572,7 @@ is
    function Has_Element (Container : Map; Position : Cursor) return Boolean is
    begin
       if Position.Node = 0
-        or else not Container.Nodes (Position.Node).Has_Element
+        or else not Container.Content.Nodes (Position.Node).Has_Element
       then
          return False;
       else
@@ -570,7 +606,7 @@ is
 
       if not Inserted then
          declare
-            N : Node_Type renames Container.Nodes (Position.Node);
+            N : Node_Type renames Container.Content.Nodes (Position.Node);
          begin
             N.Key := Key;
             N.Element := New_Item;
@@ -625,7 +661,7 @@ is
    --  Start of processing for Insert
 
    begin
-      Local_Insert (Container, Key, Position.Node, Inserted);
+      Local_Insert (Container.Content, Key, Position.Node, Inserted);
    end Insert;
 
    procedure Insert
@@ -668,7 +704,7 @@ is
 
       pragma Assert (Vet (Container, Position), "bad cursor in function Key");
 
-      return Container.Nodes (Position.Node).Key;
+      return Container.Content.Nodes (Position.Node).Key;
    end Key;
 
    ------------
@@ -677,7 +713,7 @@ is
 
    function Length (Container : Map) return Count_Type is
    begin
-      return Container.Length;
+      return Container.Content.Length;
    end Length;
 
    ----------
@@ -688,7 +724,7 @@ is
      (Target : in out Map;
       Source : in out Map)
    is
-      NN : HT_Types.Nodes_Type renames Source.Nodes;
+      NN : HT_Types.Nodes_Type renames Source.Content.Nodes;
       X  : Count_Type;
       Y  : Count_Type;
 
@@ -704,17 +740,17 @@ is
 
       Clear (Target);
 
-      if Source.Length = 0 then
+      if Source.Content.Length = 0 then
          return;
       end if;
 
-      X := HT_Ops.First (Source);
+      X := HT_Ops.First (Source.Content);
       while X /= 0 loop
          Insert (Target, NN (X).Key, NN (X).Element);  -- optimize???
 
-         Y := HT_Ops.Next (Source, X);
+         Y := HT_Ops.Next (Source.Content, X);
 
-         HT_Ops.Delete_Node_Sans_Free (Source, X);
+         HT_Ops.Delete_Node_Sans_Free (Source.Content, X);
          Free (Source, X);
 
          X := Y;
@@ -743,7 +779,8 @@ is
       pragma Assert (Vet (Container, Position), "bad cursor in function Next");
 
       declare
-         Node : constant Count_Type := HT_Ops.Next (Container, Position.Node);
+         Node : constant Count_Type :=
+           HT_Ops.Next (Container.Content, Position.Node);
 
       begin
          if Node = 0 then
@@ -759,6 +796,40 @@ is
       Position := Next (Container, Position);
    end Next;
 
+   ---------------
+   -- Reference --
+   ---------------
+
+   function Reference
+     (Container : not null access Map;
+      Position  : Cursor) return not null access Element_Type
+   is
+   begin
+      if not Has_Element (Container.all, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      pragma Assert
+        (Vet (Container.all, Position), "bad cursor in function Reference");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Reference;
+
+   function Reference
+     (Container : not null access Map;
+      Key       : Key_Type) return not null access Element_Type
+   is
+      Node : constant Count_Type := Find (Container.all, Key).Node;
+
+   begin
+      if Node = 0 then
+         raise Constraint_Error with
+           "no element available because key not in map";
+      end if;
+
+      return Container.Content.Nodes (Node).Element'Access;
+   end Reference;
+
    -------------
    -- Replace --
    -------------
@@ -768,7 +839,7 @@ is
       Key       : Key_Type;
       New_Item  : Element_Type)
    is
-      Node : constant Count_Type := Key_Ops.Find (Container, Key);
+      Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
 
    begin
       if Node = 0 then
@@ -776,7 +847,7 @@ is
       end if;
 
       declare
-         N : Node_Type renames Container.Nodes (Node);
+         N : Node_Type renames Container.Content.Nodes (Node);
       begin
          N.Key := Key;
          N.Element := New_Item;
@@ -801,7 +872,7 @@ is
       pragma Assert
         (Vet (Container, Position), "bad cursor in Replace_Element");
 
-      Container.Nodes (Position.Node).Element := New_Item;
+      Container.Content.Nodes (Position.Node).Element := New_Item;
    end Replace_Element;
 
    ----------------------
@@ -841,7 +912,7 @@ is
          X : Count_Type;
 
       begin
-         if Container.Length = 0 then
+         if Container.Content.Length = 0 then
             return False;
          end if;
 
@@ -849,7 +920,7 @@ is
             return False;
          end if;
 
-         if Container.Buckets'Length = 0 then
+         if Container.Content.Buckets'Length = 0 then
             return False;
          end if;
 
@@ -857,15 +928,17 @@ is
             return False;
          end if;
 
-         if Container.Nodes (Position.Node).Next = Position.Node then
+         if Container.Content.Nodes (Position.Node).Next = Position.Node then
             return False;
          end if;
 
          X :=
-           Container.Buckets
-             (Key_Ops.Index (Container, Container.Nodes (Position.Node).Key));
+           Container.Content.Buckets
+             (Key_Ops.Index
+                (Container.Content,
+                 Container.Content.Nodes (Position.Node).Key));
 
-         for J in 1 .. Container.Length loop
+         for J in 1 .. Container.Content.Length loop
             if X = Position.Node then
                return True;
             end if;
@@ -874,14 +947,14 @@ is
                return False;
             end if;
 
-            if X = Container.Nodes (X).Next then
+            if X = Container.Content.Nodes (X).Next then
 
                --  Prevent unnecessary looping
 
                return False;
             end if;
 
-            X := Container.Nodes (X).Next;
+            X := Container.Content.Nodes (X).Next;
          end loop;
 
          return False;
diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
index e9b0268..2b49c13 100644
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -394,6 +394,95 @@ is
                 Model (Container)'Old,
                 Key (Container, Position));
 
+   function At_End
+     (E : not null access constant Map) return not null access constant Map
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Position  : Cursor) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Constant_Reference'Result.all =
+           Element (Model (Container), Key (Container, Position));
+
+   function Reference
+     (Container : not null access Map;
+      Position  : Cursor) return not null access Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container.all, Position),
+     Post   =>
+
+       --  Order of keys and cursors is preserved
+
+       Keys (At_End (Container).all) = Keys (Container.all)
+         and Positions (At_End (Container).all) = Positions (Container.all)
+
+         --  The value designated by the result of Reference is now associated
+         --  with the key at position Position in Container.
+
+         and Element (At_End (Container).all, Position) =
+               At_End (Reference'Result).all
+
+         --  Elements associated with other keys are preserved
+
+         and M.Same_Keys
+               (Model (At_End (Container).all),
+                Model (Container.all))
+         and M.Elements_Equal_Except
+               (Model (At_End (Container).all),
+                Model (Container.all),
+                Key (At_End (Container).all, Position));
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Key       : Key_Type) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Contains (Container, Key),
+     Post   =>
+       Constant_Reference'Result.all = Element (Model (Container), Key);
+
+   function Reference
+     (Container : not null access Map;
+      Key       : Key_Type) return not null access Element_Type
+   with
+     Global => null,
+     Pre    => Contains (Container.all, Key),
+     Post   =>
+
+       --  Order of keys and cursors is preserved
+
+       Keys (At_End (Container).all) = Keys (Container.all)
+         and Positions (At_End (Container).all) = Positions (Container.all)
+
+         --  The value designated by the result of Reference is now associated
+         --  with Key in Container.
+
+         and Element (Model (At_End (Container).all), Key) =
+               At_End (Reference'Result).all
+
+         --  Elements associated with other keys are preserved
+
+         and M.Same_Keys
+               (Model (At_End (Container).all),
+                Model (Container.all))
+         and M.Elements_Equal_Except
+               (Model (At_End (Container).all),
+                Model (Container.all),
+                Key);
+
    procedure Move (Target : in out Map; Source : in out Map) with
      Global => null,
      Pre    => Target.Capacity >= Length (Source),
@@ -804,7 +893,7 @@ private
 
    type Node_Type is record
       Key         : Key_Type;
-      Element     : Element_Type;
+      Element     : aliased Element_Type;
       Next        : Count_Type;
       Has_Element : Boolean := False;
    end record;
@@ -812,8 +901,9 @@ private
    package HT_Types is new
      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
-   type Map (Capacity : Count_Type; Modulus : Hash_Type) is
-     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+   type Map (Capacity : Count_Type; Modulus : Hash_Type) is record
+     Content : HT_Types.Hash_Table_Type (Capacity, Modulus);
+   end record;
 
    Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
 
diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb
index 3679ca4..cdb8a98 100644
--- a/gcc/ada/libgnat/a-cfhase.adb
+++ b/gcc/ada/libgnat/a-cfhase.adb
@@ -136,15 +136,16 @@ is
             ENode :=
               Find
                 (Container => Right,
-                 Item      => Left.Nodes (Node).Element).Node;
+                 Item      => Left.Content.Nodes (Node).Element).Node;
 
             if ENode = 0
-              or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+              or else Right.Content.Nodes (ENode).Element /=
+              Left.Content.Nodes (Node).Element
             then
                return False;
             end if;
 
-            Node := HT_Ops.Next (Left, Node);
+            Node := HT_Ops.Next (Left.Content, Node);
          end loop;
 
          return True;
@@ -166,7 +167,7 @@ is
       --------------------
 
       procedure Insert_Element (Source_Node : Count_Type) is
-         N : Node_Type renames Source.Nodes (Source_Node);
+         N : Node_Type renames Source.Content.Nodes (Source_Node);
          X : Count_Type;
          B : Boolean;
 
@@ -186,8 +187,8 @@ is
          raise Storage_Error with "not enough capacity";  -- SE or CE? ???
       end if;
 
-      HT_Ops.Clear (Target);
-      Insert_Elements (Source);
+      HT_Ops.Clear (Target.Content);
+      Insert_Elements (Source.Content);
    end Assign;
 
    --------------
@@ -196,7 +197,7 @@ is
 
    function Capacity (Container : Set) return Count_Type is
    begin
-      return Container.Nodes'Length;
+      return Container.Content.Nodes'Length;
    end Capacity;
 
    -----------
@@ -205,9 +206,28 @@ is
 
    procedure Clear (Container : in out Set) is
    begin
-      HT_Ops.Clear (Container);
+      HT_Ops.Clear (Container.Content);
    end Clear;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Set;
+      Position  : Cursor) return not null access constant Element_Type
+   is
+   begin
+      if not Has_Element (Container, Position) then
+         raise Constraint_Error with "Position cursor equals No_Element";
+      end if;
+
+      pragma Assert
+        (Vet (Container, Position), "bad cursor in function Element");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -237,18 +257,18 @@ is
          raise Capacity_Error;
       end if;
 
-      Target.Length := Source.Length;
-      Target.Free := Source.Free;
+      Target.Content.Length := Source.Content.Length;
+      Target.Content.Free := Source.Content.Free;
 
       H := 1;
       while H <= Source.Modulus loop
-         Target.Buckets (H) := Source.Buckets (H);
+         Target.Content.Buckets (H) := Source.Content.Buckets (H);
          H := H + 1;
       end loop;
 
       N := 1;
       while N <= Source.Capacity loop
-         Target.Nodes (N) := Source.Nodes (N);
+         Target.Content.Nodes (N) := Source.Content.Nodes (N);
          N := N + 1;
       end loop;
 
@@ -278,7 +298,7 @@ is
       X : Count_Type;
 
    begin
-      Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
+      Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X);
 
       if X = 0 then
          raise Constraint_Error with "attempt to delete element not in set";
@@ -295,7 +315,7 @@ is
 
       pragma Assert (Vet (Container, Position), "bad cursor in Delete");
 
-      HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
+      HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node);
       Free (Container, Position.Node);
 
       Position := No_Element;
@@ -311,8 +331,8 @@ is
       Src_Node   : Count_Type;
       Tgt_Node   : Count_Type;
 
-      TN : Nodes_Type renames Target.Nodes;
-      SN : Nodes_Type renames Source.Nodes;
+      TN : Nodes_Type renames Target.Content.Nodes;
+      SN : Nodes_Type renames Source.Content.Nodes;
 
    begin
       if Target'Address = Source'Address then
@@ -320,44 +340,45 @@ is
          return;
       end if;
 
-      Src_Length := Source.Length;
+      Src_Length := Source.Content.Length;
 
       if Src_Length = 0 then
          return;
       end if;
 
-      if Src_Length >= Target.Length then
-         Tgt_Node := HT_Ops.First (Target);
+      if Src_Length >= Target.Content.Length then
+         Tgt_Node := HT_Ops.First (Target.Content);
          while Tgt_Node /= 0 loop
-            if Element_Keys.Find (Source, TN (Tgt_Node).Element) /= 0 then
+            if Element_Keys.Find (Source.Content, TN (Tgt_Node).Element) /= 0
+            then
                declare
                   X : constant Count_Type := Tgt_Node;
                begin
-                  Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
-                  HT_Ops.Delete_Node_Sans_Free (Target, X);
+                  Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
+                  HT_Ops.Delete_Node_Sans_Free (Target.Content, X);
                   Free (Target, X);
                end;
 
             else
-               Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
+               Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
             end if;
          end loop;
 
          return;
       else
-         Src_Node := HT_Ops.First (Source);
+         Src_Node := HT_Ops.First (Source.Content);
          Src_Last := 0;
       end if;
 
       while Src_Node /= Src_Last loop
-         Tgt_Node := Element_Keys.Find (Target, SN (Src_Node).Element);
+         Tgt_Node := Element_Keys.Find (Target.Content, SN (Src_Node).Element);
 
          if Tgt_Node /= 0 then
-            HT_Ops.Delete_Node_Sans_Free (Target, Tgt_Node);
+            HT_Ops.Delete_Node_Sans_Free (Target.Content, Tgt_Node);
             Free (Target, Tgt_Node);
          end if;
 
-         Src_Node := HT_Ops.Next (Source, Src_Node);
+         Src_Node := HT_Ops.Next (Source.Content, Src_Node);
       end loop;
    end Difference;
 
@@ -373,7 +394,7 @@ is
 
       procedure Process (L_Node : Count_Type) is
          B : Boolean;
-         E : Element_Type renames Left.Nodes (L_Node).Element;
+         E : Element_Type renames Left.Content.Nodes (L_Node).Element;
          X : Count_Type;
 
       begin
@@ -386,7 +407,7 @@ is
    --  Start of processing for Difference
 
    begin
-      Iterate (Left);
+      Iterate (Left.Content);
    end Difference;
 
    function Difference (Left : Set; Right : Set) return Set is
@@ -403,7 +424,7 @@ is
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       C := Length (Left);
@@ -430,7 +451,7 @@ is
       pragma Assert
         (Vet (Container, Position), "bad cursor in function Element");
 
-      return Container.Nodes (Position.Node).Element;
+      return Container.Content.Nodes (Position.Node).Element;
    end Element;
 
    ---------------------
@@ -479,7 +500,7 @@ is
    --  Start of processing for Equivalent_Sets
 
    begin
-      return Is_Equivalent (Left, Right);
+      return Is_Equivalent (Left.Content, Right.Content);
    end Equivalent_Sets;
 
    ---------------------
@@ -501,7 +522,7 @@ is
    procedure Exclude (Container : in out Set; Item : Element_Type) is
       X : Count_Type;
    begin
-      Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
+      Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X);
       Free (Container, X);
    end Exclude;
 
@@ -513,7 +534,8 @@ 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.Content, Item);
 
    begin
       if Node = 0 then
@@ -528,7 +550,7 @@ is
    -----------
 
    function First (Container : Set) return Cursor is
-      Node : constant Count_Type := HT_Ops.First (Container);
+      Node : constant Count_Type := HT_Ops.First (Container.Content);
 
    begin
       if Node = 0 then
@@ -632,7 +654,7 @@ is
       --------------
 
       function Elements (Container : Set) return E.Sequence is
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : E.Sequence;
 
       begin
@@ -640,8 +662,8 @@ is
          --  for their postconditions.
 
          while Position /= 0 loop
-            R := E.Add (R, Container.Nodes (Position).Element);
-            Position := HT_Ops.Next (Container, Position);
+            R := E.Add (R, Container.Content.Nodes (Position).Element);
+            Position := HT_Ops.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -710,7 +732,7 @@ is
       -----------
 
       function Model (Container : Set) return M.Set is
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : M.Set;
 
       begin
@@ -721,9 +743,9 @@ is
             R :=
               M.Add
                 (Container => R,
-                 Item      => Container.Nodes (Position).Element);
+                 Item      => Container.Content.Nodes (Position).Element);
 
-            Position := HT_Ops.Next (Container, Position);
+            Position := HT_Ops.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -735,7 +757,7 @@ is
 
       function Positions (Container : Set) return P.Map is
          I        : Count_Type := 1;
-         Position : Count_Type := HT_Ops.First (Container);
+         Position : Count_Type := HT_Ops.First (Container.Content);
          R        : P.Map;
 
       begin
@@ -745,7 +767,7 @@ is
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
             pragma Assert (P.Length (R) = I);
-            Position := HT_Ops.Next (Container, Position);
+            Position := HT_Ops.Next (Container.Content, Position);
             I := I + 1;
          end loop;
 
@@ -762,8 +784,8 @@ is
    begin
       if X /= 0 then
          pragma Assert (X <= HT.Capacity);
-         HT.Nodes (X).Has_Element := False;
-         HT_Ops.Free (HT, X);
+         HT.Content.Nodes (X).Has_Element := False;
+         HT_Ops.Free (HT.Content, X);
       end if;
    end Free;
 
@@ -774,8 +796,8 @@ is
    procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
       procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
    begin
-      Allocate (HT, Node);
-      HT.Nodes (Node).Has_Element := True;
+      Allocate (HT.Content, Node);
+      HT.Content.Nodes (Node).Has_Element := True;
    end Generic_Allocate;
 
    package body Generic_Keys with SPARK_Mode => Off is
@@ -821,7 +843,7 @@ is
          X : Count_Type;
 
       begin
-         Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+         Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X);
 
          if X = 0 then
             raise Constraint_Error with "attempt to delete key not in set";
@@ -845,7 +867,7 @@ is
             raise Constraint_Error with "key not in map";
          end if;
 
-         return Container.Nodes (Node).Element;
+         return Container.Content.Nodes (Node).Element;
       end Element;
 
       -------------------------
@@ -867,7 +889,7 @@ is
       procedure Exclude (Container : in out Set; Key : Key_Type) is
          X : Count_Type;
       begin
-         Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+         Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X);
          Free (Container, X);
       end Exclude;
 
@@ -879,7 +901,7 @@ 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.Content, Key);
       begin
          return (if Node = 0 then No_Element else (Node => Node));
       end Find;
@@ -927,7 +949,7 @@ is
            (Vet (Container, Position), "bad cursor in function Key");
 
          declare
-            N  : Node_Type renames Container.Nodes (Position.Node);
+            N  : Node_Type renames Container.Content.Nodes (Position.Node);
          begin
             return Key (N.Element);
          end;
@@ -942,14 +964,14 @@ is
          Key       : Key_Type;
          New_Item  : Element_Type)
       is
-         Node : constant Count_Type := Key_Keys.Find (Container, Key);
+         Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
 
       begin
          if Node = 0 then
             raise Constraint_Error with "attempt to replace key not in set";
          end if;
 
-         Replace_Element (Container, Node, New_Item);
+         Replace_Element (Container.Content, Node, New_Item);
       end Replace;
 
    end Generic_Keys;
@@ -961,7 +983,7 @@ is
    function Has_Element (Container : Set; Position : Cursor) return Boolean is
    begin
       if Position.Node = 0
-        or else not Container.Nodes (Position.Node).Has_Element
+        or else not Container.Content.Nodes (Position.Node).Has_Element
       then
          return False;
       end if;
@@ -990,7 +1012,7 @@ is
       Insert (Container, New_Item, Position, Inserted);
 
       if not Inserted then
-         Container.Nodes (Position.Node).Element := New_Item;
+         Container.Content.Nodes (Position.Node).Element := New_Item;
       end if;
    end Include;
 
@@ -1062,7 +1084,7 @@ is
    --  Start of processing for Insert
 
    begin
-      Local_Insert (Container, New_Item, Node, Inserted);
+      Local_Insert (Container.Content, New_Item, Node, Inserted);
    end Insert;
 
    ------------------
@@ -1071,29 +1093,29 @@ is
 
    procedure Intersection (Target : in out Set; Source : Set) is
       Tgt_Node : Count_Type;
-      TN       : Nodes_Type renames Target.Nodes;
+      TN       : Nodes_Type renames Target.Content.Nodes;
 
    begin
       if Target'Address = Source'Address then
          return;
       end if;
 
-      if Source.Length = 0 then
+      if Source.Content.Length = 0 then
          Clear (Target);
          return;
       end if;
 
-      Tgt_Node := HT_Ops.First (Target);
+      Tgt_Node := HT_Ops.First (Target.Content);
       while Tgt_Node /= 0 loop
          if Find (Source, TN (Tgt_Node).Element).Node /= 0 then
-            Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
+            Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
 
          else
             declare
                X : constant Count_Type := Tgt_Node;
             begin
-               Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
-               HT_Ops.Delete_Node_Sans_Free (Target, X);
+               Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
+               HT_Ops.Delete_Node_Sans_Free (Target.Content, X);
                Free (Target, X);
             end;
          end if;
@@ -1111,7 +1133,7 @@ is
       -------------
 
       procedure Process (L_Node : Count_Type) is
-         E : Element_Type renames Left.Nodes (L_Node).Element;
+         E : Element_Type renames Left.Content.Nodes (L_Node).Element;
          X : Count_Type;
          B : Boolean;
 
@@ -1125,7 +1147,7 @@ is
    --  Start of processing for Intersection
 
    begin
-      Iterate (Left);
+      Iterate (Left.Content);
    end Intersection;
 
    function Intersection (Left : Set; Right : Set) return Set is
@@ -1134,7 +1156,7 @@ is
 
    begin
       if Left'Address = Right'Address then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       C := Count_Type'Min (Length (Left), Length (Right));  -- ???
@@ -1162,7 +1184,7 @@ 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.Content, Key.Element) /= 0;
    end Is_In;
 
    ---------------
@@ -1171,7 +1193,7 @@ is
 
    function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
       Subset_Node  : Count_Type;
-      Subset_Nodes : Nodes_Type renames Subset.Nodes;
+      Subset_Nodes : Nodes_Type renames Subset.Content.Nodes;
 
    begin
       if Subset'Address = Of_Set'Address then
@@ -1194,7 +1216,7 @@ is
             end if;
          end;
 
-         Subset_Node := HT_Ops.Next (Subset, Subset_Node);
+         Subset_Node := HT_Ops.Next (Subset.Content, Subset_Node);
       end loop;
 
       return True;
@@ -1206,7 +1228,7 @@ is
 
    function Length (Container : Set) return Count_Type is
    begin
-      return Container.Length;
+      return Container.Content.Length;
    end Length;
 
    ----------
@@ -1216,7 +1238,7 @@ is
    --  Comments???
 
    procedure Move (Target : in out Set; Source : in out Set) is
-      NN   : HT_Types.Nodes_Type renames Source.Nodes;
+      NN   : HT_Types.Nodes_Type renames Source.Content.Nodes;
       X, Y : Count_Type;
 
    begin
@@ -1231,17 +1253,17 @@ is
 
       Clear (Target);
 
-      if Source.Length = 0 then
+      if Source.Content.Length = 0 then
          return;
       end if;
 
-      X := HT_Ops.First (Source);
+      X := HT_Ops.First (Source.Content);
       while X /= 0 loop
          Insert (Target, NN (X).Element);  -- optimize???
 
-         Y := HT_Ops.Next (Source, X);
+         Y := HT_Ops.Next (Source.Content, X);
 
-         HT_Ops.Delete_Node_Sans_Free (Source, X);
+         HT_Ops.Delete_Node_Sans_Free (Source.Content, X);
          Free (Source, X);
 
          X := Y;
@@ -1269,7 +1291,7 @@ is
 
       pragma Assert (Vet (Container, Position), "bad cursor in Next");
 
-      return (Node => HT_Ops.Next (Container, Position.Node));
+      return (Node => HT_Ops.Next (Container.Content, Position.Node));
    end Next;
 
    procedure Next (Container : Set; Position : in out Cursor) is
@@ -1283,7 +1305,7 @@ is
 
    function Overlap (Left, Right : Set) return Boolean is
       Left_Node  : Count_Type;
-      Left_Nodes : Nodes_Type renames Left.Nodes;
+      Left_Nodes : Nodes_Type renames Left.Content.Nodes;
 
    begin
       if Length (Right) = 0 or Length (Left) = 0 then
@@ -1305,7 +1327,7 @@ is
             end if;
          end;
 
-         Left_Node := HT_Ops.Next (Left, Left_Node);
+         Left_Node := HT_Ops.Next (Left.Content, Left_Node);
       end loop;
 
       return False;
@@ -1316,14 +1338,15 @@ is
    -------------
 
    procedure Replace (Container : in out Set; New_Item : Element_Type) is
-      Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
+      Node : constant Count_Type :=
+        Element_Keys.Find (Container.Content, New_Item);
 
    begin
       if Node = 0 then
          raise Constraint_Error with "attempt to replace element not in set";
       end if;
 
-      Container.Nodes (Node).Element := New_Item;
+      Container.Content.Nodes (Node).Element := New_Item;
    end Replace;
 
    ---------------------
@@ -1343,7 +1366,7 @@ is
       pragma Assert
         (Vet (Container, Position), "bad cursor in Replace_Element");
 
-      Replace_Element (Container, Position.Node, New_Item);
+      Replace_Element (Container.Content, Position.Node, New_Item);
    end Replace_Element;
 
    ----------------------
@@ -1394,7 +1417,7 @@ is
 
       procedure Process (Source_Node : Count_Type) is
          B : Boolean;
-         N : Node_Type renames Source.Nodes (Source_Node);
+         N : Node_Type renames Source.Content.Nodes (Source_Node);
          X : Count_Type;
 
       begin
@@ -1419,7 +1442,7 @@ is
          return;
       end if;
 
-      Iterate (Source);
+      Iterate (Source.Content);
    end Symmetric_Difference;
 
    function Symmetric_Difference (Left : Set; Right : Set) return Set is
@@ -1432,11 +1455,11 @@ is
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       if Length (Left) = 0 then
-         return Right.Copy;
+         return Copy (Right);
       end if;
 
       C := Length (Left) + Length (Right);
@@ -1478,7 +1501,7 @@ is
       -------------
 
       procedure Process (Src_Node : Count_Type) is
-         N : Node_Type renames Source.Nodes (Src_Node);
+         N : Node_Type renames Source.Content.Nodes (Src_Node);
          E : Element_Type renames N.Element;
 
          X : Count_Type;
@@ -1495,7 +1518,7 @@ is
          return;
       end if;
 
-      Iterate (Source);
+      Iterate (Source.Content);
    end Union;
 
    function Union (Left : Set; Right : Set) return Set is
@@ -1504,15 +1527,15 @@ is
 
    begin
       if Left'Address = Right'Address then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       if Length (Left) = 0 then
-         return Right.Copy;
+         return Copy (Right);
       end if;
 
       C := Length (Left) + Length (Right);
@@ -1535,11 +1558,11 @@ is
 
       declare
          S : Set renames Container;
-         N : Nodes_Type renames S.Nodes;
+         N : Nodes_Type renames S.Content.Nodes;
          X : Count_Type;
 
       begin
-         if S.Length = 0 then
+         if S.Content.Length = 0 then
             return False;
          end if;
 
@@ -1551,9 +1574,10 @@ is
             return False;
          end if;
 
-         X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element));
+         X := S.Content.Buckets
+           (Element_Keys.Index (S.Content, N (Position.Node).Element));
 
-         for J in 1 .. S.Length loop
+         for J in 1 .. S.Content.Length loop
             if X = Position.Node then
                return True;
             end if;
diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
index 5d57863..9bcd8ce 100644
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -515,6 +515,16 @@ is
                  Position => Position)
           and Positions (Container) = Positions (Container)'Old;
 
+   function Constant_Reference
+     (Container : aliased Set;
+      Position  : Cursor) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Constant_Reference'Result.all =
+         E.Get (Elements (Container), P.Get (Positions (Container), Position));
+
    procedure Move (Target : in out Set; Source : in out Set) with
      Global => null,
      Pre    => Target.Capacity >= Length (Source),
@@ -1462,7 +1472,7 @@ private
 
    type Node_Type is
       record
-         Element     : Element_Type;
+         Element     : aliased Element_Type;
          Next        : Count_Type;
          Has_Element : Boolean := False;
       end record;
@@ -1470,8 +1480,9 @@ private
    package HT_Types is new
      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
-   type Set (Capacity : Count_Type; Modulus : Hash_Type) is
-     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+   type Set (Capacity : Count_Type; Modulus : Hash_Type) is record
+     Content : HT_Types.Hash_Table_Type (Capacity, Modulus);
+   end record;
 
    use HT_Types;
 
diff --git a/gcc/ada/libgnat/a-cfinve.adb b/gcc/ada/libgnat/a-cfinve.adb
index 6ab4935..d0c7e82 100644
--- a/gcc/ada/libgnat/a-cfinve.adb
+++ b/gcc/ada/libgnat/a-cfinve.adb
@@ -184,6 +184,28 @@ is
       Free (Container.Elements_Ptr);
    end Clear;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Vector;
+      Index     : Index_Type) return not null access constant Element_Type
+   is
+   begin
+      if Index > Container.Last then
+         raise Constraint_Error with "Index is out of range";
+      end if;
+
+      declare
+         II : constant Int'Base := Int (Index) - Int (No_Index);
+         I  : constant Capacity_Range := Capacity_Range (II);
+
+      begin
+         return Constant_Reference (Elemsc (Container) (I));
+      end;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -1180,6 +1202,32 @@ is
       Insert (Container, Index_Type'First, New_Item, Count);
    end Prepend;
 
+   ---------------
+   -- Reference --
+   ---------------
+
+   function Reference
+     (Container : not null access Vector;
+      Index     : Index_Type) return not null access Element_Type
+   is
+   begin
+      if Index > Container.Last then
+         raise Constraint_Error with "Index is out of range";
+      end if;
+
+      declare
+         II : constant Int'Base := Int (Index) - Int (No_Index);
+         I  : constant Capacity_Range := Capacity_Range (II);
+
+      begin
+         if Container.Elements_Ptr = null then
+            return Reference (Container.Elements (I)'Access);
+         else
+            return Reference (Container.Elements_Ptr (I)'Access);
+         end if;
+      end;
+   end Reference;
+
    ---------------------
    -- Replace_Element --
    ---------------------
diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
index 37dde92..9b95437 100644
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -311,6 +311,48 @@ is
                 Right    => Model (Container),
                 Position => Index);
 
+   function At_End (E : access constant Vector) return access constant Vector
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased Vector;
+      Index     : Index_Type) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Index in First_Index (Container) .. Last_Index (Container),
+     Post   =>
+         Constant_Reference'Result.all = Element (Model (Container), Index);
+
+   function Reference
+     (Container : not null access Vector;
+      Index     : Index_Type) return not null access Element_Type
+   with
+     Global => null,
+     Pre    =>
+      Index in First_Index (Container.all) .. Last_Index (Container.all),
+     Post   =>
+      Length (Container.all) = Length (At_End (Container).all)
+
+         --  Container will have Result.all at index Index
+
+         and At_End (Reference'Result).all =
+           Element (Model (At_End (Container).all), Index)
+
+         --  All other elements are preserved
+
+         and M.Equal_Except
+               (Left     => Model (Container.all),
+                Right    => Model (At_End (Container).all),
+                Position => Index);
+
    procedure Insert
      (Container : in out Vector;
       Before    : Extended_Index;
@@ -909,7 +951,7 @@ private
    use Holders;
 
    subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
-   type Elements_Array is array (Array_Index range <>) of Holder;
+   type Elements_Array is array (Array_Index range <>) of aliased Holder;
    function "=" (L, R : Elements_Array) return Boolean is abstract;
 
    type Elements_Array_Ptr is access all Elements_Array;
diff --git a/gcc/ada/libgnat/a-cforma.adb b/gcc/ada/libgnat/a-cforma.adb
index f384619..45f9be7 100644
--- a/gcc/ada/libgnat/a-cforma.adb
+++ b/gcc/ada/libgnat/a-cforma.adb
@@ -133,19 +133,20 @@ is
          return True;
       end if;
 
-      Lst := Next (Left, Last (Left).Node);
+      Lst := Next (Left.Content, Last (Left).Node);
 
       Node := First (Left).Node;
       while Node /= Lst loop
-         ENode := Find (Right, Left.Nodes (Node).Key).Node;
+         ENode := Find (Right, Left.Content.Nodes (Node).Key).Node;
 
          if ENode = 0 or else
-           Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
+           Left.Content.Nodes (Node).Element /=
+           Right.Content.Nodes (ENode).Element
          then
             return False;
          end if;
 
-         Node := Next (Left, Node);
+         Node := Next (Left.Content, Node);
       end loop;
 
       return True;
@@ -166,7 +167,7 @@ is
       --------------------
 
       procedure Append_Element (Source_Node : Count_Type) is
-         SN : Node_Type renames Source.Nodes (Source_Node);
+         SN : Node_Type renames Source.Content.Nodes (Source_Node);
 
          procedure Set_Element (Node : in out Node_Type);
          pragma Inline (Set_Element);
@@ -193,7 +194,7 @@ is
          function New_Node return Count_Type is
             Result : Count_Type;
          begin
-            Allocate (Target, Result);
+            Allocate (Target.Content, Result);
             return Result;
          end New_Node;
 
@@ -213,7 +214,7 @@ is
 
       begin
          Unconditional_Insert_Avec_Hint
-           (Tree  => Target,
+           (Tree  => Target.Content,
             Hint  => 0,
             Key   => SN.Key,
             Node  => Target_Node);
@@ -230,8 +231,8 @@ is
          raise Storage_Error with "not enough capacity";  -- SE or CE? ???
       end if;
 
-      Tree_Operations.Clear_Tree (Target);
-      Append_Elements (Source);
+      Tree_Operations.Clear_Tree (Target.Content);
+      Append_Elements (Source.Content);
    end Assign;
 
    -------------
@@ -239,7 +240,7 @@ is
    -------------
 
    function Ceiling (Container : Map; Key : Key_Type) return Cursor is
-      Node : constant Count_Type := Key_Ops.Ceiling (Container, Key);
+      Node : constant Count_Type := Key_Ops.Ceiling (Container.Content, Key);
 
    begin
       if Node = 0 then
@@ -255,7 +256,7 @@ is
 
    procedure Clear (Container : in out Map) is
    begin
-      Tree_Operations.Clear_Tree (Container);
+      Tree_Operations.Clear_Tree (Container.Content);
    end Clear;
 
    -----------
@@ -267,6 +268,40 @@ is
       return Node.Color;
    end Color;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Position  : Cursor) return not null access constant Element_Type
+   is
+   begin
+      if not Has_Element (Container, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      pragma Assert (Vet (Container.Content, Position.Node),
+                     "bad cursor in function Constant_Reference");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Constant_Reference;
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Key       : Key_Type) return not null access constant Element_Type
+   is
+      Node : constant Node_Access := Find (Container, Key).Node;
+
+   begin
+      if Node = 0 then
+         raise Constraint_Error with
+           "no element available because key not in map";
+      end if;
+
+      return Container.Content.Nodes (Node).Element'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -291,33 +326,33 @@ is
 
       return Target : Map (Count_Type'Max (Source.Capacity, Capacity)) do
          if Length (Source) > 0 then
-            Target.Length := Source.Length;
-            Target.Root := Source.Root;
-            Target.First := Source.First;
-            Target.Last := Source.Last;
-            Target.Free := Source.Free;
+            Target.Content.Length := Source.Content.Length;
+            Target.Content.Root := Source.Content.Root;
+            Target.Content.First := Source.Content.First;
+            Target.Content.Last := Source.Content.Last;
+            Target.Content.Free := Source.Content.Free;
 
             while Node <= Source.Capacity loop
-               Target.Nodes (Node).Element :=
-                 Source.Nodes (Node).Element;
-               Target.Nodes (Node).Key :=
-                 Source.Nodes (Node).Key;
-               Target.Nodes (Node).Parent :=
-                 Source.Nodes (Node).Parent;
-               Target.Nodes (Node).Left :=
-                 Source.Nodes (Node).Left;
-               Target.Nodes (Node).Right :=
-                 Source.Nodes (Node).Right;
-               Target.Nodes (Node).Color :=
-                 Source.Nodes (Node).Color;
-               Target.Nodes (Node).Has_Element :=
-                 Source.Nodes (Node).Has_Element;
+               Target.Content.Nodes (Node).Element :=
+                 Source.Content.Nodes (Node).Element;
+               Target.Content.Nodes (Node).Key :=
+                 Source.Content.Nodes (Node).Key;
+               Target.Content.Nodes (Node).Parent :=
+                 Source.Content.Nodes (Node).Parent;
+               Target.Content.Nodes (Node).Left :=
+                 Source.Content.Nodes (Node).Left;
+               Target.Content.Nodes (Node).Right :=
+                 Source.Content.Nodes (Node).Right;
+               Target.Content.Nodes (Node).Color :=
+                 Source.Content.Nodes (Node).Color;
+               Target.Content.Nodes (Node).Has_Element :=
+                 Source.Content.Nodes (Node).Has_Element;
                Node := Node + 1;
             end loop;
 
             while Node <= Target.Capacity loop
                N := Node;
-               Formal_Ordered_Maps.Free (Tree => Target, X => N);
+               Free (Tree => Target, X => N);
                Node := Node + 1;
             end loop;
          end if;
@@ -335,25 +370,25 @@ is
            "Position cursor of Delete has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "Position cursor of Delete is bad");
 
-      Tree_Operations.Delete_Node_Sans_Free (Container,
+      Tree_Operations.Delete_Node_Sans_Free (Container.Content,
                                              Position.Node);
-      Formal_Ordered_Maps.Free (Container, Position.Node);
+      Free (Container, Position.Node);
       Position := No_Element;
    end Delete;
 
    procedure Delete (Container : in out Map; Key : Key_Type) is
-      X : constant Node_Access := Key_Ops.Find (Container, Key);
+      X : constant Node_Access := Key_Ops.Find (Container.Content, Key);
 
    begin
       if X = 0 then
          raise Constraint_Error with "key not in map";
       end if;
 
-      Tree_Operations.Delete_Node_Sans_Free (Container, X);
-      Formal_Ordered_Maps.Free (Container, X);
+      Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+      Free (Container, X);
    end Delete;
 
    ------------------
@@ -364,8 +399,8 @@ is
       X : constant Node_Access := First (Container).Node;
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Maps.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Delete_First;
 
@@ -377,8 +412,8 @@ is
       X : constant Node_Access := Last (Container).Node;
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Maps.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Delete_Last;
 
@@ -393,10 +428,10 @@ is
            "Position cursor of function Element has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "Position cursor of function Element is bad");
 
-      return Container.Nodes (Position.Node).Element;
+      return Container.Content.Nodes (Position.Node).Element;
 
    end Element;
 
@@ -408,7 +443,7 @@ is
          raise Constraint_Error with "key not in map";
       end if;
 
-      return Container.Nodes (Node).Element;
+      return Container.Content.Nodes (Node).Element;
    end Element;
 
    ---------------------
@@ -431,11 +466,11 @@ is
    -------------
 
    procedure Exclude (Container : in out Map; Key : Key_Type) is
-      X : constant Node_Access := Key_Ops.Find (Container, Key);
+      X : constant Node_Access := Key_Ops.Find (Container.Content, Key);
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Maps.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Exclude;
 
@@ -444,7 +479,7 @@ 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.Content, Key);
 
    begin
       if Node = 0 then
@@ -464,7 +499,7 @@ is
          return No_Element;
       end if;
 
-      return (Node => Container.First);
+      return (Node => Container.Content.First);
    end First;
 
    -------------------
@@ -477,7 +512,7 @@ is
          raise Constraint_Error with "map is empty";
       end if;
 
-      return Container.Nodes (First (Container).Node).Element;
+      return Container.Content.Nodes (First (Container).Node).Element;
    end First_Element;
 
    ---------------
@@ -490,7 +525,7 @@ is
          raise Constraint_Error with "map is empty";
       end if;
 
-      return Container.Nodes (First (Container).Node).Key;
+      return Container.Content.Nodes (First (Container).Node).Key;
    end First_Key;
 
    -----------
@@ -498,7 +533,7 @@ is
    -----------
 
    function Floor (Container : Map; Key : Key_Type) return Cursor is
-      Node : constant Count_Type := Key_Ops.Floor (Container, Key);
+      Node : constant Count_Type := Key_Ops.Floor (Container.Content, Key);
 
    begin
       if Node = 0 then
@@ -602,7 +637,7 @@ is
       ----------
 
       function Keys (Container : Map) return K.Sequence is
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : K.Sequence;
 
       begin
@@ -610,8 +645,8 @@ is
          --  for their postconditions.
 
          while Position /= 0 loop
-            R := K.Add (R, Container.Nodes (Position).Key);
-            Position := Tree_Operations.Next (Container, Position);
+            R := K.Add (R, Container.Content.Nodes (Position).Key);
+            Position := Tree_Operations.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -628,7 +663,7 @@ is
       -----------
 
       function Model (Container : Map) return M.Map is
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : M.Map;
 
       begin
@@ -639,10 +674,10 @@ is
             R :=
               M.Add
                 (Container => R,
-                 New_Key   => Container.Nodes (Position).Key,
-                 New_Item  => Container.Nodes (Position).Element);
+                 New_Key   => Container.Content.Nodes (Position).Key,
+                 New_Item  => Container.Content.Nodes (Position).Element);
 
-            Position := Tree_Operations.Next (Container, Position);
+            Position := Tree_Operations.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -701,7 +736,7 @@ is
 
       function Positions (Container : Map) return P.Map is
          I        : Count_Type := 1;
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : P.Map;
 
       begin
@@ -711,7 +746,7 @@ is
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
             pragma Assert (P.Length (R) = I);
-            Position := Tree_Operations.Next (Container, Position);
+            Position := Tree_Operations.Next (Container.Content, Position);
             I := I + 1;
          end loop;
 
@@ -729,8 +764,8 @@ is
       X  : Count_Type)
    is
    begin
-      Tree.Nodes (X).Has_Element := False;
-      Tree_Operations.Free (Tree, X);
+      Tree.Content.Nodes (X).Has_Element := False;
+      Tree_Operations.Free (Tree.Content, X);
    end Free;
 
    ----------------------
@@ -758,7 +793,7 @@ is
          return False;
       end if;
 
-      return Container.Nodes (Position.Node).Has_Element;
+      return Container.Content.Nodes (Position.Node).Has_Element;
    end Has_Element;
 
    -------------
@@ -778,7 +813,7 @@ is
 
       if not Inserted then
          declare
-            N : Node_Type renames Container.Nodes (Position.Node);
+            N : Node_Type renames Container.Content.Nodes (Position.Node);
          begin
             N.Key := Key;
             N.Element := New_Item;
@@ -819,7 +854,7 @@ is
          X : Node_Access;
 
       begin
-         Allocate_Node (Container, X);
+         Allocate_Node (Container.Content, X);
          return X;
       end New_Node;
 
@@ -827,7 +862,7 @@ is
 
    begin
       Insert_Sans_Hint
-        (Container,
+        (Container.Content,
          Key,
          Position.Node,
          Inserted);
@@ -895,10 +930,10 @@ is
            "Position cursor of function Key has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "Position cursor of function Key is bad");
 
-      return Container.Nodes (Position.Node).Key;
+      return Container.Content.Nodes (Position.Node).Key;
    end Key;
 
    ----------
@@ -911,7 +946,7 @@ is
          return No_Element;
       end if;
 
-      return (Node => Container.Last);
+      return (Node => Container.Content.Last);
    end Last;
 
    ------------------
@@ -924,7 +959,7 @@ is
          raise Constraint_Error with "map is empty";
       end if;
 
-      return Container.Nodes (Last (Container).Node).Element;
+      return Container.Content.Nodes (Last (Container).Node).Element;
    end Last_Element;
 
    --------------
@@ -937,7 +972,7 @@ is
          raise Constraint_Error with "map is empty";
       end if;
 
-      return Container.Nodes (Last (Container).Node).Key;
+      return Container.Content.Nodes (Last (Container).Node).Key;
    end Last_Key;
 
    --------------
@@ -955,7 +990,7 @@ is
 
    function Length (Container : Map) return Count_Type is
    begin
-      return Container.Length;
+      return Container.Content.Length;
    end Length;
 
    ----------
@@ -963,7 +998,7 @@ is
    ----------
 
    procedure Move (Target : in out Map; Source : in out Map) is
-      NN : Tree_Types.Nodes_Type renames Source.Nodes;
+      NN : Tree_Types.Nodes_Type renames Source.Content.Nodes;
       X  : Node_Access;
 
    begin
@@ -989,7 +1024,7 @@ is
 
          Insert (Target, NN (X).Key, NN (X).Element);  -- optimize???
 
-         Tree_Operations.Delete_Node_Sans_Free (Source, X);
+         Tree_Operations.Delete_Node_Sans_Free (Source.Content, X);
          Formal_Ordered_Maps.Free (Source, X);
       end loop;
    end Move;
@@ -1013,10 +1048,10 @@ is
          raise Constraint_Error;
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Next");
 
-      return (Node => Tree_Operations.Next (Container, Position.Node));
+      return (Node => Tree_Operations.Next (Container.Content, Position.Node));
    end Next;
 
    ------------
@@ -1047,12 +1082,12 @@ is
          raise Constraint_Error;
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Previous");
 
       declare
          Node : constant Count_Type :=
-           Tree_Operations.Previous (Container, Position.Node);
+           Tree_Operations.Previous (Container.Content, Position.Node);
 
       begin
          if Node = 0 then
@@ -1063,6 +1098,41 @@ is
       end;
    end Previous;
 
+   --------------
+   -- Reference --
+   --------------
+
+   function Reference
+     (Container : not null access Map;
+      Position  : Cursor) return not null access Element_Type
+   is
+   begin
+      if not Has_Element (Container.all, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      pragma Assert
+        (Vet (Container.Content, Position.Node),
+         "bad cursor in function Reference");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Reference;
+
+   function Reference
+     (Container : not null access Map;
+      Key       : Key_Type) return not null access Element_Type
+   is
+      Node : constant Count_Type := Find (Container.all, Key).Node;
+
+   begin
+      if Node = 0 then
+         raise Constraint_Error with
+           "no element available because key not in map";
+      end if;
+
+      return Container.Content.Nodes (Node).Element'Access;
+   end Reference;
+
    -------------
    -- Replace --
    -------------
@@ -1074,7 +1144,7 @@ is
    is
    begin
       declare
-         Node : constant Node_Access := Key_Ops.Find (Container, Key);
+         Node : constant Node_Access := Key_Ops.Find (Container.Content, Key);
 
       begin
          if Node = 0 then
@@ -1082,7 +1152,7 @@ is
          end if;
 
          declare
-            N : Node_Type renames Container.Nodes (Node);
+            N : Node_Type renames Container.Content.Nodes (Node);
          begin
             N.Key := Key;
             N.Element := New_Item;
@@ -1105,10 +1175,10 @@ is
            "Position cursor of Replace_Element has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "Position cursor of Replace_Element is bad");
 
-      Container.Nodes (Position.Node).Element := New_Item;
+      Container.Content.Nodes (Position.Node).Element := New_Item;
    end Replace_Element;
 
    ---------------
diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
index d32727e..a1cad03 100644
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -400,6 +400,95 @@ is
                 Model (Container)'Old,
                 Key (Container, Position));
 
+   function At_End
+     (E : not null access constant Map) return not null access constant Map
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Position  : Cursor) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Constant_Reference'Result.all =
+           Element (Model (Container), Key (Container, Position));
+
+   function Reference
+     (Container : not null access Map;
+      Position  : Cursor) return not null access Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container.all, Position),
+     Post   =>
+
+       --  Order of keys and cursors is preserved
+
+       Keys (At_End (Container).all) = Keys (Container.all)
+         and Positions (At_End (Container).all) = Positions (Container.all)
+
+         --  The value designated by the result of Reference is now associated
+         --  with the key at position Position in Container.
+
+         and Element (At_End (Container).all, Position) =
+               At_End (Reference'Result).all
+
+         --  Elements associated with other keys are preserved
+
+         and M.Same_Keys
+               (Model (At_End (Container).all),
+                Model (Container.all))
+         and M.Elements_Equal_Except
+               (Model (At_End (Container).all),
+                Model (Container.all),
+                Key (At_End (Container).all, Position));
+
+   function Constant_Reference
+     (Container : aliased Map;
+      Key       : Key_Type) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Contains (Container, Key),
+     Post   =>
+       Constant_Reference'Result.all = Element (Model (Container), Key);
+
+   function Reference
+     (Container : not null access Map;
+      Key       : Key_Type) return not null access Element_Type
+   with
+     Global => null,
+     Pre    => Contains (Container.all, Key),
+     Post   =>
+
+       --  Order of keys and cursors is preserved
+
+       Keys (At_End (Container).all) = Keys (Container.all)
+         and Positions (At_End (Container).all) = Positions (Container.all)
+
+         --  The value designated by the result of Reference is now associated
+         --  with Key in Container.
+
+         and Element (Model (At_End (Container).all), Key) =
+               At_End (Reference'Result).all
+
+         --  Elements associated with other keys are preserved
+
+         and M.Same_Keys
+               (Model (At_End (Container).all),
+                Model (Container.all))
+         and M.Elements_Equal_Except
+               (Model (At_End (Container).all),
+                Model (Container.all),
+                Key);
+
    procedure Move (Target : in out Map; Source : in out Map) with
      Global => null,
      Pre    => Target.Capacity >= Length (Source),
@@ -1045,14 +1134,15 @@ private
       Right   : Node_Access := 0;
       Color   : Red_Black_Trees.Color_Type := Red;
       Key     : Key_Type;
-      Element : Element_Type;
+      Element : aliased Element_Type;
    end record;
 
    package Tree_Types is
      new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
 
-   type Map (Capacity : Count_Type) is
-     new Tree_Types.Tree_Type (Capacity) with null record;
+   type Map (Capacity : Count_Type) is record
+     Content : Tree_Types.Tree_Type (Capacity);
+   end record;
 
    Empty_Map : constant Map := (Capacity => 0, others => <>);
 
diff --git a/gcc/ada/libgnat/a-cforse.adb b/gcc/ada/libgnat/a-cforse.adb
index e5525b9..7c45e4f 100644
--- a/gcc/ada/libgnat/a-cforse.adb
+++ b/gcc/ada/libgnat/a-cforse.adb
@@ -81,6 +81,10 @@ is
 
    --  Comments needed???
 
+   procedure Assign
+     (Target : in out Tree_Types.Tree_Type;
+      Source : Tree_Types.Tree_Type);
+
    generic
       with procedure Set_Element (Node : in out Node_Type);
    procedure Generic_Allocate
@@ -90,13 +94,13 @@ is
    procedure Free (Tree : in out Set; X : Count_Type);
 
    procedure Insert_Sans_Hint
-     (Container : in out Set;
+     (Container : in out Tree_Types.Tree_Type;
       New_Item  : Element_Type;
       Node      : out Count_Type;
       Inserted  : out Boolean);
 
    procedure Insert_With_Hint
-     (Dst_Set  : in out Set;
+     (Dst_Set  : in out Tree_Types.Tree_Type;
       Dst_Hint : Count_Type;
       Src_Node : Node_Type;
       Dst_Node : out Count_Type);
@@ -141,7 +145,7 @@ is
    package Set_Ops is
      new Red_Black_Trees.Generic_Bounded_Set_Operations
        (Tree_Operations  => Tree_Operations,
-        Set_Type         => Set,
+        Set_Type         => Tree_Types.Tree_Type,
         Assign           => Assign,
         Insert_With_Hint => Insert_With_Hint,
         Is_Less          => Is_Less_Node_Node);
@@ -164,18 +168,19 @@ is
          return True;
       end if;
 
-      Lst := Next (Left, Last (Left).Node);
+      Lst := Next (Left.Content, Last (Left).Node);
 
       Node := First (Left).Node;
       while Node /= Lst loop
-         ENode := Find (Right, Left.Nodes (Node).Element).Node;
+         ENode := Find (Right, Left.Content.Nodes (Node).Element).Node;
          if ENode = 0
-           or else Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
+           or else Left.Content.Nodes (Node).Element /=
+           Right.Content.Nodes (ENode).Element
          then
             return False;
          end if;
 
-         Node := Next (Left, Node);
+         Node := Next (Left.Content, Node);
       end loop;
 
       return True;
@@ -185,7 +190,10 @@ is
    -- Assign --
    ------------
 
-   procedure Assign (Target : in out Set; Source : Set) is
+   procedure Assign
+     (Target : in out Tree_Types.Tree_Type;
+      Source : Tree_Types.Tree_Type)
+   is
       procedure Append_Element (Source_Node : Count_Type);
 
       procedure Append_Elements is
@@ -267,12 +275,18 @@ is
       Append_Elements (Source);
    end Assign;
 
+   procedure Assign (Target : in out Set; Source : Set) is
+   begin
+      Assign (Target.Content, Source.Content);
+   end Assign;
+
    -------------
    -- Ceiling --
    -------------
 
    function Ceiling (Container : Set; Item : Element_Type) return Cursor is
-      Node : constant Count_Type := Element_Keys.Ceiling (Container, Item);
+      Node : constant Count_Type :=
+        Element_Keys.Ceiling (Container.Content, Item);
 
    begin
       if Node = 0 then
@@ -288,7 +302,7 @@ is
 
    procedure Clear (Container : in out Set) is
    begin
-      Tree_Operations.Clear_Tree (Container);
+      Tree_Operations.Clear_Tree (Container.Content);
    end Clear;
 
    -----------
@@ -300,6 +314,25 @@ is
       return Node.Color;
    end Color;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Set;
+      Position  : Cursor) return not null access constant Element_Type
+   is
+   begin
+      if not Has_Element (Container, Position) then
+         raise Constraint_Error with "Position cursor has no element";
+      end if;
+
+      pragma Assert (Vet (Container.Content, Position.Node),
+                     "bad cursor in Element");
+
+      return Container.Content.Nodes (Position.Node).Element'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -327,32 +360,32 @@ is
       end if;
 
       if Length (Source) > 0 then
-         Target.Length := Source.Length;
-         Target.Root   := Source.Root;
-         Target.First  := Source.First;
-         Target.Last   := Source.Last;
-         Target.Free   := Source.Free;
+         Target.Content.Length := Source.Content.Length;
+         Target.Content.Root   := Source.Content.Root;
+         Target.Content.First  := Source.Content.First;
+         Target.Content.Last   := Source.Content.Last;
+         Target.Content.Free   := Source.Content.Free;
 
          Node := 1;
          while Node <= Source.Capacity loop
-            Target.Nodes (Node).Element :=
-              Source.Nodes (Node).Element;
-            Target.Nodes (Node).Parent :=
-              Source.Nodes (Node).Parent;
-            Target.Nodes (Node).Left :=
-              Source.Nodes (Node).Left;
-            Target.Nodes (Node).Right :=
-              Source.Nodes (Node).Right;
-            Target.Nodes (Node).Color :=
-              Source.Nodes (Node).Color;
-            Target.Nodes (Node).Has_Element :=
-              Source.Nodes (Node).Has_Element;
+            Target.Content.Nodes (Node).Element :=
+              Source.Content.Nodes (Node).Element;
+            Target.Content.Nodes (Node).Parent :=
+              Source.Content.Nodes (Node).Parent;
+            Target.Content.Nodes (Node).Left :=
+              Source.Content.Nodes (Node).Left;
+            Target.Content.Nodes (Node).Right :=
+              Source.Content.Nodes (Node).Right;
+            Target.Content.Nodes (Node).Color :=
+              Source.Content.Nodes (Node).Color;
+            Target.Content.Nodes (Node).Has_Element :=
+              Source.Content.Nodes (Node).Has_Element;
             Node := Node + 1;
          end loop;
 
          while Node <= Target.Capacity loop
             N := Node;
-            Formal_Ordered_Sets.Free (Tree => Target, X => N);
+            Free (Tree => Target, X => N);
             Node := Node + 1;
          end loop;
       end if;
@@ -370,25 +403,25 @@ is
          raise Constraint_Error with "Position cursor has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Delete");
 
-      Tree_Operations.Delete_Node_Sans_Free (Container,
+      Tree_Operations.Delete_Node_Sans_Free (Container.Content,
                                              Position.Node);
-      Formal_Ordered_Sets.Free (Container, Position.Node);
+      Free (Container, Position.Node);
       Position := No_Element;
    end Delete;
 
    procedure Delete (Container : in out Set; Item : Element_Type) is
-      X : constant Count_Type := Element_Keys.Find (Container, Item);
+      X : constant Count_Type := Element_Keys.Find (Container.Content, Item);
 
    begin
       if X = 0 then
          raise Constraint_Error with "attempt to delete element not in set";
       end if;
 
-      Tree_Operations.Delete_Node_Sans_Free (Container, X);
-      Formal_Ordered_Sets.Free (Container, X);
+      Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+      Free (Container, X);
    end Delete;
 
    ------------------
@@ -396,11 +429,11 @@ is
    ------------------
 
    procedure Delete_First (Container : in out Set) is
-      X    : constant Count_Type := Container.First;
+      X    : constant Count_Type := Container.Content.First;
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Sets.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Delete_First;
 
@@ -409,11 +442,11 @@ is
    -----------------
 
    procedure Delete_Last (Container : in out Set) is
-      X    : constant Count_Type := Container.Last;
+      X    : constant Count_Type := Container.Content.Last;
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Sets.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Delete_Last;
 
@@ -423,7 +456,7 @@ is
 
    procedure Difference (Target : in out Set; Source : Set) is
    begin
-      Set_Ops.Set_Difference (Target, Source);
+      Set_Ops.Set_Difference (Target.Content, Source.Content);
    end Difference;
 
    function Difference (Left, Right : Set) return Set is
@@ -437,11 +470,12 @@ is
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       return S : Set (Length (Left)) do
-            Assign (S, Set_Ops.Set_Difference (Left, Right));
+         Assign
+           (S.Content, Set_Ops.Set_Difference (Left.Content, Right.Content));
       end return;
    end Difference;
 
@@ -455,10 +489,10 @@ is
          raise Constraint_Error with "Position cursor has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Element");
 
-      return Container.Nodes (Position.Node).Element;
+      return Container.Content.Nodes (Position.Node).Element;
    end Element;
 
    -------------------------
@@ -506,7 +540,7 @@ is
    --  Start of processing for Equivalent_Sets
 
    begin
-      return Is_Equivalent (Left, Right);
+      return Is_Equivalent (Left.Content, Right.Content);
    end Equivalent_Sets;
 
    -------------
@@ -514,11 +548,11 @@ is
    -------------
 
    procedure Exclude (Container : in out Set; Item : Element_Type) is
-      X : constant Count_Type := Element_Keys.Find (Container, Item);
+      X : constant Count_Type := Element_Keys.Find (Container.Content, Item);
    begin
       if X /= 0 then
-         Tree_Operations.Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Sets.Free (Container, X);
+         Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end if;
    end Exclude;
 
@@ -527,7 +561,8 @@ is
    ----------
 
    function Find (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.Content, Item);
 
    begin
       if Node = 0 then
@@ -547,7 +582,7 @@ is
          return No_Element;
       end if;
 
-      return (Node => Container.First);
+      return (Node => Container.Content.First);
    end First;
 
    -------------------
@@ -562,7 +597,7 @@ is
       end if;
 
       declare
-         N : Tree_Types.Nodes_Type renames Container.Nodes;
+         N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
       begin
          return N (Fst).Element;
       end;
@@ -575,7 +610,8 @@ is
    function Floor (Container : Set; Item : Element_Type) return Cursor is
    begin
       declare
-         Node : constant Count_Type := Element_Keys.Floor (Container, Item);
+         Node : constant Count_Type :=
+           Element_Keys.Floor (Container.Content, Item);
 
       begin
          if Node = 0 then
@@ -748,7 +784,7 @@ is
       --------------
 
       function Elements (Container : Set) return E.Sequence is
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : E.Sequence;
 
       begin
@@ -756,8 +792,8 @@ is
          --  for their postconditions.
 
          while Position /= 0 loop
-            R := E.Add (R, Container.Nodes (Position).Element);
-            Position := Tree_Operations.Next (Container, Position);
+            R := E.Add (R, Container.Content.Nodes (Position).Element);
+            Position := Tree_Operations.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -873,7 +909,7 @@ is
       -----------
 
       function Model (Container : Set) return M.Set is
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : M.Set;
 
       begin
@@ -884,9 +920,9 @@ is
             R :=
               M.Add
                 (Container => R,
-                 Item      => Container.Nodes (Position).Element);
+                 Item      => Container.Content.Nodes (Position).Element);
 
-            Position := Tree_Operations.Next (Container, Position);
+            Position := Tree_Operations.Next (Container.Content, Position);
          end loop;
 
          return R;
@@ -898,7 +934,7 @@ is
 
       function Positions (Container : Set) return P.Map is
          I        : Count_Type := 1;
-         Position : Count_Type := Container.First;
+         Position : Count_Type := Container.Content.First;
          R        : P.Map;
 
       begin
@@ -908,7 +944,7 @@ is
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
             pragma Assert (P.Length (R) = I);
-            Position := Tree_Operations.Next (Container, Position);
+            Position := Tree_Operations.Next (Container.Content, Position);
             I := I + 1;
          end loop;
 
@@ -923,8 +959,8 @@ is
 
    procedure Free (Tree : in out Set; X : Count_Type) is
    begin
-      Tree.Nodes (X).Has_Element := False;
-      Tree_Operations.Free (Tree, X);
+      Tree.Content.Nodes (X).Has_Element := False;
+      Tree_Operations.Free (Tree.Content, X);
    end Free;
 
    ----------------------
@@ -978,7 +1014,8 @@ is
       -------------
 
       function Ceiling (Container : Set; Key : Key_Type) return Cursor is
-         Node : constant Count_Type := Key_Keys.Ceiling (Container, Key);
+         Node : constant Count_Type :=
+           Key_Keys.Ceiling (Container.Content, Key);
 
       begin
          if Node = 0 then
@@ -1002,15 +1039,15 @@ is
       ------------
 
       procedure Delete (Container : in out Set; Key : Key_Type) is
-         X : constant Count_Type := Key_Keys.Find (Container, Key);
+         X : constant Count_Type := Key_Keys.Find (Container.Content, Key);
 
       begin
          if X = 0 then
             raise Constraint_Error with "attempt to delete key not in set";
          end if;
 
-         Delete_Node_Sans_Free (Container, X);
-         Formal_Ordered_Sets.Free (Container, X);
+         Delete_Node_Sans_Free (Container.Content, X);
+         Free (Container, X);
       end Delete;
 
       -------------
@@ -1018,7 +1055,7 @@ is
       -------------
 
       function Element (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.Content, Key);
 
       begin
          if Node = 0 then
@@ -1026,7 +1063,7 @@ is
          end if;
 
          declare
-            N : Tree_Types.Nodes_Type renames Container.Nodes;
+            N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
          begin
             return N (Node).Element;
          end;
@@ -1052,11 +1089,11 @@ is
       -------------
 
       procedure Exclude (Container : in out Set; Key : Key_Type) is
-         X : constant Count_Type := Key_Keys.Find (Container, Key);
+         X : constant Count_Type := Key_Keys.Find (Container.Content, Key);
       begin
          if X /= 0 then
-            Delete_Node_Sans_Free (Container, X);
-            Formal_Ordered_Sets.Free (Container, X);
+            Delete_Node_Sans_Free (Container.Content, X);
+            Free (Container, X);
          end if;
       end Exclude;
 
@@ -1065,7 +1102,7 @@ is
       ----------
 
       function Find (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.Content, Key);
       begin
          return (if Node = 0 then No_Element else (Node => Node));
       end Find;
@@ -1075,7 +1112,7 @@ is
       -----------
 
       function Floor (Container : Set; Key : Key_Type) return Cursor is
-         Node : constant Count_Type := Key_Keys.Floor (Container, Key);
+         Node : constant Count_Type := Key_Keys.Floor (Container.Content, Key);
       begin
          return (if Node = 0 then No_Element else (Node => Node));
       end Floor;
@@ -1225,11 +1262,11 @@ is
               "Position cursor has no element";
          end if;
 
-         pragma Assert (Vet (Container, Position.Node),
+         pragma Assert (Vet (Container.Content, Position.Node),
                         "bad cursor in Key");
 
          declare
-            N : Tree_Types.Nodes_Type renames Container.Nodes;
+            N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
          begin
             return Key (N (Position.Node).Element);
          end;
@@ -1244,7 +1281,7 @@ is
          Key       : Key_Type;
          New_Item  : Element_Type)
       is
-         Node : constant Count_Type := Key_Keys.Find (Container, Key);
+         Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
       begin
          if not Has_Element (Container, (Node => Node)) then
             raise Constraint_Error with
@@ -1265,7 +1302,7 @@ is
       if Position.Node = 0 then
          return False;
       else
-         return Container.Nodes (Position.Node).Has_Element;
+         return Container.Content.Nodes (Position.Node).Has_Element;
       end if;
    end Has_Element;
 
@@ -1282,7 +1319,7 @@ is
 
       if not Inserted then
          declare
-            N : Tree_Types.Nodes_Type renames Container.Nodes;
+            N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
          begin
             N (Position.Node).Element := New_Item;
          end;
@@ -1300,7 +1337,7 @@ is
       Inserted  : out Boolean)
    is
    begin
-      Insert_Sans_Hint (Container, New_Item, Position.Node, Inserted);
+      Insert_Sans_Hint (Container.Content, New_Item, Position.Node, Inserted);
    end Insert;
 
    procedure Insert
@@ -1324,7 +1361,7 @@ is
    ----------------------
 
    procedure Insert_Sans_Hint
-     (Container : in out Set;
+     (Container : in out Tree_Types.Tree_Type;
       New_Item  : Element_Type;
       Node      : out Count_Type;
       Inserted  : out Boolean)
@@ -1377,7 +1414,7 @@ is
    ----------------------
 
    procedure Insert_With_Hint
-     (Dst_Set  : in out Set;
+     (Dst_Set  : in out Tree_Types.Tree_Type;
       Dst_Hint : Count_Type;
       Src_Node : Node_Type;
       Dst_Node : out Count_Type)
@@ -1439,17 +1476,18 @@ is
 
    procedure Intersection (Target : in out Set; Source : Set) is
    begin
-      Set_Ops.Set_Intersection (Target, Source);
+      Set_Ops.Set_Intersection (Target.Content, Source.Content);
    end Intersection;
 
    function Intersection (Left, Right : Set) return Set is
    begin
       if Left'Address = Right'Address then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       return S : Set (Count_Type'Min (Length (Left), Length (Right))) do
-            Assign (S, Set_Ops.Set_Intersection (Left, Right));
+            Assign (S.Content,
+                    Set_Ops.Set_Intersection (Left.Content, Right.Content));
       end return;
    end Intersection;
 
@@ -1503,7 +1541,7 @@ is
 
    function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
    begin
-      return Set_Ops.Set_Subset (Subset, Of_Set => Of_Set);
+      return Set_Ops.Set_Subset (Subset.Content, Of_Set => Of_Set.Content);
    end Is_Subset;
 
    ----------
@@ -1514,7 +1552,7 @@ is
    begin
       return (if Length (Container) = 0
               then No_Element
-              else (Node => Container.Last));
+              else (Node => Container.Content.Last));
    end Last;
 
    ------------------
@@ -1528,7 +1566,7 @@ is
       end if;
 
       declare
-         N : Tree_Types.Nodes_Type renames Container.Nodes;
+         N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
       begin
          return N (Last (Container).Node).Element;
       end;
@@ -1549,7 +1587,7 @@ is
 
    function Length (Container : Set) return Count_Type is
    begin
-      return Container.Length;
+      return Container.Content.Length;
    end Length;
 
    ----------
@@ -1557,7 +1595,7 @@ is
    ----------
 
    procedure Move (Target : in out Set; Source : in out Set) is
-      N : Tree_Types.Nodes_Type renames Source.Nodes;
+      N : Tree_Types.Nodes_Type renames Source.Content.Nodes;
       X : Count_Type;
 
    begin
@@ -1573,13 +1611,13 @@ is
       Clear (Target);
 
       loop
-         X := Source.First;
+         X := Source.Content.First;
          exit when X = 0;
 
          Insert (Target, N (X).Element);  -- optimize???
 
-         Tree_Operations.Delete_Node_Sans_Free (Source, X);
-         Formal_Ordered_Sets.Free (Source, X);
+         Tree_Operations.Delete_Node_Sans_Free (Source.Content, X);
+         Free (Source, X);
       end loop;
    end Move;
 
@@ -1597,9 +1635,9 @@ is
          raise Constraint_Error;
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Next");
-      return (Node => Tree_Operations.Next (Container, Position.Node));
+      return (Node => Tree_Operations.Next (Container.Content, Position.Node));
    end Next;
 
    procedure Next (Container : Set; Position : in out Cursor) is
@@ -1613,7 +1651,7 @@ is
 
    function Overlap (Left, Right : Set) return Boolean is
    begin
-      return Set_Ops.Set_Overlap (Left, Right);
+      return Set_Ops.Set_Overlap (Left.Content, Right.Content);
    end Overlap;
 
    ------------
@@ -1639,12 +1677,12 @@ is
          raise Constraint_Error;
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Previous");
 
       declare
          Node : constant Count_Type :=
-           Tree_Operations.Previous (Container, Position.Node);
+           Tree_Operations.Previous (Container.Content, Position.Node);
       begin
          return (if Node = 0 then No_Element else (Node => Node));
       end;
@@ -1660,7 +1698,8 @@ is
    -------------
 
    procedure Replace (Container : in out Set; New_Item : Element_Type) is
-      Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
+      Node : constant Count_Type :=
+        Element_Keys.Find (Container.Content, New_Item);
 
    begin
       if Node = 0 then
@@ -1668,7 +1707,7 @@ is
            "attempt to replace element not in set";
       end if;
 
-      Container.Nodes (Node).Element := New_Item;
+      Container.Content.Nodes (Node).Element := New_Item;
    end Replace;
 
    ---------------------
@@ -1696,7 +1735,7 @@ is
           (Local_Insert_Post,
            Local_Insert_Sans_Hint);
 
-      NN : Tree_Types.Nodes_Type renames Tree.Nodes;
+      NN : Tree_Types.Nodes_Type renames Tree.Content.Nodes;
 
       --------------
       -- New_Node --
@@ -1730,7 +1769,7 @@ is
          return;
       end if;
 
-      Hint := Element_Keys.Ceiling (Tree, Item);
+      Hint := Element_Keys.Ceiling (Tree.Content, Item);
 
       if Hint = 0 then
          null;
@@ -1746,10 +1785,10 @@ is
          raise Program_Error with "attempt to replace existing element";
       end if;
 
-      Tree_Operations.Delete_Node_Sans_Free (Tree, Node);
+      Tree_Operations.Delete_Node_Sans_Free (Tree.Content, Node);
 
       Local_Insert_With_Hint
-        (Tree     => Tree,
+        (Tree     => Tree.Content,
          Position => Hint,
          Key      => Item,
          Node     => Result,
@@ -1770,7 +1809,7 @@ is
            "Position cursor has no element";
       end if;
 
-      pragma Assert (Vet (Container, Position.Node),
+      pragma Assert (Vet (Container.Content, Position.Node),
                      "bad cursor in Replace_Element");
 
       Replace_Element (Container, Position.Node, New_Item);
@@ -1830,7 +1869,7 @@ is
 
    procedure Symmetric_Difference (Target : in out Set; Source : Set) is
    begin
-      Set_Ops.Set_Symmetric_Difference (Target, Source);
+      Set_Ops.Set_Symmetric_Difference (Target.Content, Source.Content);
    end Symmetric_Difference;
 
    function Symmetric_Difference (Left, Right : Set) return Set is
@@ -1840,15 +1879,17 @@ is
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       if Length (Left) = 0 then
-         return Right.Copy;
+         return Copy (Right);
       end if;
 
       return S : Set (Length (Left) + Length (Right)) do
-         Assign (S, Set_Ops.Set_Symmetric_Difference (Left, Right));
+         Assign
+           (S.Content,
+            Set_Ops.Set_Symmetric_Difference (Left.Content, Right.Content));
       end return;
    end Symmetric_Difference;
 
@@ -1861,7 +1902,7 @@ is
       Inserted : Boolean;
    begin
       return S : Set (Capacity => 1) do
-         Insert_Sans_Hint (S, New_Item, Node, Inserted);
+         Insert_Sans_Hint (S.Content, New_Item, Node, Inserted);
          pragma Assert (Inserted);
       end return;
    end To_Set;
@@ -1872,21 +1913,21 @@ is
 
    procedure Union (Target : in out Set; Source : Set) is
    begin
-      Set_Ops.Set_Union (Target, Source);
+      Set_Ops.Set_Union (Target.Content, Source.Content);
    end Union;
 
    function Union (Left, Right : Set) return Set is
    begin
       if Left'Address = Right'Address then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       if Length (Left) = 0 then
-         return Right.Copy;
+         return Copy (Right);
       end if;
 
       if Length (Right) = 0 then
-         return Left.Copy;
+         return Copy (Left);
       end if;
 
       return S : Set (Length (Left) + Length (Right)) do
diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index 12d2d3c..e1d7c91 100644
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -529,6 +529,16 @@ is
                  Position => Position)
           and Positions (Container) = Positions (Container)'Old;
 
+   function Constant_Reference
+     (Container : aliased Set;
+      Position  : Cursor) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Constant_Reference'Result.all =
+         E.Get (Elements (Container), P.Get (Positions (Container), Position));
+
    procedure Move (Target : in out Set; Source : in out Set) with
      Global => null,
      Pre    => Target.Capacity >= Length (Source),
@@ -1770,18 +1780,19 @@ private
 
    type Node_Type is record
       Has_Element : Boolean := False;
-      Parent  : Count_Type := 0;
-      Left    : Count_Type := 0;
-      Right   : Count_Type := 0;
-      Color   : Red_Black_Trees.Color_Type;
-      Element : Element_Type;
+      Parent      : Count_Type := 0;
+      Left        : Count_Type := 0;
+      Right       : Count_Type := 0;
+      Color       : Red_Black_Trees.Color_Type;
+      Element     : aliased Element_Type;
    end record;
 
    package Tree_Types is
      new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
 
-   type Set (Capacity : Count_Type) is
-     new Tree_Types.Tree_Type (Capacity) with null record;
+   type Set (Capacity : Count_Type) is record
+     Content : Tree_Types.Tree_Type (Capacity);
+   end record;
 
    use Red_Black_Trees;
 
diff --git a/gcc/ada/libgnat/a-coboho.adb b/gcc/ada/libgnat/a-coboho.adb
index 32346d0..21b9f54 100644
--- a/gcc/ada/libgnat/a-coboho.adb
+++ b/gcc/ada/libgnat/a-coboho.adb
@@ -65,6 +65,26 @@ package body Ada.Containers.Bounded_Holders is
       return Get (Left) = Get (Right);
    end "=";
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Holder) return not null access constant Element_Type
+   is
+   begin
+      return Cast (Container'Address);
+   end Constant_Reference;
+
+   ---------
+   -- Get --
+   ---------
+
+   function Get (Container : Holder) return Element_Type is
+   begin
+      return Cast (Container'Address).all;
+   end Get;
+
    ---------------
    -- Put_Image --
    ---------------
@@ -79,14 +99,16 @@ package body Ada.Containers.Bounded_Holders is
       Array_After (S);
    end Put_Image;
 
-   ---------
-   -- Get --
-   ---------
+   ---------------
+   -- Reference --
+   ---------------
 
-   function Get (Container : Holder) return Element_Type is
+   function Reference
+     (Container : not null access Holder) return not null access Element_Type
+   is
    begin
-      return Cast (Container'Address).all;
-   end Get;
+      return Cast (Container.all'Address);
+   end Reference;
 
    ---------
    -- Set --
diff --git a/gcc/ada/libgnat/a-coboho.ads b/gcc/ada/libgnat/a-coboho.ads
index 9dd73ba..086f194 100644
--- a/gcc/ada/libgnat/a-coboho.ads
+++ b/gcc/ada/libgnat/a-coboho.ads
@@ -81,6 +81,12 @@ package Ada.Containers.Bounded_Holders is
 
    procedure Set (Container : in out Holder; New_Item  : Element_Type);
 
+   function Constant_Reference
+     (Container : aliased Holder) return not null access constant Element_Type;
+
+   function Reference
+     (Container : not null access Holder) return not null access Element_Type;
+
 private
 
    --  The implementation uses low-level tricks (Address clauses and unchecked
diff --git a/gcc/ada/libgnat/a-cofove.adb b/gcc/ada/libgnat/a-cofove.adb
index a1f13ed..c7f4f06 100644
--- a/gcc/ada/libgnat/a-cofove.adb
+++ b/gcc/ada/libgnat/a-cofove.adb
@@ -142,6 +142,22 @@ is
       Container.Last := No_Index;
    end Clear;
 
+   ------------------------
+   -- Constant_Reference --
+   ------------------------
+
+   function Constant_Reference
+     (Container : aliased Vector;
+      Index     : Index_Type) return not null access constant Element_Type
+   is
+   begin
+      if Index > Container.Last then
+         raise Constraint_Error with "Index is out of range";
+      end if;
+
+      return Container.Elements (To_Array_Index (Index))'Access;
+   end Constant_Reference;
+
    --------------
    -- Contains --
    --------------
@@ -1096,6 +1112,22 @@ is
       end;
    end Replace_Element;
 
+   ---------------
+   -- Reference --
+   ---------------
+
+   function Reference
+     (Container : not null access Vector;
+      Index     : Index_Type) return not null access Element_Type
+   is
+   begin
+      if Index > Container.Last then
+         raise Constraint_Error with "Index is out of range";
+      end if;
+
+      return Container.Elements (To_Array_Index (Index))'Access;
+   end Reference;
+
    ----------------------
    -- Reserve_Capacity --
    ----------------------
diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
index 61115dd..a4ed7e5 100644
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -290,6 +290,48 @@ is
                 Right    => Model (Container),
                 Position => Index);
 
+   function At_End (E : access constant Vector) return access constant Vector
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased Vector;
+      Index     : Index_Type) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Index in First_Index (Container) .. Last_Index (Container),
+     Post   =>
+         Constant_Reference'Result.all = Element (Model (Container), Index);
+
+   function Reference
+     (Container : not null access Vector;
+      Index     : Index_Type) return not null access Element_Type
+   with
+     Global => null,
+     Pre    =>
+      Index in First_Index (Container.all) .. Last_Index (Container.all),
+     Post   =>
+      Length (Container.all) = Length (At_End (Container).all)
+
+         --  Container will have Result.all at index Index
+
+         and At_End (Reference'Result).all =
+           Element (Model (At_End (Container).all), Index)
+
+         --  All other elements are preserved
+
+         and M.Equal_Except
+               (Left     => Model (Container.all),
+                Right    => Model (At_End (Container).all),
+                Position => Index);
+
    procedure Insert
      (Container : in out Vector;
       Before    : Extended_Index;
@@ -905,7 +947,7 @@ private
    pragma Inline (Contains);
 
    subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
-   type Elements_Array is array (Array_Index range <>) of Element_Type;
+   type Elements_Array is array (Array_Index range <>) of aliased Element_Type;
    function "=" (L, R : Elements_Array) return Boolean is abstract;
 
    type Vector (Capacity : Capacity_Range) is record
diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index ca872e2..a1dd764 100644
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -302,6 +302,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
      Global => null,
      Pre    => Has_Witness (Container, Witness);
 
+   function Copy_Key (Key : Key_Type) return Key_Type is (Key);
+   function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+   --  Elements and Keys of maps are copied by numerous primitives in this
+   --  package. This function causes GNATprove to verify that such a copy is
+   --  valid (in particular, it does not break the ownership policy of SPARK,
+   --  i.e. it does not contain pointers that could be used to alias mutable
+   --  data).
+
    ---------------------------
    --  Iteration Primitives --
    ---------------------------
diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads
index d852be9..d0acba7 100644
--- a/gcc/ada/libgnat/a-cofuse.ads
+++ b/gcc/ada/libgnat/a-cofuse.ads
@@ -249,6 +249,13 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
            and Right <= Union'Result
            and Included_In_Union (Union'Result, Left, Right);
 
+   function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+   --  Elements of containers are copied by numerous primitives in this
+   --  package. This function causes GNATprove to verify that such a copy is
+   --  valid (in particular, it does not break the ownership policy of SPARK,
+   --  i.e. it does not contain pointers that could be used to alias mutable
+   --  data).
+
    ---------------------------
    --  Iteration Primitives --
    ---------------------------
diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index bdd0e94..ee52730 100644
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -336,6 +336,13 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
                      Lst    => Last (Remove'Result),
                      Offset => 1);
 
+   function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+   --  Elements of containers are copied by numerous primitives in this
+   --  package. This function causes GNATprove to verify that such a copy is
+   --  valid (in particular, it does not break the ownership policy of SPARK,
+   --  i.e. it does not contain pointers that could be used to alias mutable
+   --  data).
+
    ---------------------------
    --  Iteration Primitives --
    ---------------------------