[multiple changes]

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb Add new type Visited_Element
	and update the contents of table Elab_Visited.	Various code clean up.
	(Check_Elab_Call): Determine whether a prior call to
	the same subprogram was already examined within the same context.
	(Check_Internal_Call_Continue): Register the subprogram being
	called as examined within a particular context. Do not suppress
	elaboration warnings.

2017-04-27  Gary Dismukes  <dismukes@adacore.com>

	* xoscons.adb, osint.ads: Minor reformatting.

2017-04-27  Bob Duff  <duff@adacore.com>

	* g-dyntab.ads, g-dyntab.adb: Misc cleanup. Rename
	Table_Count_Type --> Table_Last_Type, because the name
	was confusing (a "count" usually starts at zero).  Add
	functionality supported or needed by other tables packages
	(Move, Release_Threshold).
	* g-table.ads, g-table.adb: This is now just a thin wrapper
	around g-dyntab.ads/g-dyntab.adb.  Add functionality supported
	or needed by other tables packages (Save, Restore).
	* table.ads, table.adb: This is now just a thin wrapper around
	* g-table.ads/g-table.adb.
	* namet.h, scos.h, uintp.h: These files are reaching into the
	private data of some instances of g-table, whose names changed,
	so the above change requires some adjustment here. It now uses
	public interfaces.

2017-04-27  Bob Duff  <duff@adacore.com>

	* namet.adb, namet.ads: Minor: remove unused procedures.

2017-04-27  Eric Botcazou  <ebotcazou@adacore.com>

	* checks.adb (Apply_Scalar_Range_Check): Initialize Ok variable too.
	(Minimize_Eliminate_Overflows): Initialize Llo and Lhi.
	Add pragma Warnings on Rtype variable in nested block.	*
	* exp_ch3.adb (Build_Init_Statements): Initialize VAR_LOC.
	* exp_ch4.adb (Expand_Concatenate): Initialize 3 variables.
	(Size_In_Storage_Elements): Add pragma Warnings on Res variable.
	* exp_ch7.adb (Build_Adjust_Statements): Initialize Bod_Stmts.
	(Process_Component_List_For_Finalize): Initialize Counter_Id.
	(Build_Finalize_Statements): Initialize Bod_Stmts.
	* exp_disp.adb (Expand_Dispatching_Call): Initialize SCIL_Node.

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cfhama.adb, a-cfhamai.ads (=): Generic parameter removed to
	allow the use of regular equality over elements in contracts.
	(Formal_Model): Ghost package containing model functions that are
	used in subprogram contracts.
	(Current_To_Last): Removed, model
	functions should be used instead.
	(First_To_Previous): Removed, model functions should be used instead.
	(Strict_Equal): Removed, model functions should be used instead.
	(No_Overlap): Removed, model functions should be used instead.
	(Equivalent_Keys): Functions over cursors are removed. They were
	awkward with explicit container parameters.
	* a-cofuma.adb, a-cofuma.ads (Lift_Equivalent_Keys): New lemma
	(proof only) procedure to help GNATprove when equivalence over
	keys is not equality.

From-SVN: r247320

24 files changed, 1241 insertions, 1459 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d8863a2..d68ec0e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,70 @@
 2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* sem_elab.adb Add new type Visited_Element
+	and update the contents of table Elab_Visited.	Various code clean up.
+	(Check_Elab_Call): Determine whether a prior call to
+	the same subprogram was already examined within the same context.
+	(Check_Internal_Call_Continue): Register the subprogram being
+	called as examined within a particular context. Do not suppress
+	elaboration warnings.
+
+2017-04-27  Gary Dismukes  <dismukes@adacore.com>
+
+	* xoscons.adb, osint.ads: Minor reformatting.
+
+2017-04-27  Bob Duff  <duff@adacore.com>
+
+	* g-dyntab.ads, g-dyntab.adb: Misc cleanup. Rename
+	Table_Count_Type --> Table_Last_Type, because the name
+	was confusing (a "count" usually starts at zero).  Add
+	functionality supported or needed by other tables packages
+	(Move, Release_Threshold).
+	* g-table.ads, g-table.adb: This is now just a thin wrapper
+	around g-dyntab.ads/g-dyntab.adb.  Add functionality supported
+	or needed by other tables packages (Save, Restore).
+	* table.ads, table.adb: This is now just a thin wrapper around
+	* g-table.ads/g-table.adb.
+	* namet.h, scos.h, uintp.h: These files are reaching into the
+	private data of some instances of g-table, whose names changed,
+	so the above change requires some adjustment here. It now uses
+	public interfaces.
+
+2017-04-27  Bob Duff  <duff@adacore.com>
+
+	* namet.adb, namet.ads: Minor: remove unused procedures.
+
+2017-04-27  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* checks.adb (Apply_Scalar_Range_Check): Initialize Ok variable too.
+	(Minimize_Eliminate_Overflows): Initialize Llo and Lhi.
+	Add pragma Warnings on Rtype variable in nested block.	*
+	* exp_ch3.adb (Build_Init_Statements): Initialize VAR_LOC.
+	* exp_ch4.adb (Expand_Concatenate): Initialize 3 variables.
+	(Size_In_Storage_Elements): Add pragma Warnings on Res variable.
+	* exp_ch7.adb (Build_Adjust_Statements): Initialize Bod_Stmts.
+	(Process_Component_List_For_Finalize): Initialize Counter_Id.
+	(Build_Finalize_Statements): Initialize Bod_Stmts.
+	* exp_disp.adb (Expand_Dispatching_Call): Initialize SCIL_Node.
+
+2017-04-27  Claire Dross  <dross@adacore.com>
+
+	* a-cfhama.adb, a-cfhamai.ads (=): Generic parameter removed to
+	allow the use of regular equality over elements in contracts.
+	(Formal_Model): Ghost package containing model functions that are
+	used in subprogram contracts.
+	(Current_To_Last): Removed, model
+	functions should be used instead.
+	(First_To_Previous): Removed, model functions should be used instead.
+	(Strict_Equal): Removed, model functions should be used instead.
+	(No_Overlap): Removed, model functions should be used instead.
+	(Equivalent_Keys): Functions over cursors are removed. They were
+	awkward with explicit container parameters.
+	* a-cofuma.adb, a-cofuma.ads (Lift_Equivalent_Keys): New lemma
+	(proof only) procedure to help GNATprove when equivalence over
+	keys is not equality.
+
+2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb,
 	sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads:
 	Minor reformatting and code cleanups.
diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb
index 7fd9b7f..c292701 100644
--- a/gcc/ada/a-cfhama.adb
+++ b/gcc/ada/a-cfhama.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -238,35 +238,6 @@ is
    end Copy;
 
    ---------------------
-   -- Current_To_Last --
-   ---------------------
-
-   function Current_To_Last (Container : Map; Current : Cursor) return Map is
-      Curs : Cursor := First (Container);
-      C    : Map (Container.Capacity, Container.Modulus) :=
-               Copy (Container, Container.Capacity);
-      Node : Count_Type;
-
-   begin
-      if Curs = No_Element then
-         Clear (C);
-         return C;
-
-      elsif Current /= No_Element and not Has_Element (Container, Current) then
-         raise Constraint_Error;
-
-      else
-         while Curs.Node /= Current.Node loop
-            Node := Curs.Node;
-            Delete (C, Curs);
-            Curs := Next (Container, (Node => Node));
-         end loop;
-
-         return C;
-      end if;
-   end Current_To_Last;
-
-   ---------------------
    -- Default_Modulus --
    ---------------------
 
@@ -304,6 +275,7 @@ is
       HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
 
       Free (Container, Position.Node);
+      Position := No_Element;
    end Delete;
 
    -------------
@@ -346,79 +318,6 @@ is
       return Equivalent_Keys (Key, Node.Key);
    end Equivalent_Keys;
 
-   function Equivalent_Keys
-     (Left   : Map;
-      CLeft  : Cursor;
-      Right  : Map;
-      CRight : Cursor) return Boolean
-   is
-   begin
-      if not Has_Element (Left, CLeft) then
-         raise Constraint_Error with
-           "Left cursor of Equivalent_Keys has no element";
-      end if;
-
-      if not Has_Element (Right, CRight) then
-         raise Constraint_Error with
-           "Right cursor of Equivalent_Keys has no element";
-      end if;
-
-      pragma Assert (Vet (Left, CLeft),
-                     "Left cursor of Equivalent_Keys is bad");
-      pragma Assert (Vet (Right, CRight),
-                     "Right cursor of Equivalent_Keys is bad");
-
-      declare
-         LN : Node_Type renames Left.Nodes (CLeft.Node);
-         RN : Node_Type renames Right.Nodes (CRight.Node);
-      begin
-         return Equivalent_Keys (LN.Key, RN.Key);
-      end;
-   end Equivalent_Keys;
-
-   function Equivalent_Keys
-     (Left  : Map;
-      CLeft : Cursor;
-      Right : Key_Type) return Boolean
-   is
-   begin
-      if not Has_Element (Left, CLeft) then
-         raise Constraint_Error with
-           "Left cursor of Equivalent_Keys has no element";
-      end if;
-
-      pragma Assert (Vet (Left, CLeft),
-                     "Left cursor in Equivalent_Keys is bad");
-
-      declare
-         LN : Node_Type renames Left.Nodes (CLeft.Node);
-      begin
-         return Equivalent_Keys (LN.Key, Right);
-      end;
-   end Equivalent_Keys;
-
-   function Equivalent_Keys
-     (Left   : Key_Type;
-      Right  : Map;
-      CRight : Cursor) return Boolean
-   is
-   begin
-      if Has_Element (Right, CRight) then
-         raise Constraint_Error with
-           "Right cursor of Equivalent_Keys has no element";
-      end if;
-
-      pragma Assert (Vet (Right, CRight),
-                     "Right cursor of Equivalent_Keys is bad");
-
-      declare
-         RN : Node_Type renames Right.Nodes (CRight.Node);
-
-      begin
-         return Equivalent_Keys (Left, RN.Key);
-      end;
-   end Equivalent_Keys;
-
    -------------
    -- Exclude --
    -------------
@@ -460,37 +359,109 @@ is
       return (Node => Node);
    end First;
 
-   -----------------------
-   -- First_To_Previous --
-   -----------------------
+   ------------------
+   -- Formal_Model --
+   ------------------
 
-   function First_To_Previous
-     (Container : Map;
-      Current : Cursor) return Map is
-      Curs : Cursor;
-      C    : Map (Container.Capacity, Container.Modulus) :=
-               Copy (Container, Container.Capacity);
-      Node : Count_Type;
+   package body Formal_Model is
 
-   begin
-      Curs := Current;
+      ----------
+      -- Keys --
+      ----------
 
-      if Curs = No_Element then
-         return C;
+      function Keys (Container : Map) return K.Sequence is
+         Position : Count_Type := HT_Ops.First (Container);
+         R        : K.Sequence;
 
-      elsif not Has_Element (Container, Curs) then
-         raise Constraint_Error;
+      begin
+         --  Can't use First, Next or Element here, since they depend on models
+         --  for their postconditions.
 
-      else
-         while Curs.Node /= 0 loop
-            Node := Curs.Node;
-            Delete (C, Curs);
-            Curs := Next (Container, (Node => Node));
+         while Position /= 0 loop
+            R := K.Add (R, Container.Nodes (Position).Key);
+            Position := HT_Ops.Next (Container, Position);
          end loop;
 
-         return C;
-      end if;
-   end First_To_Previous;
+         return R;
+      end Keys;
+
+      ----------------------------
+      -- Lift_Abstraction_Level --
+      ----------------------------
+
+      procedure Lift_Abstraction_Level (Container : Map) is null;
+
+      -----------------------
+      -- Mapping_preserved --
+      -----------------------
+
+      function Mapping_Preserved
+        (K_Left  : K.Sequence;
+         K_Right : K.Sequence;
+         P_Left  : P.Map;
+         P_Right : P.Map) return Boolean
+      is
+      begin
+         for C of P_Left loop
+            if not P.Has_Key (P_Right, C)
+              or else P.Get (P_Left,  C) > K.Length (K_Left)
+              or else P.Get (P_Right, C) > K.Length (K_Right)
+              or else K.Get (K_Left,  P.Get (P_Left,  C)) /=
+                      K.Get (K_Right, P.Get (P_Right, C))
+            then
+               return False;
+            end if;
+         end loop;
+
+         return True;
+      end Mapping_Preserved;
+
+      -----------
+      -- Model --
+      -----------
+
+      function Model (Container : Map) return M.Map is
+         Position : Count_Type := HT_Ops.First (Container);
+         R        : M.Map;
+
+      begin
+         --  Can't use First, Next or Element here, since they depend on models
+         --  for their postconditions.
+
+         while Position /= 0 loop
+            R := M.Add (Container => R,
+                        New_Key   => Container.Nodes (Position).Key,
+                        New_Item  => Container.Nodes (Position).Element);
+            Position := HT_Ops.Next (Container, Position);
+         end loop;
+
+         return R;
+      end Model;
+
+      ---------------
+      -- Positions --
+      ---------------
+
+      function Positions (Container : Map) return P.Map is
+         I        : Count_Type := 1;
+         Position : Count_Type := HT_Ops.First (Container);
+         R        : P.Map;
+
+      begin
+         --  Can't use First, Next or Element here, since they depend on models
+         --  for their postconditions.
+
+         while Position /= 0 loop
+            R := P.Add (R, (Node => Position), I);
+            pragma Assert (P.Length (R) = I);
+            Position := HT_Ops.Next (Container, Position);
+            I := I + 1;
+         end loop;
+
+         return R;
+      end Positions;
+
+   end Formal_Model;
 
    ----------
    -- Free --
@@ -748,40 +719,6 @@ is
    end Next;
 
    -------------
-   -- Overlap --
-   -------------
-
-   function Overlap (Left, Right : Map) return Boolean is
-      Left_Node  : Count_Type;
-      Left_Nodes : Nodes_Type renames Left.Nodes;
-
-   begin
-      if Length (Right) = 0 or Length (Left) = 0 then
-         return False;
-      end if;
-
-      if Left'Address = Right'Address then
-         return True;
-      end if;
-
-      Left_Node := First (Left).Node;
-      while Left_Node /= 0 loop
-         declare
-            N : Node_Type renames Left_Nodes (Left_Node);
-            E : Key_Type renames N.Key;
-         begin
-            if Find (Right, E).Node /= 0 then
-               return True;
-            end if;
-         end;
-
-         Left_Node := HT_Ops.Next (Left, Left_Node);
-      end loop;
-
-      return False;
-   end Overlap;
-
-   -------------
    -- Replace --
    -------------
 
@@ -850,35 +787,6 @@ is
       Node.Next := Next;
    end Set_Next;
 
-   ------------------
-   -- Strict_Equal --
-   ------------------
-
-   function Strict_Equal (Left, Right : Map) return Boolean is
-      CuL : Cursor := First (Left);
-      CuR : Cursor := First (Right);
-
-   begin
-      if Length (Left) /= Length (Right) then
-         return False;
-      end if;
-
-      while CuL.Node /= 0 or else CuR.Node /= 0 loop
-         if CuL.Node /= CuR.Node
-           or else
-             Left.Nodes (CuL.Node).Element /= Right.Nodes (CuR.Node).Element
-           or else Left.Nodes (CuL.Node).Key /= Right.Nodes (CuR.Node).Key
-         then
-            return False;
-         end if;
-
-         CuL := Next (Left, CuL);
-         CuR := Next (Right, CuR);
-      end loop;
-
-      return True;
-   end Strict_Equal;
-
    ---------
    -- Vet --
    ---------
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index 8d6e96a..bc10de0 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -44,17 +44,11 @@
 --    and its previous version C'Old) for expressing properties, which is not
 --    possible if cursors encapsulate an access to the underlying container.
 
---    There are four new functions:
-
---      function Strict_Equal (Left, Right : Map) return Boolean;
---      function Overlap (Left, Right : Map) return Boolean;
---      function First_To_Previous (Container : Map; Current : Cursor)
---         return Map;
---      function Current_To_Last (Container : Map; Current : Cursor)
---         return Map;
-
---    See detailed specifications for these subprograms
+--  Iteration over maps is done using the Iterable aspect which is SPARK
+--  compatible. For of iteration ranges over keys instead of elements.
 
+with Ada.Containers.Functional_Vectors;
+with Ada.Containers.Functional_Maps;
 private with Ada.Containers.Hash_Tables;
 
 generic
@@ -63,77 +57,267 @@ generic
 
    with function Hash (Key : Key_Type) return Hash_Type;
    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
-   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Hashed_Maps with
-  Pure,
   SPARK_Mode
 is
-   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
                   Next        => Next,
                   Has_Element => Has_Element,
-                  Element     => Element),
-     Default_Initial_Condition => Is_Empty (Map);
+                  Element     => Key),
+     Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0;
    pragma Preelaborable_Initialization (Map);
 
-   type Cursor is private;
-   pragma Preelaborable_Initialization (Cursor);
-
    Empty_Map : constant Map;
 
-   No_Element : constant Cursor;
+   type Cursor is record
+      Node : Count_Type;
+   end record;
+
+   No_Element : constant Cursor := (Node => 0);
+
+   function Length (Container : Map) return Count_Type with
+     Global => null,
+     Post   => Length'Result <= Container.Capacity;
+
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   package Formal_Model with Ghost is
+      subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+      package M is new Ada.Containers.Functional_Maps
+        (Element_Type    => Element_Type,
+         Key_Type        => Key_Type,
+         Equivalent_Keys => Equivalent_Keys);
+
+      function "="
+        (Left  : M.Map;
+         Right : M.Map) return Boolean renames M."=";
+
+      function "<="
+        (Left  : M.Map;
+         Right : M.Map) return Boolean renames M."<=";
+
+      package K is new Ada.Containers.Functional_Vectors
+        (Element_Type => Key_Type,
+         Index_Type   => Positive_Count_Type);
+
+      function "="
+        (Left  : K.Sequence;
+         Right : K.Sequence) return Boolean renames K."=";
+
+      function "<"
+        (Left  : K.Sequence;
+         Right : K.Sequence) return Boolean renames K."<";
+
+      function "<="
+        (Left  : K.Sequence;
+         Right : K.Sequence) return Boolean renames K."<=";
+
+      package P is new Ada.Containers.Functional_Maps
+        (Key_Type        => Cursor,
+         Element_Type    => Positive_Count_Type,
+         Equivalent_Keys => "=");
+
+      function "="
+        (Left  : P.Map;
+         Right : P.Map) return Boolean renames P."=";
+
+      function "<="
+        (Left  : P.Map;
+         Right : P.Map) return Boolean renames P."<=";
+
+      function Mapping_Preserved
+        (K_Left  : K.Sequence;
+         K_Right : K.Sequence;
+         P_Left  : P.Map;
+         P_Right : P.Map) return Boolean
+      with
+        Ghost,
+        Global => null,
+        Post   =>
+          (if Mapping_Preserved'Result then
+
+             --  Right contains all the cursors of Left
+
+             P.Keys_Included (P_Left, P_Right)
+
+               --  Mappings from cursors to elements induced by K_Left, P_Left
+               --  and K_Right, P_Right are the same.
+
+               and (for all C of P_Left =>
+                     K.Get (K_Left, P.Get (P_Left, C)) =
+                     K.Get (K_Right, P.Get (P_Right, C))));
+
+      function Model (Container : Map) return M.Map with
+      --  The highlevel model of a map is a map from keys to elements. Neither
+      --  cursors nor order of elements are represented in this model. Keys are
+      --  modeled up to equivalence.
+
+        Ghost,
+        Global => null;
+
+      function Keys (Container : Map) return K.Sequence with
+      --  The Keys sequence represents the underlying list structure of maps
+      --  that is used for iteration. It stores the actual values of keys in
+      --  the map. It does not model cursors nor elements.
+
+        Ghost,
+        Global => null,
+        Post   =>
+          K.Length (Keys'Result) = Length (Container)
+
+            --  It only contains keys contained in Model
+
+            and (for all Key of Keys'Result =>
+                   M.Has_Key (Model (Container), Key))
+
+            --  It contains all the keys contained in Model
+
+            and
+              (for all Key of Model (Container) =>
+                (for some L of Keys'Result => Equivalent_Keys (L, Key)))
+
+            --  It has no duplicate
+
+            and
+              (for all I in 1 .. Length (Container) =>
+                (for all J in 1 .. Length (Container) =>
+                  (if Equivalent_Keys
+                        (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
+                   then I = J)));
+      pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
+
+      function Positions (Container : Map) return P.Map with
+      --  The Positions map is used to model cursors. It only contains valid
+      --  cursors and map them to their position in the container.
+
+        Ghost,
+        Global => null,
+        Post   =>
+          not P.Has_Key (Positions'Result, No_Element)
+
+            --  Positions of cursors are smaller than the container's length.
+
+            and then
+              (for all I of Positions'Result =>
+                P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+            --  No two cursors have the same position. Note that we do not
+            --  state that there is a cursor in the map for each position, as
+            --  it is rarely needed.
+
+            and then
+              (for all J of Positions'Result =>
+                (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
+                  then I = J)));
+
+      procedure Lift_Abstraction_Level (Container : Map) with
+        --  Lift_Abstraction_Level is a ghost procedure that does nothing but
+        --  assume that we can access to the same elements by iterating over
+        --  positions or cursors.
+        --  This information is not generally useful except when switching from
+        --  a lowlevel, cursor aware view of a container, to a highlevel
+        --  position based view.
+
+        Ghost,
+        Global => null,
+        Post   =>
+          (for all Key of Keys (Container) =>
+            (for some I of Positions (Container) =>
+              K.Get (Keys (Container), P.Get (Positions (Container), I)) =
+                Key));
+
+      function Contains
+        (C : M.Map;
+         K : Key_Type) return Boolean renames M.Has_Key;
+      --  To improve readability of contracts, we rename the function used to
+      --  search for a key in the model to Contains.
+
+      function Element
+        (C : M.Map;
+         K : Key_Type) return Element_Type renames M.Get;
+      --  To improve readability of contracts, we rename the function used to
+      --  access an element in the model to Element.
+   end Formal_Model;
+   use Formal_Model;
 
    function "=" (Left, Right : Map) return Boolean with
-     Global => null;
+     Global => null,
+     Post   => "="'Result = (Model (Left) = Model (Right));
 
    function Capacity (Container : Map) return Count_Type with
-     Global => null;
+     Global => null,
+     Post   => Capacity'Result = Container.Capacity;
 
    procedure Reserve_Capacity
      (Container : in out Map;
       Capacity  : Count_Type)
    with
      Global => null,
-     Pre    => Capacity <= Container.Capacity;
-
-   function Length (Container : Map) return Count_Type with
-     Global => null;
+     Pre    => Capacity <= Container.Capacity,
+     Post   => Model (Container) = Model (Container)'Old;
 
    function Is_Empty (Container : Map) return Boolean with
-     Global => null;
+     Global => null,
+     Post   => Is_Empty'Result = M.Is_Empty (Model (Container));
 
    procedure Clear (Container : in out Map) with
-     Global => null;
+     Global => null,
+     Post   => Length (Container) = 0 and M.Is_Empty (Model (Container));
 
    procedure Assign (Target : in out Map; Source : Map) with
      Global => null,
-     Pre    => Target.Capacity >= Length (Source);
+     Pre    => Target.Capacity >= Length (Source),
+     Post   =>
+       Model (Target) = Model (Source)
+         and Length (Source) = Length (Target)
+
+         --  Actual keys are preserved
+
+         and
+           (for all Key of Keys (Source) =>
+              Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
 
    function Copy
      (Source   : Map;
       Capacity : Count_Type := 0) return Map
    with
      Global => null,
-     Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
+     Pre    => Capacity = 0 or else Capacity >= Source.Capacity,
+     Post   =>
+       Model (Copy'Result) = Model (Source)
+         and Keys (Copy'Result) = Keys (Source)
+         and Positions (Copy'Result) = Positions (Source)
+         and (if Capacity = 0 then
+                 Copy'Result.Capacity = Source.Capacity
+              else
+                 Copy'Result.Capacity = Capacity);
    --  Copy returns a container stricty equal to Source. It must have
    --  the same cursors associated with each element. Therefore:
-   --  - capacity=0 means use container.capacity as capacity of target
+   --  - capacity=0 means use Source.Capacity as capacity of target
    --  - the modulus cannot be changed.
 
    function Key (Container : Map; Position : Cursor) return Key_Type with
      Global => null,
-     Pre    => Has_Element (Container, Position);
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Key'Result =
+         K.Get (Keys (Container), P.Get (Positions (Container), Position));
+   pragma Annotate (GNATprove, Inline_For_Proof, Key);
 
    function Element
      (Container : Map;
       Position  : Cursor) return Element_Type
    with
      Global => null,
-     Pre    => Has_Element (Container, Position);
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Element'Result = Element (Model (Container), Key (Container, Position));
+   pragma Annotate (GNATprove, Inline_For_Proof, Element);
 
    procedure Replace_Element
      (Container : in out Map;
@@ -141,11 +325,40 @@ is
       New_Item  : Element_Type)
    with
      Global => null,
-     Pre    => Has_Element (Container, Position);
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+
+       --  Order of keys and cursors are preserved
+
+       Keys (Container) = Keys (Container)'Old
+         and Positions (Container) = Positions (Container)'Old
+
+         --  New_Item is now associated to the key at position Position in
+         --  Container.
+
+         and Element (Container, Position) = New_Item
+
+         --  Elements associated to other keys are preserved
+
+         and M.Same_Keys (Model (Container), Model (Container)'Old)
+         and M.Elements_Equal_Except
+               (Model (Container),
+                Model (Container)'Old,
+                Key (Container, Position));
 
    procedure Move (Target : in out Map; Source : in out Map) with
      Global => null,
-     Pre    => Target.Capacity >= Length (Source);
+     Pre    => Target.Capacity >= Length (Source),
+     Post   =>
+       Model (Target) = Model (Source)'Old
+         and Length (Source)'Old = Length (Target)
+         and Length (Source) = 0
+
+         --  Actual keys are preserved
+
+         and
+           (for all Key of Keys (Source)'Old =>
+              Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
 
    procedure Insert
      (Container : in out Map;
@@ -154,8 +367,55 @@ is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
-     Global => null,
-     Pre    => Length (Container) < Container.Capacity;
+     Global         => null,
+     Pre            =>
+       Length (Container) < Container.Capacity or Contains (Container, Key),
+     Post           =>
+       Contains (Container, Key)
+         and Has_Element (Container, Position)
+         and Equivalent_Keys
+               (Formal_Hashed_Maps.Key (Container, Position), Key),
+     Contract_Cases =>
+
+       --  If Key is already in Container, it is not modified and Inserted is
+       --  set to False.
+
+       (Contains (Container, Key) =>
+          not Inserted
+            and Model (Container) = Model (Container)'Old
+            and Keys (Container) = Keys (Container)'Old
+            and Positions (Container) = Positions (Container)'Old,
+
+        --  Otherwise, Key is inserted in Container and Inserted is set to True
+
+        others =>
+          Inserted
+            and Length (Container) = Length (Container)'Old + 1
+
+            --  Key now maps to New_Item
+
+            and Formal_Hashed_Maps.Key (Container, Position) = Key
+            and Element (Model (Container), Key) = New_Item
+
+            --  Other keys are preserved
+
+            and Model (Container)'Old <= Model (Container)
+            and M.Keys_Included_Except
+                  (Model (Container),
+                   Model (Container)'Old,
+                   Key)
+
+            --  Mapping from cursors to keys are preserved
+
+            and Mapping_Preserved
+                  (K_Left  => Keys (Container)'Old,
+                   K_Right => Keys (Container),
+                   P_Left  => Positions (Container)'Old,
+                   P_Right => Positions (Container))
+            and P.Keys_Included_Except
+                  (Positions (Container),
+                   Positions (Container)'Old,
+                   Position));
 
    procedure Insert
      (Container : in out Map;
@@ -163,16 +423,100 @@ is
       New_Item  : Element_Type)
    with
      Global => null,
-     Pre    => Length (Container) < Container.Capacity
-                 and then (not Contains (Container, Key));
+     Pre    =>
+       Length (Container) < Container.Capacity
+        and then (not Contains (Container, Key)),
+     Post   =>
+       Length (Container) = Length (Container)'Old + 1
+         and Contains (Container, Key)
+
+         --  Key now maps to New_Item
+
+         and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
+         and Element (Model (Container), Key) = New_Item
+
+         --  Other keys are preserved
+
+         and Model (Container)'Old <= Model (Container)
+         and M.Keys_Included_Except
+               (Model (Container),
+                Model (Container)'Old,
+                Key)
+
+         --  Mapping from cursors to keys are preserved
+
+         and Mapping_Preserved
+               (K_Left  => Keys (Container)'Old,
+                K_Right => Keys (Container),
+                P_Left  => Positions (Container)'Old,
+                P_Right => Positions (Container))
+         and P.Keys_Included_Except
+               (Positions (Container),
+                Positions (Container)'Old,
+                Find (Container, Key));
 
    procedure Include
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
-     Global => null,
-     Pre    => Length (Container) < Container.Capacity;
+     Global         => null,
+     Pre            =>
+       Length (Container) < Container.Capacity or Contains (Container, Key),
+     Post           =>
+       Contains (Container, Key) and Element (Container, Key) = New_Item,
+     Contract_Cases =>
+
+       --  If Key is already in Container, Key is mapped to New_Item
+
+       (Contains (Container, Key) =>
+
+          --  Cursors are preserved
+
+          Positions (Container) = Positions (Container)'Old
+
+            --  The key equivalent to Key in Container is replaced by Key
+
+            and K.Get (Keys (Container),
+                       P.Get (Positions (Container), Find (Container, Key))) =
+                Key
+            and K.Equal_Except
+                  (Keys (Container)'Old,
+                   Keys (Container),
+                   P.Get (Positions (Container), Find (Container, Key)))
+
+            --  Elements associated to other keys are preserved
+
+            and M.Same_Keys (Model (Container), Model (Container)'Old)
+            and M.Elements_Equal_Except
+                  (Model (Container),
+                   Model (Container)'Old,
+                   Key),
+
+        --  Otherwise, Key is inserted in Container
+
+        others =>
+          Length (Container) = Length (Container)'Old + 1
+
+            --  Other keys are preserved
+
+            and Model (Container)'Old <= Model (Container)
+            and M.Keys_Included_Except
+                  (Model (Container),
+                   Model (Container)'Old,
+                   Key)
+
+            --  Mapping from cursors to keys are preserved
+
+            and Mapping_Preserved
+                  (K_Left  => Keys (Container)'Old,
+                   K_Right => Keys (Container),
+                   P_Left  => Positions (Container)'Old,
+                   P_Right => Positions (Container))
+            and P.Keys_Included_Except
+                  (Positions (Container),
+                   Positions (Container)'Old,
+                   Find (Container, Key)));
 
    procedure Replace
      (Container : in out Map;
@@ -180,98 +524,212 @@ is
       New_Item  : Element_Type)
    with
      Global => null,
-     Pre    => Contains (Container, Key);
+     Pre    => Contains (Container, Key),
+     Post   =>
+
+       --  Cursors are preserved
+
+       Positions (Container) = Positions (Container)'Old
+
+         --  The key equivalent to Key in Container is replaced by Key
+
+         and K.Get (Keys (Container),
+                    P.Get (Positions (Container), Find (Container, Key))) = Key
+         and K.Equal_Except
+              (Keys (Container)'Old,
+               Keys (Container),
+               P.Get (Positions (Container), Find (Container, Key)))
+
+         --  New_Item is now associated to the Key in Container
+
+         and Element (Model (Container), Key) = New_Item
+
+         --  Elements associated to other keys are preserved
+
+         and M.Same_Keys (Model (Container), Model (Container)'Old)
+         and M.Elements_Equal_Except
+               (Model (Container),
+                Model (Container)'Old,
+                Key);
 
    procedure Exclude (Container : in out Map; Key : Key_Type) with
-     Global => null;
+     Global         => null,
+     Post           => not Contains (Container, Key),
+     Contract_Cases =>
+
+       --  If Key is not in Container, nothing is changed
+
+       (not Contains (Container, Key) =>
+          Model (Container) = Model (Container)'Old
+            and Keys (Container) = Keys (Container)'Old
+            and Positions (Container) = Positions (Container)'Old,
+
+        --  Otherwise, Key is removed from Container
+
+        others =>
+          Length (Container) = Length (Container)'Old - 1
+
+            --  Other keys are preserved
+
+            and Model (Container) <= Model (Container)'Old
+            and M.Keys_Included_Except
+                  (Model (Container)'Old,
+                   Model (Container),
+                   Key)
+
+            --  Mapping from cursors to keys are preserved
+
+            and Mapping_Preserved
+                  (K_Left  => Keys (Container),
+                   K_Right => Keys (Container)'Old,
+                   P_Left  => Positions (Container),
+                   P_Right => Positions (Container)'Old)
+            and P.Keys_Included_Except
+                  (Positions (Container)'Old,
+                   Positions (Container),
+                   Find (Container, Key)'Old));
 
    procedure Delete (Container : in out Map; Key : Key_Type) with
      Global => null,
-     Pre    => Contains (Container, Key);
+     Pre    => Contains (Container, Key),
+     Post   =>
+       Length (Container) = Length (Container)'Old - 1
+
+         --  Key is no longer in Container
+
+         and not Contains (Container, Key)
+
+         --  Other keys are preserved
+
+         and Model (Container) <= Model (Container)'Old
+         and M.Keys_Included_Except
+               (Model (Container)'Old,
+                Model (Container),
+                Key)
+
+         --  Mapping from cursors to keys are preserved
+
+         and Mapping_Preserved
+               (K_Left  => Keys (Container),
+                K_Right => Keys (Container)'Old,
+                P_Left  => Positions (Container),
+                P_Right => Positions (Container)'Old)
+         and P.Keys_Included_Except
+               (Positions (Container)'Old,
+                Positions (Container),
+                Find (Container, Key)'Old);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
      Global => null,
-     Pre    => Has_Element (Container, Position);
+     Pre    => Has_Element (Container, Position),
+     Post   =>
+       Position = No_Element
+         and Length (Container) = Length (Container)'Old - 1
+
+         --  The key at position Position is no longer in Container
+
+         and not Contains (Container, Key (Container, Position)'Old)
+         and not P.Has_Key (Positions (Container), Position'Old)
+
+         --  Other keys are preserved
+
+         and Model (Container) <= Model (Container)'Old
+         and M.Keys_Included_Except
+               (Model (Container)'Old,
+                Model (Container),
+                Key (Container, Position)'Old)
+
+         --  Mapping from cursors to keys are preserved
+
+         and Mapping_Preserved
+               (K_Left  => Keys (Container),
+                K_Right => Keys (Container)'Old,
+                P_Left  => Positions (Container),
+                P_Right => Positions (Container)'Old)
+         and P.Keys_Included_Except
+               (Positions (Container)'Old,
+                Positions (Container),
+                Position'Old);
 
    function First (Container : Map) return Cursor with
-     Global => null;
+     Global         => null,
+     Contract_Cases =>
+       (Length (Container) = 0 =>
+          First'Result = No_Element,
+
+        others =>
+          Has_Element (Container, First'Result)
+            and P.Get (Positions (Container), First'Result) = 1);
 
    function Next (Container : Map; Position : Cursor) return Cursor with
-     Global => null,
-     Pre    => Has_Element (Container, Position) or else Position = No_Element;
+     Global         => null,
+     Pre            =>
+       Has_Element (Container, Position) or else Position = No_Element,
+     Contract_Cases =>
+       (Position = No_Element
+          or else P.Get (Positions (Container), Position) = Length (Container)
+        =>
+          Next'Result = No_Element,
+
+        others =>
+          Has_Element (Container, Next'Result)
+            and then P.Get (Positions (Container), Next'Result) =
+                     P.Get (Positions (Container), Position) + 1);
 
    procedure Next (Container : Map; Position : in out Cursor) with
-     Global => null,
-     Pre    => Has_Element (Container, Position) or else Position = No_Element;
+     Global         => null,
+     Pre            =>
+       Has_Element (Container, Position) or else Position = No_Element,
+     Contract_Cases =>
+       (Position = No_Element
+          or else P.Get (Positions (Container), Position) = Length (Container)
+        =>
+          Position = No_Element,
+
+        others =>
+          Has_Element (Container, Position)
+            and then P.Get (Positions (Container), Position) =
+                     P.Get (Positions (Container), Position'Old) + 1);
 
    function Find (Container : Map; Key : Key_Type) return Cursor with
-     Global => null;
+     Global         => null,
+     Contract_Cases =>
 
-   function Contains (Container : Map; Key : Key_Type) return Boolean with
-     Global => null;
+       --  If Key is not is not contained in Container, Find returns No_Element
 
-   function Element (Container : Map; Key : Key_Type) return Element_Type with
-     Global => null,
-     Pre    => Contains (Container, Key);
+       (not Contains (Model (Container), Key) =>
+          Find'Result = No_Element,
 
-   function Has_Element (Container : Map; Position : Cursor) return Boolean
-   with
-     Global => null;
+        --  Otherwise, Find returns a valid cusror in Container
 
-   function Equivalent_Keys
-     (Left   : Map;
-      CLeft  : Cursor;
-      Right  : Map;
-      CRight : Cursor) return Boolean
-   with
-     Global => null;
+        others =>
+          P.Has_Key (Positions (Container), Find'Result)
 
-   function Equivalent_Keys
-     (Left  : Map;
-      CLeft : Cursor;
-      Right : Key_Type) return Boolean
-   with
-     Global => null;
+            --  The key designated by the result of Find is Key
 
-   function Equivalent_Keys
-     (Left   : Key_Type;
-      Right  : Map;
-      CRight : Cursor) return Boolean
-   with
-     Global => null;
-
-   function Default_Modulus (Capacity : Count_Type) return Hash_Type with
-     Global => null;
+            and Equivalent_Keys
+                  (Formal_Hashed_Maps.Key (Container, Find'Result), Key));
 
-   function Strict_Equal (Left, Right : Map) return Boolean with
-     Ghost,
-     Global => null;
-   --  Strict_Equal returns True if the containers are physically equal, i.e.
-   --  they are structurally equal (function "=" returns True) and that they
-   --  have the same set of cursors.
+   function Contains (Container : Map; Key : Key_Type) return Boolean with
+     Global => null,
+     Post   => Contains'Result = Contains (Model (Container), Key);
+   pragma Annotate (GNATprove, Inline_For_Proof, Contains);
 
-   function First_To_Previous (Container : Map; Current : Cursor) return Map
-   with
-     Ghost,
+   function Element (Container : Map; Key : Key_Type) return Element_Type with
      Global => null,
-     Pre    => Has_Element (Container, Current) or else Current = No_Element;
+     Pre    => Contains (Container, Key),
+     Post   => Element'Result = Element (Model (Container), Key);
+   pragma Annotate (GNATprove, Inline_For_Proof, Element);
 
-   function Current_To_Last (Container : Map; Current : Cursor) return Map
+   function Has_Element (Container : Map; Position : Cursor) return Boolean
    with
-     Ghost,
      Global => null,
-     Pre    => Has_Element (Container, Current) or else Current = No_Element;
-   --  First_To_Previous returns a container containing all elements preceding
-   --  Current (excluded) in Container. Current_To_Last returns a container
-   --  containing all elements following Current (included) in Container.
-   --  These two new functions can be used to express invariant properties in
-   --  loops which iterate over containers. First_To_Previous returns the part
-   --  of the container already scanned and Current_To_Last the part not
-   --  scanned yet.
-
-   function Overlap (Left, Right : Map) return Boolean with
+     Post   =>
+       Has_Element'Result = P.Has_Key (Positions (Container), Position);
+   pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
+
+   function Default_Modulus (Capacity : Count_Type) return Hash_Type with
      Global => null;
-   --  Overlap returns True if the containers have common keys
 
 private
    pragma SPARK_Mode (Off);
@@ -302,12 +760,6 @@ private
 
    use HT_Types;
 
-   type Cursor is record
-      Node : Count_Type;
-   end record;
-
    Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
 
-   No_Element : constant Cursor := (Node => 0);
-
 end Ada.Containers.Formal_Hashed_Maps;
diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb
index e4ee198..38e481b 100644
--- a/gcc/ada/a-cofuma.adb
+++ b/gcc/ada/a-cofuma.adb
@@ -93,8 +93,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
             K : constant Key_Type := Get (Left.Keys, I);
          begin
             if not Equivalent_Keys (K, New_Key)
-              and then Get (Right.Elements, Find (Right.Keys, K)) /=
-                       Get (Left.Elements, I)
+              and then
+                (Find (Right.Keys, K) = 0
+                   or else Get (Right.Elements, Find (Right.Keys, K)) /=
+                           Get (Left.Elements, I))
             then
                return False;
             end if;
@@ -116,8 +118,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
          begin
             if not Equivalent_Keys (K, X)
               and then not Equivalent_Keys (K, Y)
-              and then Get (Right.Elements, Find (Right.Keys, K)) /=
-                       Get (Left.Elements, I)
+              and then
+                (Find (Right.Keys, K) = 0
+                   or else Get (Right.Elements, Find (Right.Keys, K)) /=
+                           Get (Left.Elements, I))
             then
                return False;
             end if;
@@ -229,6 +233,16 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       return Length (Container.Elements);
    end Length;
 
+   --------------------------
+   -- Lift_Equivalent_Keys --
+   --------------------------
+
+   procedure Lift_Equivalent_Keys
+     (Container : Map;
+      Left      : Key_Type;
+      Right     : Key_Type)
+   is null;
+
    ---------------
    -- Same_Keys --
    ---------------
diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads
index 9d3bb97..1172d11 100644
--- a/gcc/ada/a-cofuma.ads
+++ b/gcc/ada/a-cofuma.ads
@@ -48,6 +48,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
    --  Maps are empty when default initialized.
    --  "For in" quantification over maps should not be used.
    --  "For of" quantification over maps iterates over keys.
+   --  Note that, for proof, for of quantification is understood modulo
+   --  equivalence (quantification includes keys equivalent to keys of the
+   --  map).
 
    -----------------------
    --  Basic operations --
@@ -71,6 +74,22 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
      Global => null;
    --  Return the number of mappings in Container
 
+   procedure Lift_Equivalent_Keys
+     (Container : Map;
+      Left      : Key_Type;
+      Right     : Key_Type)
+   --  Lemma function which can be called manually to allow GNATprove to deduce
+   --  that Has_Key and Get always return the same result on equivalent keys.
+
+   with
+     Ghost,
+     Global => null,
+     Pre    => Equivalent_Keys (Left, Right),
+     Post   =>
+       Has_Key (Container, Left) = Has_Key (Container, Right)
+         and (if Has_Key (Container, Left) then
+                Get (Container, Left) = Get (Container, Right));
+
    ------------------------
    -- Property Functions --
    ------------------------
@@ -162,12 +181,12 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
 
    with
      Global => null,
-     Pre    => Keys_Included_Except (Left, Right, New_Key),
      Post   =>
        Elements_Equal_Except'Result =
          (for all Key of Left =>
            (if not Equivalent_Keys (Key, New_Key) then
-               Get (Left, Key) = Get (Right, Key)));
+               Has_Key (Right, Key)
+                 and then Get (Left, Key) = Get (Right, Key)));
 
    function Elements_Equal_Except
      (Left  : Map;
@@ -179,14 +198,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
 
    with
      Global => null,
-     Pre    => Keys_Included_Except (Left, Right, X, Y),
      Post   =>
        Elements_Equal_Except'Result =
          (for all Key of Left =>
            (if not Equivalent_Keys (Key, X)
               and not Equivalent_Keys (Key, Y)
             then
-               Get (Left, Key) = Get (Right, Key)));
+               Has_Key (Right, Key)
+                 and then Get (Left, Key) = Get (Right, Key)));
 
    ----------------------------
    -- Construction Functions --
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 2833fff..8ed4893 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -2738,7 +2738,7 @@ package body Checks is
       S_Typ   : Entity_Id;
       Arr     : Node_Id   := Empty;  -- initialize to prevent warning
       Arr_Typ : Entity_Id := Empty;  -- initialize to prevent warning
-      OK      : Boolean;
+      OK      : Boolean   := False;  -- initialize to prevent warning
 
       Is_Subscr_Ref : Boolean;
       --  Set true if Expr is a subscript
@@ -7936,7 +7936,8 @@ package body Checks is
       Rlo, Rhi : Uint;
       --  Ranges of values for right operand (operator case)
 
-      Llo, Lhi : Uint;
+      Llo : Uint := No_Uint;  -- initialize to prevent warning
+      Lhi : Uint := No_Uint;  -- initialize to prevent warning
       --  Ranges of values for left operand (operator case)
 
       LLIB : constant Entity_Id := Base_Type (Standard_Long_Long_Integer);
@@ -8238,6 +8239,7 @@ package body Checks is
             else
                declare
                   Rtype    : Entity_Id;
+                  pragma Warnings (Off, Rtype);
                   New_Alts : List_Id;
                   New_Exp  : Node_Id;
 
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 094f70e..8520de4 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -3174,7 +3174,7 @@ package body Exp_Ch3 is
          if Present (Variant_Part (Comp_List)) then
             declare
                Variant_Alts : constant List_Id := New_List;
-               Var_Loc      : Source_Ptr;
+               Var_Loc      : Source_Ptr := No_Location;
                Variant      : Node_Id;
 
             begin
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index e247c8b..21d2621 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -2700,7 +2700,7 @@ package body Exp_Ch4 is
       --  last operand is always retained, in case it provides the bounds for
       --  a null result.
 
-      Opnd : Node_Id;
+      Opnd : Node_Id := Empty;
       --  Current operand being processed in the loop through operands. After
       --  this loop is complete, always contains the last operand (which is not
       --  the same as Operands (NN), since null operands are skipped).
@@ -2742,13 +2742,13 @@ package body Exp_Ch4 is
       --  This is either an integer literal node, or an identifier reference to
       --  a constant entity initialized to the appropriate value.
 
-      Last_Opnd_Low_Bound : Node_Id;
+      Last_Opnd_Low_Bound : Node_Id := Empty;
       --  A tree node representing the low bound of the last operand. This
       --  need only be set if the result could be null. It is used for the
       --  special case of setting the right low bound for a null result.
       --  This is of type Ityp.
 
-      Last_Opnd_High_Bound : Node_Id;
+      Last_Opnd_High_Bound : Node_Id := Empty;
       --  A tree node representing the high bound of the last operand. This
       --  need only be set if the result could be null. It is used for the
       --  special case of setting the right high bound for a null result.
@@ -4036,6 +4036,7 @@ package body Exp_Ch4 is
          declare
             Len : Node_Id;
             Res : Node_Id;
+            pragma Warnings (Off, Res);
 
          begin
             for J in 1 .. Number_Dimensions (E) loop
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 8f52966..0a9bc0e 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -6722,7 +6722,7 @@ package body Exp_Ch7 is
 
          --  Local variables
 
-         Bod_Stmts       : List_Id;
+         Bod_Stmts       : List_Id := No_List;
          Finalizer_Decls : List_Id := No_List;
          Rec_Def         : Node_Id;
 
@@ -7068,7 +7068,7 @@ package body Exp_Ch7 is
             --  Local variables
 
             Alts       : List_Id;
-            Counter_Id : Entity_Id;
+            Counter_Id : Entity_Id := Empty;
             Decl       : Node_Id;
             Decl_Id    : Entity_Id;
             Decl_Typ   : Entity_Id;
@@ -7305,7 +7305,7 @@ package body Exp_Ch7 is
 
          --  Local variables
 
-         Bod_Stmts       : List_Id;
+         Bod_Stmts       : List_Id := No_List;
          Finalizer_Decls : List_Id := No_List;
          Rec_Def         : Node_Id;
 
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 4bdd525..0a6a03b 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -673,7 +673,7 @@ package body Exp_Disp is
       --  Local variables
 
       New_Node          : Node_Id;
-      SCIL_Node         : Node_Id;
+      SCIL_Node         : Node_Id := Empty;
       SCIL_Related_Node : Node_Id := Call_Node;
 
    --  Start of processing for Expand_Dispatching_Call
diff --git a/gcc/ada/g-dyntab.adb b/gcc/ada/g-dyntab.adb
index 8210419..384d513 100644
--- a/gcc/ada/g-dyntab.adb
+++ b/gcc/ada/g-dyntab.adb
@@ -34,6 +34,7 @@ pragma Compiler_Unit_Warning;
 with GNAT.Heap_Sort_G;
 
 with Ada.Unchecked_Deallocation;
+with System;
 
 package body GNAT.Dynamic_Tables is
 
@@ -44,7 +45,7 @@ package body GNAT.Dynamic_Tables is
    -- Local Subprograms --
    -----------------------
 
-   procedure Grow (T : in out Instance; New_Last : Table_Count_Type);
+   procedure Grow (T : in out Instance; New_Last : Table_Last_Type);
    --  This is called when we are about to set the value of Last to a value
    --  that is larger than Last_Allocated. This reallocates the table to the
    --  larger size, as indicated by New_Last. At the time this is called,
@@ -128,14 +129,12 @@ package body GNAT.Dynamic_Tables is
 
    begin
       if T.Table = Empty then
-         pragma Assert (T.P.Last_Allocated = First - 1);
-         pragma Assert (T.P.Last = First - 1);
+         pragma Assert (T.P = (Last_Allocated | Last => First - 1));
          null;
       else
          Free (Temp);
          T.Table := Empty;
-         T.P.Last_Allocated := First - 1;
-         T.P.Last := First - 1;
+         T.P := (Last_Allocated | Last => First - 1);
       end if;
    end Free;
 
@@ -143,7 +142,7 @@ package body GNAT.Dynamic_Tables is
    -- Grow --
    ----------
 
-   procedure Grow (T : in out Instance; New_Last : Table_Count_Type) is
+   procedure Grow (T : in out Instance; New_Last : Table_Last_Type) is
 
       --  Note: Type Alloc_Ptr below needs to be declared locally so we know
       --  the bounds. That means that the collection is local, so is finalized
@@ -158,7 +157,7 @@ package body GNAT.Dynamic_Tables is
       subtype Table_Length_Type is Table_Index_Type'Base
         range 0 .. Table_Index_Type'Base'Last;
 
-      Old_Last_Allocated   : constant Table_Count_Type  := T.P.Last_Allocated;
+      Old_Last_Allocated   : constant Table_Last_Type  := T.P.Last_Allocated;
       Old_Allocated_Length : constant Table_Length_Type :=
                                Old_Last_Allocated - First + 1;
 
@@ -241,24 +240,82 @@ package body GNAT.Dynamic_Tables is
       Free (T);
    end Init;
 
+   --------------
+   -- Is_Empty --
+   --------------
+
+   function Is_Empty (T : Instance) return Boolean is
+      Result : constant Boolean := T.P.Last = Table_Low_Bound - 1;
+   begin
+      pragma Assert (Result = (T.Table = Empty));
+      return Result;
+   end Is_Empty;
+
    ----------
    -- Last --
    ----------
 
-   function Last (T : Instance) return Table_Count_Type is
+   function Last (T : Instance) return Table_Last_Type is
    begin
       return T.P.Last;
    end Last;
 
+   ----------
+   -- Move --
+   ----------
+
+   procedure Move (From, To : in out Instance) is
+   begin
+      pragma Assert (Is_Empty (To));
+      To := From;
+
+      From.Table            := Empty;
+      From.Locked           := False;
+      From.P.Last_Allocated := Table_Low_Bound - 1;
+      From.P.Last           := Table_Low_Bound - 1;
+      pragma Assert (Is_Empty (From));
+   end Move;
+
    -------------
    -- Release --
    -------------
 
    procedure Release (T : in out Instance) is
-      pragma Assert (not T.Locked);
-      Old_Last_Allocated : constant Table_Count_Type := T.P.Last_Allocated;
+      Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated;
+
+      function New_Last_Allocated return Table_Last_Type;
+      --  Compute the new value of Last_Allocated. This is normally equal to
+      --  Last, but if Release_Threshold /= 0, then we need to take that into
+      --  account.
+
+      function New_Last_Allocated return Table_Last_Type is
+         subtype Table_Length_Type is Table_Index_Type'Base
+           range 0 .. Table_Index_Type'Base'Last;
+         Length : constant Table_Length_Type := T.P.Last - First + 1;
+         Comp_Size_In_Bytes : constant Table_Length_Type :=
+           Table_Type'Component_Size / System.Storage_Unit;
+         Length_Threshold : constant Table_Length_Type :=
+           Table_Length_Type (Release_Threshold) / Comp_Size_In_Bytes;
+      begin
+         if Release_Threshold = 0
+           or else Length < Length_Threshold
+         then
+            return T.P.Last;
+         else
+            declare
+               Extra_Length : constant Table_Length_Type := Length / 1000;
+            begin
+               return (Length + Extra_Length) - 1 + First;
+            end;
+         end if;
+      end New_Last_Allocated;
+
+      New_Last_Alloc : constant Table_Last_Type := New_Last_Allocated;
+
+   --  Start of processing for Release
+
    begin
-      if T.P.Last /= T.P.Last_Allocated then
+      if New_Last_Alloc < T.P.Last_Allocated then
          pragma Assert (T.P.Last < T.P.Last_Allocated);
          pragma Assert (T.Table /= Empty);
 
@@ -272,23 +329,21 @@ package body GNAT.Dynamic_Tables is
               new Ada.Unchecked_Conversion (Table_Ptr, Old_Alloc_Ptr);
 
             subtype Alloc_Type is
-              Table_Type (First .. First + T.P.Last - 1);
+              Table_Type (First .. New_Last_Alloc);
             type Alloc_Ptr is access all Alloc_Type;
 
             function To_Table_Ptr is
-              new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
+               new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
 
             Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table);
-            New_Table : constant Alloc_Ptr :=
-                          new Alloc_Type'(Old_Table (Alloc_Type'Range));
+            New_Table : constant Alloc_Ptr := new Alloc_Type;
          begin
-            T.P.Last_Allocated := T.P.Last;
+            New_Table (Alloc_Type'Range) := Old_Table (Alloc_Type'Range);
+            T.P.Last_Allocated := New_Last_Alloc;
             Free (Old_Table);
             T.Table := To_Table_Ptr (New_Table);
          end;
       end if;
-
-      pragma Assert (T.P.Last = T.P.Last_Allocated);
    end Release;
 
    --------------
@@ -329,8 +384,7 @@ package body GNAT.Dynamic_Tables is
    -- Set_Last --
    --------------
 
-   procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type) is
-      pragma Assert (not T.Locked);
+   procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is
    begin
       if New_Val > T.P.Last_Allocated then
          Grow (T, New_Val);
diff --git a/gcc/ada/g-dyntab.ads b/gcc/ada/g-dyntab.ads
index eb71815..9bfccc2 100644
--- a/gcc/ada/g-dyntab.ads
+++ b/gcc/ada/g-dyntab.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---                     Copyright (C) 2000-2016, AdaCore                     --
+--                     Copyright (C) 2000-2017, AdaCore                     --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -36,13 +36,10 @@
 --  arrays as closely as possible with the one additional capability of
 --  dynamically modifying the value of the Last attribute.
 
---  This package provides a facility similar to that of GNAT.Table, except
---  that this package declares a type that can be used to define dynamic
---  instances of the table, while an instantiation of GNAT.Table creates a
---  single instance of the table type.
+--  This package provides a facility similar to that of Ada.Containers.Vectors.
 
 --  Note that these three interfaces should remain synchronized to keep as much
---  coherency as possible among these three related units:
+--  coherency as possible among these related units:
 --
 --     GNAT.Dynamic_Tables
 --     GNAT.Table
@@ -56,9 +53,10 @@ generic
    type Table_Component_Type is private;
    type Table_Index_Type     is range <>;
 
-   Table_Low_Bound : Table_Index_Type;
-   Table_Initial   : Positive := 8;
-   Table_Increment : Natural := 100;
+   Table_Low_Bound   : Table_Index_Type;
+   Table_Initial     : Positive := 8;
+   Table_Increment   : Natural := 100;
+   Release_Threshold : Natural := 0; -- size in bytes
 
 package GNAT.Dynamic_Tables is
 
@@ -69,15 +67,42 @@ package GNAT.Dynamic_Tables is
 
    --  The lower bound of Table_Index_Type is ignored.
 
-   pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First);
+   --  Table_Component_Type must not be a type with controlled parts.
 
-   function First return Table_Index_Type;
-   pragma Inline (First);
-   --  Export First as synonym for Table_Low_Bound (parallel with use of Last)
+   --  The Table_Initial value controls the allocation of the table when
+   --  it is first allocated.
+
+   --  The Table_Increment value controls the amount of increase, if the
+   --  table has to be increased in size. The value given is a percentage
+   --  value (e.g. 100 = increase table size by 100%, i.e. double it).
+
+   --  The Last and Set_Last subprograms provide control over the current
+   --  logical allocation. They are quite efficient, so they can be used
+   --  freely (expensive reallocation occurs only at major granularity
+   --  chunks controlled by the allocation parameters).
+
+   --  Note: we do not make the table components aliased, since this would
+   --  restrict the use of table for discriminated types. If it is necessary
+   --  to take the access of a table element, use Unrestricted_Access.
+
+   --  WARNING: On HPPA, the virtual addressing approach used in this unit
+   --  is incompatible with the indexing instructions on the HPPA. So when
+   --  using this unit, compile your application with -mdisable-indexing.
+
+   --  WARNING: If the table is reallocated, then the address of all its
+   --  components will change. So do not capture the address of an element
+   --  and then use the address later after the table may be reallocated.
+   --  One tricky case of this is passing an element of the table to a
+   --  subprogram by reference where the table gets reallocated during
+   --  the execution of the subprogram. The best rule to follow is never
+   --  to pass a table element as a parameter except for the case of IN
+   --  mode parameters with scalar values.
+
+   pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First);
 
    subtype Valid_Table_Index_Type is Table_Index_Type'Base
      range Table_Low_Bound .. Table_Index_Type'Base'Last;
-   subtype Table_Count_Type is Table_Index_Type'Base
+   subtype Table_Last_Type is Table_Index_Type'Base
      range Table_Low_Bound - 1 .. Table_Index_Type'Base'Last;
 
    --  Table_Component_Type must not be a type with controlled parts.
@@ -112,7 +137,7 @@ package GNAT.Dynamic_Tables is
 
    --     Table : Table_Type renames T.Table (First .. Last (T));
 
-   --  and the refer to components of Table.
+   --  and then refer to components of Table.
 
    type Table_Ptr is access all Big_Table_Type;
    for Table_Ptr'Storage_Size use 0;
@@ -132,7 +157,7 @@ package GNAT.Dynamic_Tables is
    --  an empty array.
 
    type Instance is record
-      Table : aliased Table_Ptr :=
+      Table : Table_Ptr :=
                 Empty_Table_Array_Ptr_To_Table_Ptr (Empty_Table_Array'Access);
       --  The table itself. The lower bound is the value of First. Logically
       --  the upper bound is the current value of Last (although the actual
@@ -143,35 +168,50 @@ package GNAT.Dynamic_Tables is
       --  to ensure bounds checking, as in:
       --
       --     Tab : Table_Type renames X.Table (First .. X.Last);
+      --
+      --  Note: The Table component must come first. See declarations of
+      --  SCO_Unit_Table and SCO_Table in scos.h.
 
       Locked : Boolean := False;
-      --  Table expansion is permitted only if this switch is set to False. A
-      --  client may set Locked to True, in which case any attempt to expand
-      --  the table will cause an assertion failure. Note that while a table
-      --  is locked, its address in memory remains fixed and unchanging.
+      --  Table expansion is permitted only if this is False. A client may set
+      --  Locked to True, in which case any attempt to expand the table will
+      --  cause an assertion failure. Note that while a table is locked, its
+      --  address in memory remains fixed and unchanging.
 
       P : Table_Private;
    end record;
 
+   function Is_Empty (T : Instance) return Boolean;
+
    procedure Init (T : in out Instance);
    --  Reinitializes the table to empty. There is no need to call this before
    --  using a table; tables default to empty.
 
-   function Last (T : Instance) return Table_Count_Type;
+   function First return Table_Index_Type;
+   pragma Inline (First);
+   --  Export First as synonym for Table_Low_Bound (parallel with use of Last)
+
+   function Last (T : Instance) return Table_Last_Type;
    pragma Inline (Last);
    --  Returns the current value of the last used entry in the table, which can
    --  then be used as a subscript for Table.
 
    procedure Release (T : in out Instance);
    --  Storage is allocated in chunks according to the values given in the
-   --  Table_Initial and Table_Increment parameters. A call to Release releases
-   --  all storage that is allocated, but is not logically part of the current
-   --  array value. Current array values are not affected by this call.
+   --  Table_Initial and Table_Increment parameters. If Release_Threshold is 0
+   --  or the length of the table does not exceed this threshold then a call to
+   --  Release releases all storage that is allocated, but is not logically
+   --  part of the current array value; otherwise the call to Release leaves
+   --  the current array value plus 0.1% of the current table length free
+   --  elements located at the end of the table. This parameter facilitates
+   --  reopening large tables and adding a few elements without allocating a
+   --  chunk of memory. In both cases current array values are not affected by
+   --  this call.
 
    procedure Free (T : in out Instance);
    --  Same as Init
 
-   procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type);
+   procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type);
    pragma Inline (Set_Last);
    --  This procedure sets Last to the indicated value. If necessary the table
    --  is reallocated to accommodate the new value (i.e. on return the
@@ -205,8 +245,11 @@ package GNAT.Dynamic_Tables is
    pragma Inline (Set_Item);
    --  Put Item in the table at position Index. If Index points to an existing
    --  item (i.e. it is in the range First .. Last (T)), the item is replaced.
-   --  Otherwise (i.e. Index > Last (T), the table is expanded, and Last is set
-   --  to Index.
+   --  Otherwise (i.e. Index > Last (T)), the table is expanded, and Last is
+   --  set to Index.
+
+   procedure Move (From, To : in out Instance);
+   --  Moves from From to To, and sets From to empty
 
    procedure Allocate (T : in out Instance; Num : Integer := 1);
    pragma Inline (Allocate);
@@ -236,11 +279,11 @@ package GNAT.Dynamic_Tables is
 private
 
    type Table_Private is record
-      Last_Allocated : Table_Count_Type := Table_Low_Bound - 1;
+      Last_Allocated : Table_Last_Type := Table_Low_Bound - 1;
       --  Subscript of the maximum entry in the currently allocated table.
       --  Initial value ensures that we initially allocate the table.
 
-      Last : Table_Count_Type := Table_Low_Bound - 1;
+      Last : Table_Last_Type := Table_Low_Bound - 1;
       --  Current value of Last function
 
       --  Invariant: Last <= Last_Allocated
diff --git a/gcc/ada/g-table.adb b/gcc/ada/g-table.adb
index c5c5891..1c122d7 100644
--- a/gcc/ada/g-table.adb
+++ b/gcc/ada/g-table.adb
@@ -29,8 +29,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with GNAT.Heap_Sort_G;
-
 with System;        use System;
 with System.Memory; use System.Memory;
 
@@ -38,53 +36,20 @@ with Ada.Unchecked_Conversion;
 
 package body GNAT.Table is
 
-   Min : constant Integer := Integer (Table_Low_Bound);
-   --  Subscript of the minimum entry in the currently allocated table
-
-   Max : Integer;
-   --  Subscript of the maximum entry in the currently allocated table
-
-   Length : Integer := 0;
-   --  Number of entries in currently allocated table. The value of zero
-   --  ensures that we initially allocate the table.
-
-   Last_Val : Integer;
-   --  Current value of Last
-
-   -----------------------
-   -- Local Subprograms --
-   -----------------------
-
-   procedure Reallocate;
-   --  Reallocate the existing table according to the current value stored
-   --  in Max. Works correctly to do an initial allocation if the table
-   --  is currently null.
-
-   pragma Warnings (Off);
-   --  Turn off warnings. The following unchecked conversions are only used
-   --  internally in this package, and cannot never result in any instances
-   --  of improperly aliased pointers for the client of the package.
-
-   function To_Address is new Ada.Unchecked_Conversion (Table_Ptr, Address);
-   function To_Pointer is new Ada.Unchecked_Conversion (Address, Table_Ptr);
-
-   pragma Warnings (On);
-
    --------------
    -- Allocate --
    --------------
 
-   function Allocate (Num : Integer := 1) return Table_Index_Type is
-      Old_Last : constant Integer := Last_Val;
-
+   procedure Allocate (Num : Integer := 1) is
    begin
-      Last_Val := Last_Val + Num;
-
-      if Last_Val > Max then
-         Reallocate;
-      end if;
+      Tab.Allocate (The_Instance, Num);
+   end Allocate;
 
-      return Table_Index_Type (Old_Last + 1);
+   function Allocate (Num : Integer := 1) return Valid_Table_Index_Type is
+      Result : constant Valid_Table_Index_Type := Last + 1;
+   begin
+      Allocate (Num);
+      return Result;
    end Allocate;
 
    ------------
@@ -93,7 +58,7 @@ package body GNAT.Table is
 
    procedure Append (New_Val : Table_Component_Type) is
    begin
-      Set_Item (Table_Index_Type (Last_Val + 1), New_Val);
+      Tab.Append (The_Instance, New_Val);
    end Append;
 
    ----------------
@@ -102,9 +67,7 @@ package body GNAT.Table is
 
    procedure Append_All (New_Vals : Table_Type) is
    begin
-      for J in New_Vals'Range loop
-         Append (New_Vals (J));
-      end loop;
+      Tab.Append_All (The_Instance, New_Vals);
    end Append_All;
 
    --------------------
@@ -113,7 +76,7 @@ package body GNAT.Table is
 
    procedure Decrement_Last is
    begin
-      Last_Val := Last_Val - 1;
+      Tab.Decrement_Last (The_Instance);
    end Decrement_Last;
 
    -----------
@@ -122,7 +85,7 @@ package body GNAT.Table is
 
    function First return Table_Index_Type is
    begin
-      return Table_Low_Bound;
+      return Tab.First;
    end First;
 
    --------------
@@ -130,12 +93,9 @@ package body GNAT.Table is
    --------------
 
    procedure For_Each is
-      Quit : Boolean := False;
+      procedure For_Each is new Tab.For_Each (Action);
    begin
-      for Index in Table_Low_Bound .. Table_Index_Type (Last_Val) loop
-         Action (Index, Table (Index), Quit);
-         exit when Quit;
-      end loop;
+      For_Each (The_Instance);
    end For_Each;
 
    ----------
@@ -144,9 +104,7 @@ package body GNAT.Table is
 
    procedure Free is
    begin
-      Free (To_Address (Table));
-      Table := null;
-      Length := 0;
+      Tab.Free (The_Instance);
    end Free;
 
    --------------------
@@ -155,201 +113,85 @@ package body GNAT.Table is
 
    procedure Increment_Last is
    begin
-      Last_Val := Last_Val + 1;
-
-      if Last_Val > Max then
-         Reallocate;
-      end if;
+      Tab.Increment_Last (The_Instance);
    end Increment_Last;
 
+   --------------
+   -- Is_Empty --
+   --------------
+
+   function Is_Empty return Boolean is
+   begin
+      return Tab.Is_Empty (The_Instance);
+   end Is_Empty;
+
    ----------
    -- Init --
    ----------
 
    procedure Init is
-      Old_Length : constant Integer := Length;
-
    begin
-      Last_Val := Min - 1;
-      Max      := Min + Table_Initial - 1;
-      Length   := Max - Min + 1;
-
-      --  If table is same size as before (happens when table is never
-      --  expanded which is a common case), then simply reuse it. Note
-      --  that this also means that an explicit Init call right after
-      --  the implicit one in the package body is harmless.
-
-      if Old_Length = Length then
-         return;
-
-      --  Otherwise we can use Reallocate to get a table of the right size.
-      --  Note that Reallocate works fine to allocate a table of the right
-      --  initial size when it is first allocated.
-
-      else
-         Reallocate;
-      end if;
+      Tab.Init (The_Instance);
    end Init;
 
    ----------
    -- Last --
    ----------
 
-   function Last return Table_Index_Type is
+   function Last return Table_Last_Type is
    begin
-      return Table_Index_Type (Last_Val);
+      return Tab.Last (The_Instance);
    end Last;
 
-   ----------------
-   -- Reallocate --
-   ----------------
-
-   procedure Reallocate is
-      New_Size   : size_t;
-      New_Length : Long_Long_Integer;
-
-   begin
-      if Max < Last_Val then
-         pragma Assert (not Locked);
-
-         --  Now increment table length until it is sufficiently large. Use
-         --  the increment value or 10, which ever is larger (the reason
-         --  for the use of 10 here is to ensure that the table does really
-         --  increase in size (which would not be the case for a table of
-         --  length 10 increased by 3% for instance). Do the intermediate
-         --  calculation in Long_Long_Integer to avoid overflow.
-
-         while Max < Last_Val loop
-            New_Length :=
-              Long_Long_Integer (Length) *
-                (100 + Long_Long_Integer (Table_Increment)) / 100;
-            Length := Integer'Max (Integer (New_Length), Length + 10);
-            Max := Min + Length - 1;
-         end loop;
-      end if;
-
-      New_Size :=
-        size_t ((Max - Min + 1) *
-                (Table_Type'Component_Size / Storage_Unit));
-
-      if Table = null then
-         Table := To_Pointer (Alloc (New_Size));
-
-      elsif New_Size > 0 then
-         Table :=
-           To_Pointer (Realloc (Ptr  => To_Address (Table),
-                                Size => New_Size));
-      end if;
-
-      if Length /= 0 and then Table = null then
-         raise Storage_Error;
-      end if;
-
-   end Reallocate;
-
    -------------
    -- Release --
    -------------
 
    procedure Release is
    begin
-      Length := Last_Val - Integer (Table_Low_Bound) + 1;
-      Max    := Last_Val;
-      Reallocate;
+      Tab.Release (The_Instance);
    end Release;
 
+   -------------
+   -- Restore --
+   -------------
+
+   procedure Restore (T : in out Saved_Table) is
+   begin
+      Init;
+      Tab.Move (From => T, To => The_Instance);
+   end Restore;
+
+   ----------
+   -- Save --
+   ----------
+
+   function Save return Saved_Table is
+      Result : Saved_Table;
+   begin
+      Tab.Move (From => The_Instance, To => Result);
+      return Result;
+   end Save;
+
    --------------
    -- Set_Item --
    --------------
 
    procedure Set_Item
-      (Index : Table_Index_Type;
-       Item  : Table_Component_Type)
+     (Index : Valid_Table_Index_Type;
+      Item  : Table_Component_Type)
    is
-      --  If Item is a value within the current allocation, and we are going to
-      --  reallocate, then we must preserve an intermediate copy here before
-      --  calling Increment_Last. Otherwise, if Table_Component_Type is passed
-      --  by reference, we are going to end up copying from storage that might
-      --  have been deallocated from Increment_Last calling Reallocate.
-
-      subtype Allocated_Table_T is
-        Table_Type (Table'First .. Table_Index_Type (Max + 1));
-      --  A constrained table subtype one element larger than the currently
-      --  allocated table.
-
-      Allocated_Table_Address : constant System.Address :=
-                                  Table.all'Address;
-      --  Used for address clause below (we can't use non-static expression
-      --  Table.all'Address directly in the clause because some older versions
-      --  of the compiler do not allow it).
-
-      Allocated_Table : Allocated_Table_T;
-      pragma Import (Ada, Allocated_Table);
-      pragma Suppress (Range_Check, On => Allocated_Table);
-      for Allocated_Table'Address use Allocated_Table_Address;
-      --  Allocated_Table represents the currently allocated array, plus one
-      --  element (the supplementary element is used to have a convenient
-      --  way of computing the address just past the end of the current
-      --  allocation). Range checks are suppressed because this unit uses
-      --  direct calls to System.Memory for allocation, and this can yield
-      --  misaligned storage (and we cannot rely on the bootstrap compiler
-      --  supporting specifically disabling alignment checks, so we need to
-      --  suppress all range checks). It is safe to suppress this check here
-      --  because we know that a (possibly misaligned) object of that type
-      --  does actually exist at that address. ??? We should really improve
-      --  the allocation circuitry here to
-      --  guarantee proper alignment.
-
-      Need_Realloc : constant Boolean := Integer (Index) > Max;
-      --  True if this operation requires storage reallocation (which may
-      --  involve moving table contents around).
-
    begin
-      --  If we're going to reallocate, check whether Item references an
-      --  element of the currently allocated table.
-
-      if Need_Realloc
-        and then Allocated_Table'Address <= Item'Address
-        and then Item'Address <
-                   Allocated_Table (Table_Index_Type (Max + 1))'Address
-      then
-         --  If so, save a copy on the stack because Increment_Last will
-         --  reallocate storage and might deallocate the current table.
-
-         declare
-            Item_Copy : constant Table_Component_Type := Item;
-         begin
-            Set_Last (Index);
-            Table (Index) := Item_Copy;
-         end;
-
-      else
-         --  Here we know that either we won't reallocate (case of Index < Max)
-         --  or that Item is not in the currently allocated table.
-
-         if Integer (Index) > Last_Val then
-            Set_Last (Index);
-         end if;
-
-         Table (Index) := Item;
-      end if;
+      Tab.Set_Item (The_Instance, Index, Item);
    end Set_Item;
 
    --------------
    -- Set_Last --
    --------------
 
-   procedure Set_Last (New_Val : Table_Index_Type) is
+   procedure Set_Last (New_Val : Table_Last_Type) is
    begin
-      if Integer (New_Val) < Last_Val then
-         Last_Val := Integer (New_Val);
-      else
-         Last_Val := Integer (New_Val);
-
-         if Last_Val > Max then
-            Reallocate;
-         end if;
-      end if;
+      Tab.Set_Last (The_Instance, New_Val);
    end Set_Last;
 
    ----------------
@@ -357,69 +199,9 @@ package body GNAT.Table is
    ----------------
 
    procedure Sort_Table is
-
-      Temp : Table_Component_Type;
-      --  A temporary position to simulate index 0
-
-      --  Local subprograms
-
-      function Index_Of (Idx : Natural) return Table_Index_Type;
-      --  Return index of Idx'th element of table
-
-      function Lower_Than (Op1, Op2 : Natural) return Boolean;
-      --  Compare two components
-
-      procedure Move (From : Natural; To : Natural);
-      --  Move one component
-
-      package Heap_Sort is new GNAT.Heap_Sort_G (Move, Lower_Than);
-
-      --------------
-      -- Index_Of --
-      --------------
-
-      function Index_Of (Idx : Natural) return Table_Index_Type is
-         J : constant Integer'Base := Table_Index_Type'Pos (First) + Idx - 1;
-      begin
-         return Table_Index_Type'Val (J);
-      end Index_Of;
-
-      ----------
-      -- Move --
-      ----------
-
-      procedure Move (From : Natural; To : Natural) is
-      begin
-         if From = 0 then
-            Table (Index_Of (To)) := Temp;
-         elsif To = 0 then
-            Temp := Table (Index_Of (From));
-         else
-            Table (Index_Of (To)) := Table (Index_Of (From));
-         end if;
-      end Move;
-
-      ----------------
-      -- Lower_Than --
-      ----------------
-
-      function Lower_Than (Op1, Op2 : Natural) return Boolean is
-      begin
-         if Op1 = 0 then
-            return Lt (Temp, Table (Index_Of (Op2)));
-         elsif Op2 = 0 then
-            return Lt (Table (Index_Of (Op1)), Temp);
-         else
-            return Lt (Table (Index_Of (Op1)), Table (Index_Of (Op2)));
-         end if;
-      end Lower_Than;
-
-   --  Start of processing for Sort_Table
-
+      procedure Sort_Table is new Tab.Sort_Table (Lt);
    begin
-      Heap_Sort.Sort (Natural (Last - First) + 1);
+      Sort_Table (The_Instance);
    end Sort_Table;
 
-begin
-   Init;
 end GNAT.Table;
diff --git a/gcc/ada/g-table.ads b/gcc/ada/g-table.ads
index d27b322..c2c3324 100644
--- a/gcc/ada/g-table.ads
+++ b/gcc/ada/g-table.ads
@@ -29,198 +29,117 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  Resizable one dimensional array support
+--  This package provides a singleton version of GNAT.Dynamic_Tables
+--  (g-dyntab.ads). See that package for documentation. This package just
+--  declares a single instance of GNAT.Dynamic_Tables.Instance, and provides
+--  wrappers for all the subprograms, passing that single instance.
 
---  This package provides an implementation of dynamically resizable one
---  dimensional arrays. The idea is to mimic the normal Ada semantics for
---  arrays as closely as possible with the one additional capability of
---  dynamically modifying the value of the Last attribute.
+--  Note that these three interfaces should remain synchronized to keep as much
+--  coherency as possible among these related units:
+--
+--     GNAT.Dynamic_Tables
+--     GNAT.Table
+--     Table (the compiler unit)
 
---  This package provides a facility similar to that of GNAT.Dynamic_Tables,
---  except that this package declares a single instance of the table type,
---  while an instantiation of GNAT.Dynamic_Tables creates a type that can be
---  used to define dynamic instances of the table.
+pragma Compiler_Unit_Warning;
 
---  Note that this interface should remain synchronized with those in
---  GNAT.Dynamic_Tables and the GNAT compiler source unit Table to keep
---  as much coherency as possible between these three related units.
+with GNAT.Dynamic_Tables;
 
 generic
    type Table_Component_Type is private;
    type Table_Index_Type     is range <>;
 
-   Table_Low_Bound : Table_Index_Type;
-   Table_Initial   : Positive;
-   Table_Increment : Natural;
+   Table_Low_Bound   : Table_Index_Type;
+   Table_Initial     : Positive := 8;
+   Table_Increment   : Natural := 100;
+   Table_Name        : String := ""; -- for debugging printouts
+   pragma Unreferenced (Table_Name);
+   Release_Threshold : Natural := 0;
 
 package GNAT.Table is
    pragma Elaborate_Body;
 
-   --  Table_Component_Type and Table_Index_Type specify the type of the
-   --  array, Table_Low_Bound is the lower bound. Table_Index_Type must be an
-   --  integer type. The effect is roughly to declare:
-
-   --    Table : array (Table_Index_Type range Table_Low_Bound .. <>)
-   --                       of Table_Component_Type;
-
-   --    Note: since the upper bound can be one less than the lower
-   --    bound for an empty array, the table index type must be able
-   --    to cover this range, e.g. if the lower bound is 1, then the
-   --    Table_Index_Type should be Natural rather than Positive.
-
-   --  Table_Component_Type may be any Ada type, except that controlled
-   --  types are not supported. Note however that default initialization
-   --  will NOT occur for array components.
-
-   --  The Table_Initial values controls the allocation of the table when
-   --  it is first allocated, either by default, or by an explicit Init call.
-
-   --  The Table_Increment value controls the amount of increase, if the
-   --  table has to be increased in size. The value given is a percentage
-   --  value (e.g. 100 = increase table size by 100%, i.e. double it).
-
-   --  The Last and Set_Last subprograms provide control over the current
-   --  logical allocation. They are quite efficient, so they can be used
-   --  freely (expensive reallocation occurs only at major granularity
-   --  chunks controlled by the allocation parameters).
-
-   --  Note: we do not make the table components aliased, since this would
-   --  restrict the use of table for discriminated types. If it is necessary
-   --  to take the access of a table element, use Unrestricted_Access.
-
-   --  WARNING: On HPPA, the virtual addressing approach used in this unit
-   --  is incompatible with the indexing instructions on the HPPA. So when
-   --  using this unit, compile your application with -mdisable-indexing.
-
-   --  WARNING: If the table is reallocated, then the address of all its
-   --  components will change. So do not capture the address of an element
-   --  and then use the address later after the table may be reallocated.
-   --  One tricky case of this is passing an element of the table to a
-   --  subprogram by reference where the table gets reallocated during
-   --  the execution of the subprogram. The best rule to follow is never
-   --  to pass a table element as a parameter except for the case of IN
-   --  mode parameters with scalar values.
-
-   type Table_Type is
-     array (Table_Index_Type range <>) of Table_Component_Type;
-   subtype Big_Table_Type is
-     Table_Type (Table_Low_Bound .. Table_Index_Type'Last);
-   --  We work with pointers to a bogus array type that is constrained
-   --  with the maximum possible range bound. This means that the pointer
-   --  is a thin pointer, which is more efficient. Since subscript checks
-   --  in any case must be on the logical, rather than physical bounds,
-   --  safety is not compromised by this approach. These types should never
-   --  be used by the client.
-
-   type Table_Ptr is access all Big_Table_Type;
-   for Table_Ptr'Storage_Size use 0;
-   --  The table is actually represented as a pointer to allow reallocation.
-   --  This type should never be used by the client.
-
-   Table : aliased Table_Ptr := null;
-   --  The table itself. The lower bound is the value of Low_Bound.
-   --  Logically the upper bound is the current value of Last (although
-   --  the actual size of the allocated table may be larger than this).
-   --  The program may only access and modify Table entries in the range
-   --  First .. Last.
-
-   Locked : Boolean := False;
-   --  Table expansion is permitted only if this switch is set to False. A
-   --  client may set Locked to True, in which case any attempt to expand
-   --  the table will cause an assertion failure. Note that while a table
-   --  is locked, its address in memory remains fixed and unchanging.
+   package Tab is new GNAT.Dynamic_Tables
+     (Table_Component_Type,
+      Table_Index_Type,
+      Table_Low_Bound,
+      Table_Initial,
+      Table_Increment,
+      Release_Threshold);
+
+   subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type;
+   subtype Table_Last_Type is Tab.Table_Last_Type;
+   subtype Table_Type is Tab.Table_Type;
+   subtype Big_Table_Type is Tab.Big_Table_Type;
+
+   subtype Table_Ptr is Tab.Table_Ptr;
+
+   The_Instance : Tab.Instance;
+   Table : Table_Ptr renames The_Instance.Table;
+   Locked : Boolean renames The_Instance.Locked;
+
+   function Is_Empty return Boolean;
 
    procedure Init;
-   --  This procedure allocates a new table of size Initial (freeing any
-   --  previously allocated larger table). It is not necessary to call
-   --  Init when a table is first instantiated (since the instantiation does
-   --  the same initialization steps). However, it is harmless to do so, and
-   --  Init is convenient in reestablishing a table for new use.
 
-   function Last return Table_Index_Type;
+   function First return Table_Index_Type;
+   pragma Inline (First);
+
+   function Last return Table_Last_Type;
    pragma Inline (Last);
-   --  Returns the current value of the last used entry in the table, which
-   --  can then be used as a subscript for Table. Note that the only way to
-   --  modify Last is to call the Set_Last procedure. Last must always be
-   --  used to determine the logically last entry.
 
    procedure Release;
-   --  Storage is allocated in chunks according to the values given in the
-   --  Initial and Increment parameters. A call to Release releases all
-   --  storage that is allocated, but is not logically part of the current
-   --  array value. Current array values are not affected by this call.
 
    procedure Free;
-   --  Free all allocated memory for the table. A call to Init is required
-   --  before any use of this table after calling Free.
 
-   function First return Table_Index_Type;
-   pragma Inline (First);
-   --  Export First as synonym for Table_Low_Bound (parallel with use of Last)
-
-   procedure Set_Last (New_Val : Table_Index_Type);
+   procedure Set_Last (New_Val : Table_Last_Type);
    pragma Inline (Set_Last);
-   --  This procedure sets Last to the indicated value. If necessary the
-   --  table is reallocated to accommodate the new value (i.e. on return
-   --  the allocated table has an upper bound of at least Last). If Set_Last
-   --  reduces the size of the table, then logically entries are removed
-   --  from the table. If Set_Last increases the size of the table, then
-   --  new entries are logically added to the table.
 
    procedure Increment_Last;
    pragma Inline (Increment_Last);
-   --  Adds 1 to Last (same as Set_Last (Last + 1)
 
    procedure Decrement_Last;
    pragma Inline (Decrement_Last);
-   --  Subtracts 1 from Last (same as Set_Last (Last - 1)
 
    procedure Append (New_Val : Table_Component_Type);
    pragma Inline (Append);
-   --  Equivalent to:
-   --    x.Increment_Last;
-   --    x.Table (x.Last) := New_Val;
-   --  i.e. the table size is increased by one, and the given new item
-   --  stored in the newly created table element.
 
    procedure Append_All (New_Vals : Table_Type);
-   --  Appends all components of New_Vals
 
    procedure Set_Item
-     (Index : Table_Index_Type;
+     (Index : Valid_Table_Index_Type;
       Item  : Table_Component_Type);
    pragma Inline (Set_Item);
-   --  Put Item in the table at position Index. The table is expanded if the
-   --  current table length is less than Index and in that case Last is set to
-   --  Index. Item will replace any value already present in the table at this
-   --  position.
 
-   function Allocate (Num : Integer := 1) return Table_Index_Type;
+   subtype Saved_Table is Tab.Instance;
+   --  Type used for Save/Restore subprograms
+
+   function Save return Saved_Table;
+   --  Resets table to empty, but saves old contents of table in returned
+   --  value, for possible later restoration by a call to Restore.
+
+   procedure Restore (T : in out Saved_Table);
+   --  Given a Saved_Table value returned by a prior call to Save, restores
+   --  the table to the state it was in at the time of the Save call.
+
+   procedure Allocate (Num : Integer := 1);
+   function Allocate (Num : Integer := 1) return Valid_Table_Index_Type;
    pragma Inline (Allocate);
-   --  Adds Num to Last, and returns the old value of Last + 1. Note that
-   --  this function has the possible side effect of reallocating the table.
-   --  This means that a reference X.Table (X.Allocate) is incorrect, since
-   --  the call to X.Allocate may modify the results of calling X.Table.
+   --  Adds Num to Last. The function version also returns the old value of
+   --  Last + 1. Note that this function has the possible side effect of
+   --  reallocating the table. This means that a reference X.Table (X.Allocate)
+   --  is incorrect, since the call to X.Allocate may modify the results of
+   --  calling X.Table.
 
    generic
      with procedure Action
-       (Index : Table_Index_Type;
+       (Index : Valid_Table_Index_Type;
         Item  : Table_Component_Type;
         Quit  : in out Boolean) is <>;
    procedure For_Each;
-   --  Calls procedure Action for each component of the table, or until
-   --  one of these calls set Quit to True.
 
    generic
      with function Lt (Comp1, Comp2 : Table_Component_Type) return Boolean;
    procedure Sort_Table;
-   --  This procedure sorts the components of the table into ascending
-   --  order making calls to Lt to do required comparisons, and using
-   --  assignments to move components around. The Lt function returns True
-   --  if Comp1 is less than Comp2 (in the sense of the desired sort), and
-   --  False if Comp1 is greater than Comp2. For equal objects it does not
-   --  matter if True or False is returned (it is slightly more efficient
-   --  to return False). The sort is not stable (the order of equal items
-   --  in the table is not preserved).
 
 end GNAT.Table;
diff --git a/gcc/ada/namet.adb b/gcc/ada/namet.adb
index aed8531..20dd504 100644
--- a/gcc/ada/namet.adb
+++ b/gcc/ada/namet.adb
@@ -36,6 +36,7 @@
 with Debug;    use Debug;
 with Opt;      use Opt;
 with Output;   use Output;
+with System;   use System;
 with Tree_IO;  use Tree_IO;
 with Widechar; use Widechar;
 
@@ -1093,15 +1094,6 @@ package body Namet is
       Name_Entries.Release;
    end Lock;
 
-   ------------------------
-   -- Name_Chars_Address --
-   ------------------------
-
-   function Name_Chars_Address return System.Address is
-   begin
-      return Name_Chars.Table (0)'Address;
-   end Name_Chars_Address;
-
    ----------------
    -- Name_Enter --
    ----------------
@@ -1139,15 +1131,6 @@ package body Namet is
       return Name_Enter (Buf);
    end Name_Enter;
 
-   --------------------------
-   -- Name_Entries_Address --
-   --------------------------
-
-   function Name_Entries_Address return System.Address is
-   begin
-      return Name_Entries.Table (First_Name_Id)'Address;
-   end Name_Entries_Address;
-
    ------------------------
    -- Name_Entries_Count --
    ------------------------
diff --git a/gcc/ada/namet.ads b/gcc/ada/namet.ads
index b2a2ed5..124f778 100644
--- a/gcc/ada/namet.ads
+++ b/gcc/ada/namet.ads
@@ -32,7 +32,6 @@
 with Alloc;
 with Hostparm; use Hostparm;
 with Table;
-with System;   use System;
 with Types;    use Types;
 
 package Namet is
@@ -564,13 +563,6 @@ package Namet is
    --  Like Write_Name, except that the name written is the decoded name, as
    --  described for Append_Decoded.
 
-   function Name_Chars_Address return System.Address;
-   --  Return starting address of name characters table (used in Back_End call
-   --  to Gigi).
-
-   function Name_Entries_Address return System.Address;
-   --  Return starting address of Names table (used in Back_End call to Gigi)
-
    function Name_Entries_Count return Nat;
    --  Return current number of entries in the names table
 
diff --git a/gcc/ada/namet.h b/gcc/ada/namet.h
index a016f93..84255a8 100644
--- a/gcc/ada/namet.h
+++ b/gcc/ada/namet.h
@@ -6,7 +6,7 @@
  *                                                                          *
  *                              C Header File                               *
  *                                                                          *
- *            Copyright (C) 1992-2016, Free Software Foundation, Inc.       *
+ *            Copyright (C) 1992-2017, Free Software Foundation, Inc.       *
  *                                                                          *
  * GNAT is free software;  you can  redistribute it  and/or modify it under *
  * terms of the  GNU General Public License as published  by the Free Soft- *
@@ -45,11 +45,11 @@ struct Name_Entry
 };
 
 /* Pointer to names table vector. */
-#define Names_Ptr namet__name_entries__table
+#define Names_Ptr namet__name_entries__tab__the_instance
 extern struct Name_Entry *Names_Ptr;
 
 /* Pointer to name characters table. */
-#define Name_Chars_Ptr namet__name_chars__table
+#define Name_Chars_Ptr namet__name_chars__tab__the_instance
 extern char *Name_Chars_Ptr;
 
 /* This is Hostparm.Max_Line_Length.  */
diff --git a/gcc/ada/osint.ads b/gcc/ada/osint.ads
index 4712b98..2805bfe 100644
--- a/gcc/ada/osint.ads
+++ b/gcc/ada/osint.ads
@@ -662,7 +662,7 @@ package Osint is
    --  The suffixes used for the ALI files
 
    function Prep_Suffix return String;
-   --  The suffix used for pre-processed files
+   --  The suffix used for preprocessed files
 
 private
 
diff --git a/gcc/ada/scos.h b/gcc/ada/scos.h
index 6c1f545..4fb396c 100644
--- a/gcc/ada/scos.h
+++ b/gcc/ada/scos.h
@@ -45,8 +45,10 @@ struct SCO_Unit_Table_Entry
 
 typedef struct SCO_Unit_Table_Entry *SCO_Unit_Table_Type;
 
-extern SCO_Unit_Table_Type scos__sco_unit_table__table;
-#define SCO_Unit_Table scos__sco_unit_table__table
+/* The following depends on the fact that The_Instance.Table
+   is the first component. */
+extern SCO_Unit_Table_Type scos__sco_unit_table__the_instance;
+#define SCO_Unit_Table scos__sco_unit_table__the_instance
 
 extern Int scos__sco_unit_table__first(void);
 #define SCO_Unit_Table_First scos__sco_unit_table__first
@@ -74,8 +76,10 @@ struct SCO_Table_Entry
 
 typedef struct SCO_Table_Entry *SCO_Table_Type;
 
-extern SCO_Table_Type scos__sco_table__table;
-#define SCO_Table scos__sco_table__table
+/* The following depends on the fact that The_Instance.Table
+   is the first component. */
+extern SCO_Table_Type scos__sco_table__the_instance;
+#define SCO_Table scos__sco_table__the_instance
 
 extern Int scos__sco_table__first(void);
 #define SCO_Table_First scos__sco_table__first
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 6bf6dfd..2579ab5 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -65,36 +65,51 @@ package body Sem_Elab is
    --  Elab_Call.Last) indicates the current depth of recursion and is used to
    --  identify the outer level.
 
-   type Elab_Call_Entry is record
+   type Elab_Call_Element is record
       Cloc : Source_Ptr;
       Ent  : Entity_Id;
    end record;
 
    package Elab_Call is new Table.Table
-     (Table_Component_Type => Elab_Call_Entry,
+     (Table_Component_Type => Elab_Call_Element,
       Table_Index_Type     => Int,
       Table_Low_Bound      => 1,
       Table_Initial        => 50,
       Table_Increment      => 100,
       Table_Name           => "Elab_Call");
 
-   --  This table is initialized at the start of each outer level call. It
-   --  holds the entities for all subprograms that have been examined for this
-   --  particular outer level call, and is used to prevent both infinite
-   --  recursion, and useless reanalysis of bodies already seen
+   --  The following table records all calls that have been processed starting
+   --  from an outer level call. The table prevents both infinite recursion and
+   --  useless reanalysis of calls within the same context. The use of context
+   --  is important because it allows for proper checks in more complex code:
+
+   --    if ... then
+   --       Call;  --  requires a check
+   --       Call;  --  does not need a check thanks to the table
+   --    elsif ... then
+   --       Call;  --  requires a check, different context
+   --    end if;
+
+   --    Call;     --  requires a check, different context
+
+   type Visited_Element is record
+      Subp_Id : Entity_Id;
+      --  The entity of the subprogram being called
+
+      Context : Node_Id;
+      --  The context where the call to the subprogram occurs
+   end record;
 
    package Elab_Visited is new Table.Table
-     (Table_Component_Type => Entity_Id,
+     (Table_Component_Type => Visited_Element,
       Table_Index_Type     => Int,
       Table_Low_Bound      => 1,
       Table_Initial        => 200,
       Table_Increment      => 100,
       Table_Name           => "Elab_Visited");
 
-   --  This table stores calls to Check_Internal_Call that are delayed until
-   --  all generics are instantiated and in particular until after all generic
-   --  bodies have been inserted. We need to delay, because we need to be able
-   --  to look through the inserted bodies.
+   --  The following table records delayed calls which must be examined after
+   --  all generic bodies have been instantiated.
 
    type Delay_Element is record
       N : Node_Id;
@@ -743,7 +758,7 @@ package body Sem_Elab is
 
          loop
             if (Suppress_Elaboration_Warnings (Ent)
-                or else Elaboration_Checks_Suppressed (Ent))
+                 or else Elaboration_Checks_Suppressed (Ent))
               and then (Inst_Case or else No (Alias (Ent)))
             then
                return;
@@ -913,17 +928,17 @@ package body Sem_Elab is
            Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (C_Scope)));
       end if;
 
-      --  Do not give a warning if the with'ed unit is internal and the
-      --  caller is not internal (since the binder always elaborates
-      --  internal units first).
+      --  Do not give a warning if the with'ed unit is internal and the caller
+      --  is not internal (since the binder always elaborates internal units
+      --  first).
 
-      if Callee_Unit_Internal and (not Caller_Unit_Internal) then
+      if Callee_Unit_Internal and not Caller_Unit_Internal then
          return;
       end if;
 
-      --  For now, if debug flag -gnatdE is not set, do no checking for
-      --  one internal unit withing another. This fixes the problem with
-      --  the sgi build and storage errors. To be resolved later ???
+      --  For now, if debug flag -gnatdE is not set, do no checking for one
+      --  internal unit withing another. This fixes the problem with the sgi
+      --  build and storage errors. To be resolved later ???
 
       if (Callee_Unit_Internal and Caller_Unit_Internal)
         and not Debug_Flag_EE
@@ -1151,7 +1166,7 @@ package body Sem_Elab is
          --  All_Errors_Mode.
 
          if not All_Errors_Mode and not Dynamic_Elaboration_Checks then
-            Set_Suppress_Elaboration_Warnings (W_Scope, True);
+            Set_Suppress_Elaboration_Warnings (W_Scope);
          end if;
       end if;
 
@@ -1218,8 +1233,8 @@ package body Sem_Elab is
             then
                Error_Msg_Node_2 := W_Scope;
                Error_Msg_NE
-                 ("info: call to& in elaboration code " &
-                  "requires pragma Elaborate_All on&?$?", N, E);
+                 ("info: call to& in elaboration code requires pragma "
+                  & "Elaborate_All on&?$?", N, E);
             end if;
 
             --  Set indication for binder to generate Elaborate_All
@@ -1623,14 +1638,22 @@ package body Sem_Elab is
          return;
       end if;
 
-      --  Nothing to do if this is a recursive call (i.e. a call to
-      --  an entity that is already in the Elab_Call stack)
+      --  Determine whether a prior call to the same subprogram was already
+      --  examined within the same context. If this is the case, then there is
+      --  no need to proceed with the various warnings and checks because the
+      --  work was already done for the previous call.
 
-      for J in 1 .. Elab_Visited.Last loop
-         if Ent = Elab_Visited.Table (J) then
-            return;
-         end if;
-      end loop;
+      declare
+         Self : constant Visited_Element :=
+                  (Subp_Id => Ent, Context => Parent (N));
+
+      begin
+         for Index in 1 .. Elab_Visited.Last loop
+            if Self = Elab_Visited.Table (Index) then
+               return;
+            end if;
+         end loop;
+      end;
 
       --  See if we need to analyze this reference. We analyze it if either of
       --  the following conditions is met:
@@ -2394,14 +2417,19 @@ package body Sem_Elab is
          Outer_Level_Sloc := Loc;
       end if;
 
-      Elab_Visited.Append (E);
-
       --  If the call is to a function that renames a literal, no check needed
 
       if Ekind (E) = E_Enumeration_Literal then
          return;
       end if;
 
+      --  Register the subprogram as examined within this particular context.
+      --  This ensures that calls to the same subprogram but in different
+      --  contexts receive warnings and checks of their own since the calls
+      --  may be reached through different flow paths.
+
+      Elab_Visited.Append ((Subp_Id => E, Context => Parent (N)));
+
       Sbody := Unit_Declaration_Node (E);
 
       if not Nkind_In (Sbody, N_Subprogram_Body, N_Package_Body) then
@@ -2422,8 +2450,8 @@ package body Sem_Elab is
       then
          null;
 
-      --  If we have the instantiation case we are done, since we now
-      --  know that the body of the generic appeared earlier.
+      --  If we have the instantiation case we are done, since we now know that
+      --  the body of the generic appeared earlier.
 
       elsif Inst_Case then
          return;
@@ -2579,26 +2607,22 @@ package body Sem_Elab is
          if GNATprove_Mode then
             null;
 
-         --  Deal with dynamic elaboration check
+         --  Generate an elaboration check
 
          elsif not Elaboration_Checks_Suppressed (E) then
             Set_Elaboration_Entity_Required (E);
 
-            --  Case of no elaboration entity allocated yet
+            --  Create a declaration of the elaboration entity, and insert it
+            --  prior to the subprogram or the generic unit, within the same
+            --  scope. Since the subprogram may be overloaded, create a unique
+            --  entity.
 
             if No (Elaboration_Entity (E)) then
-
-               --  Create object declaration for elaboration entity, and put it
-               --  just in front of the spec of the subprogram or generic unit,
-               --  in the same scope as this unit. The subprogram may be over-
-               --  loaded, so make the name of elaboration entity unique by
-               --  means of a numeric suffix.
-
                declare
                   Loce : constant Source_Ptr := Sloc (E);
                   Ent  : constant Entity_Id  :=
                            Make_Defining_Identifier (Loc,
-                             Chars => New_External_Name (Chars (E), 'E', -1));
+                             New_External_Name (Chars (E), 'E', -1));
 
                begin
                   Set_Elaboration_Entity (E, Ent);
@@ -2629,12 +2653,15 @@ package body Sem_Elab is
                end;
             end if;
 
-            --  Generate check of the elaboration counter
+            --  Generate:
+            --    if Enn = 0 then
+            --       raise Program_Error with "access before elaboration";
+            --    end if;
 
             Insert_Elab_Check (N,
-               Make_Attribute_Reference (Loc,
-                 Attribute_Name => Name_Elaborated,
-                 Prefix         => New_Occurrence_Of (E, Loc)));
+              Make_Attribute_Reference (Loc,
+                Attribute_Name => Name_Elaborated,
+                Prefix         => New_Occurrence_Of (E, Loc)));
          end if;
 
          --  Generate the warning
@@ -2657,8 +2684,8 @@ package body Sem_Elab is
                  ("instantiation of& may occur before body is seen<l<",
                   N, Orig_Ent);
             else
-               --  A rather specific check. For Finalize/Adjust/Initialize,
-               --  if the type has Warnings_Off set, suppress the warning.
+               --  A rather specific check. For Finalize/Adjust/Initialize, if
+               --  the type has Warnings_Off set, suppress the warning.
 
                if Nam_In (Chars (E), Name_Adjust,
                                      Name_Finalize,
@@ -2697,13 +2724,6 @@ package body Sem_Elab is
             Output_Calls (N, Check_Elab_Flag => False);
          end if;
       end if;
-
-      --  Set flag to suppress further warnings on same subprogram
-      --  unless in all errors mode
-
-      if not All_Errors_Mode then
-         Set_Suppress_Elaboration_Warnings (E);
-      end if;
    end Check_Internal_Call_Continue;
 
    ---------------------------
@@ -2909,32 +2929,32 @@ package body Sem_Elab is
          elsif Dynamic_Elaboration_Checks then
             if not Elaboration_Checks_Suppressed (Ent)
               and then not Cunit_SC
-              and then
-                not Restriction_Active (No_Entry_Calls_In_Elaboration_Code)
+              and then not Restriction_Active
+                             (No_Entry_Calls_In_Elaboration_Code)
             then
                --  Runtime elaboration check required. Generate check of the
                --  elaboration counter for the unit containing the entity.
 
                Insert_Elab_Check (N,
                  Make_Attribute_Reference (Loc,
-                   Attribute_Name => Name_Elaborated,
-                   Prefix =>
-                     New_Occurrence_Of (Spec_Entity (Task_Scope), Loc)));
+                   Prefix         =>
+                     New_Occurrence_Of (Spec_Entity (Task_Scope), Loc),
+                   Attribute_Name => Name_Elaborated));
             end if;
 
          else
             --  Force the binder to elaborate other unit first
 
-            if not Suppress_Elaboration_Warnings (Ent)
+            if Elab_Info_Messages
+              and then not Suppress_Elaboration_Warnings (Ent)
               and then not Elaboration_Checks_Suppressed (Ent)
-              and then Elab_Info_Messages
               and then not Suppress_Elaboration_Warnings (Task_Scope)
               and then not Elaboration_Checks_Suppressed (Task_Scope)
             then
                Error_Msg_Node_2 := Task_Scope;
                Error_Msg_NE
-                 ("info: activation of an instance of task type&" &
-                  " requires pragma Elaborate_All on &?$?", N, Ent);
+                 ("info: activation of an instance of task type & requires "
+                  & "pragma Elaborate_All on &?$?", N, Ent);
             end if;
 
             Activate_Elaborate_All_Desirable (N, Task_Scope);
@@ -2988,18 +3008,19 @@ package body Sem_Elab is
      Subp : Entity_Id;
      Scop : Entity_Id)
    is
-      Elab_Unit  : Entity_Id;
+      Elab_Unit : Entity_Id;
 
       --  Check whether this is a call to an Initialize subprogram for a
       --  controlled type. Note that Call can also be a 'Access attribute
       --  reference, which now generates an elaboration check.
 
-      Init_Call  : constant Boolean :=
-                     Nkind (Call) = N_Procedure_Call_Statement
-                       and then Chars (Subp) = Name_Initialize
-                       and then Comes_From_Source (Subp)
-                       and then Present (Parameter_Associations (Call))
-                       and then Is_Controlled (Etype (First_Actual (Call)));
+      Init_Call : constant Boolean :=
+                    Nkind (Call) = N_Procedure_Call_Statement
+                      and then Chars (Subp) = Name_Initialize
+                      and then Comes_From_Source (Subp)
+                      and then Present (Parameter_Associations (Call))
+                      and then Is_Controlled (Etype (First_Actual (Call)));
+
    begin
       --  If the unit is mentioned in a with_clause of the current unit, it is
       --  visible, and we can set the elaboration flag.
@@ -3008,13 +3029,13 @@ package body Sem_Elab is
         or else (Is_Child_Unit (Scop) and then Is_Visible_Lib_Unit (Scop))
       then
          Activate_Elaborate_All_Desirable (Call, Scop);
-         Set_Suppress_Elaboration_Warnings (Scop, True);
+         Set_Suppress_Elaboration_Warnings (Scop);
          return;
       end if;
 
       --  If this is not an initialization call or a call using object notation
-      --  we know that the unit of the called entity is in the context, and
-      --  we can set the flag as well. The unit need not be visible if the call
+      --  we know that the unit of the called entity is in the context, and we
+      --  can set the flag as well. The unit need not be visible if the call
       --  occurs within an instantiation.
 
       if Is_Init_Proc (Subp)
@@ -3025,7 +3046,7 @@ package body Sem_Elab is
 
       else
          Activate_Elaborate_All_Desirable (Call, Scop);
-         Set_Suppress_Elaboration_Warnings (Scop, True);
+         Set_Suppress_Elaboration_Warnings (Scop);
          return;
       end if;
 
@@ -3070,7 +3091,7 @@ package body Sem_Elab is
       end if;
 
       Activate_Elaborate_All_Desirable (Call, Elab_Unit);
-      Set_Suppress_Elaboration_Warnings (Elab_Unit, True);
+      Set_Suppress_Elaboration_Warnings (Elab_Unit);
    end Set_Elaboration_Constraint;
 
    ------------------------
@@ -3616,23 +3637,22 @@ package body Sem_Elab is
             if No (Corresponding_Body (N)) then
                declare
                   Loc     : constant Source_Ptr := Sloc (N);
-                  B       : Node_Id;
-                  Formals : constant List_Id := Copy_Parameter_List (Ent);
-                  Nam     : constant Entity_Id :=
+                  Formals : constant List_Id    := Copy_Parameter_List (Ent);
+                  Nam     : constant Entity_Id  :=
                               Make_Defining_Identifier (Loc, Chars (Ent));
-                  Spec    : Node_Id;
-                  Stats   : constant List_Id :=
-                              New_List
-                               (Make_Raise_Program_Error (Loc,
+                  Stats   : constant List_Id    :=
+                              New_List (
+                                Make_Raise_Program_Error (Loc,
                                   Reason => PE_Access_Before_Elaboration));
+                  Spec    : Node_Id;
 
                begin
                   if Ekind (Ent) = E_Function then
                      Spec :=
                         Make_Function_Specification (Loc,
-                          Defining_Unit_Name => Nam,
+                          Defining_Unit_Name       => Nam,
                           Parameter_Specifications => Formals,
-                          Result_Definition =>
+                          Result_Definition        =>
                             New_Copy_Tree
                               (Result_Definition (Specification (N))));
 
@@ -3645,17 +3665,16 @@ package body Sem_Elab is
                   else
                      Spec :=
                         Make_Procedure_Specification (Loc,
-                          Defining_Unit_Name => Nam,
+                          Defining_Unit_Name       => Nam,
                           Parameter_Specifications => Formals);
                   end if;
 
-                  B := Make_Subprogram_Body (Loc,
-                          Specification => Spec,
-                          Declarations => New_List,
-                          Handled_Statement_Sequence =>
-                            Make_Handled_Sequence_Of_Statements (Loc,  Stats));
-                  Insert_After (N, B);
-                  Analyze (B);
+                  Insert_After_And_Analyze (N,
+                    Make_Subprogram_Body (Loc,
+                      Specification               => Spec,
+                       Declarations               => New_List,
+                       Handled_Statement_Sequence =>
+                         Make_Handled_Sequence_Of_Statements (Loc,  Stats)));
                end;
             end if;
          end;
diff --git a/gcc/ada/table.adb b/gcc/ada/table.adb
index 2c7eb0c..5d4522b 100644
--- a/gcc/ada/table.adb
+++ b/gcc/ada/table.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,9 +29,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Debug;   use Debug;
-with Opt;     use Opt;
-with Output;  use Output;
 with System;  use System;
 with Tree_IO; use Tree_IO;
 
@@ -39,370 +36,20 @@ with System.Memory; use System.Memory;
 
 with Unchecked_Conversion;
 
-pragma Elaborate_All (Output);
-
 package body Table is
    package body Table is
 
-      Min : constant Int := Int (Table_Low_Bound);
-      --  Subscript of the minimum entry in the currently allocated table
-
-      Length : Int := 0;
-      --  Number of entries in currently allocated table. The value of zero
-      --  ensures that we initially allocate the table.
-
-      -----------------------
-      -- Local Subprograms --
-      -----------------------
-
-      procedure Reallocate;
-      --  Reallocate the existing table according to the current value stored
-      --  in Max. Works correctly to do an initial allocation if the table
-      --  is currently null.
-
       function Tree_Get_Table_Address return Address;
       --  Return Null_Address if the table length is zero,
       --  Table (First)'Address if not.
 
-      pragma Warnings (Off);
-      --  Turn off warnings. The following unchecked conversions are only used
-      --  internally in this package, and cannot never result in any instances
-      --  of improperly aliased pointers for the client of the package.
-
-      function To_Address is new Unchecked_Conversion (Table_Ptr, Address);
-      function To_Pointer is new Unchecked_Conversion (Address, Table_Ptr);
-
-      pragma Warnings (On);
-
-      ------------
-      -- Append --
-      ------------
-
-      procedure Append (New_Val : Table_Component_Type) is
-      begin
-         Set_Item (Table_Index_Type (Last_Val + 1), New_Val);
-      end Append;
-
-      ----------------
-      -- Append_All --
-      ----------------
-
-      procedure Append_All (New_Vals : Table_Type) is
-      begin
-         for J in New_Vals'Range loop
-            Append (New_Vals (J));
-         end loop;
-      end Append_All;
-
-      --------------------
-      -- Decrement_Last --
-      --------------------
-
-      procedure Decrement_Last is
-      begin
-         Last_Val := Last_Val - 1;
-      end Decrement_Last;
-
-      ----------
-      -- Free --
-      ----------
-
-      procedure Free is
-      begin
-         Free (To_Address (Table));
-         Table := null;
-         Length := 0;
-      end Free;
-
-      --------------------
-      -- Increment_Last --
-      --------------------
-
-      procedure Increment_Last is
-      begin
-         Last_Val := Last_Val + 1;
-
-         if Last_Val > Max then
-            Reallocate;
-         end if;
-      end Increment_Last;
-
-      ----------
-      -- Init --
-      ----------
-
-      procedure Init is
-         Old_Length : constant Int := Length;
-
-      begin
-         Locked   := False;
-         Last_Val := Min - 1;
-         Max      := Min + (Table_Initial * Table_Factor) - 1;
-         Length   := Max - Min + 1;
-
-         --  If table is same size as before (happens when table is never
-         --  expanded which is a common case), then simply reuse it. Note
-         --  that this also means that an explicit Init call right after
-         --  the implicit one in the package body is harmless.
-
-         if Old_Length = Length then
-            return;
-
-         --  Otherwise we can use Reallocate to get a table of the right size.
-         --  Note that Reallocate works fine to allocate a table of the right
-         --  initial size when it is first allocated.
-
-         else
-            Reallocate;
-         end if;
-      end Init;
-
-      ----------
-      -- Last --
-      ----------
-
-      function Last return Table_Index_Type is
-      begin
-         return Table_Index_Type (Last_Val);
-      end Last;
-
-      ----------------
-      -- Reallocate --
-      ----------------
-
-      procedure Reallocate is
-         New_Size   : Memory.size_t;
-         New_Length : Long_Long_Integer;
-
-      begin
-         if Max < Last_Val then
-            pragma Assert (not Locked);
-
-            --  Make sure that we have at least the initial allocation. This
-            --  is needed in cases where a zero length table is written out.
-
-            Length := Int'Max (Length, Table_Initial);
-
-            --  Now increment table length until it is sufficiently large. Use
-            --  the increment value or 10, which ever is larger (the reason
-            --  for the use of 10 here is to ensure that the table does really
-            --  increase in size (which would not be the case for a table of
-            --  length 10 increased by 3% for instance). Do the intermediate
-            --  calculation in Long_Long_Integer to avoid overflow.
-
-            while Max < Last_Val loop
-               New_Length :=
-                 Long_Long_Integer (Length) *
-                    (100 + Long_Long_Integer (Table_Increment)) / 100;
-               Length := Int'Max (Int (New_Length), Length + 10);
-               Max := Min + Length - 1;
-            end loop;
-
-            if Debug_Flag_D then
-               Write_Str ("--> Allocating new ");
-               Write_Str (Table_Name);
-               Write_Str (" table, size = ");
-               Write_Int (Max - Min + 1);
-               Write_Eol;
-            end if;
-         end if;
-
-         --  Do the intermediate calculation in size_t to avoid signed overflow
-
-         New_Size :=
-           Memory.size_t (Max - Min + 1) *
-                                    (Table_Type'Component_Size / Storage_Unit);
-
-         if Table = null then
-            Table := To_Pointer (Alloc (New_Size));
-
-         elsif New_Size > 0 then
-            Table :=
-              To_Pointer (Realloc (Ptr  => To_Address (Table),
-                                   Size => New_Size));
-         end if;
-
-         if Length /= 0 and then Table = null then
-            Set_Standard_Error;
-            Write_Str ("available memory exhausted");
-            Write_Eol;
-            Set_Standard_Output;
-            raise Unrecoverable_Error;
-         end if;
-      end Reallocate;
-
-      -------------
-      -- Release --
-      -------------
-
-      procedure Release is
-         Extra_Length : Int;
-         Size         : Memory.size_t;
-
-      begin
-         Length := Last_Val - Int (Table_Low_Bound) + 1;
-         Size   := Memory.size_t (Length) *
-                     (Table_Type'Component_Size / Storage_Unit);
-
-         --  If the size of the table exceeds the release threshold then leave
-         --  space to store as many extra elements as 0.1% of the table length.
-
-         if Release_Threshold > 0
-           and then Size > Memory.size_t (Release_Threshold)
-         then
-            Extra_Length := Length / 1000;
-            Length := Length + Extra_Length;
-            Max    := Int (Table_Low_Bound) + Length - 1;
-
-            if Debug_Flag_D then
-               Write_Str ("--> Release_Threshold reached (length=");
-               Write_Int (Int (Size));
-               Write_Str ("): leaving room space for ");
-               Write_Int (Extra_Length);
-               Write_Str (" components");
-               Write_Eol;
-            end if;
-         else
-            Max := Last_Val;
-         end if;
-
-         Reallocate;
-      end Release;
-
-      -------------
-      -- Restore --
-      -------------
-
-      procedure Restore (T : Saved_Table) is
-      begin
-         Free (To_Address (Table));
-         Last_Val := T.Last_Val;
-         Max      := T.Max;
-         Table    := T.Table;
-         Length   := Max - Min + 1;
-      end Restore;
-
-      ----------
-      -- Save --
-      ----------
-
-      function Save return Saved_Table is
-         Res : Saved_Table;
-
-      begin
-         Res.Last_Val := Last_Val;
-         Res.Max      := Max;
-         Res.Table    := Table;
-
-         Table  := null;
-         Length := 0;
-         Init;
-         return Res;
-      end Save;
-
-      --------------
-      -- Set_Item --
-      --------------
-
-      procedure Set_Item
-         (Index : Table_Index_Type;
-          Item  : Table_Component_Type)
-      is
-         --  If Item is a value within the current allocation, and we are going
-         --  to reallocate, then we must preserve an intermediate copy here
-         --  before calling Increment_Last. Otherwise, if Table_Component_Type
-         --  is passed by reference, we are going to end up copying from
-         --  storage that might have been deallocated from Increment_Last
-         --  calling Reallocate.
-
-         subtype Allocated_Table_T is
-           Table_Type (Table'First .. Table_Index_Type (Max + 1));
-         --  A constrained table subtype one element larger than the currently
-         --  allocated table.
-
-         Allocated_Table_Address : constant System.Address :=
-                                     Table.all'Address;
-         --  Used for address clause below (we can't use non-static expression
-         --  Table.all'Address directly in the clause because some older
-         --  versions of the compiler do not allow it).
-
-         Allocated_Table : Allocated_Table_T;
-         pragma Import (Ada, Allocated_Table);
-         pragma Suppress (Range_Check, On => Allocated_Table);
-         for Allocated_Table'Address use Allocated_Table_Address;
-         --  Allocated_Table represents the currently allocated array, plus one
-         --  element (the supplementary element is used to have a convenient
-         --  way of computing the address just past the end of the current
-         --  allocation). Range checks are suppressed because this unit
-         --  uses direct calls to System.Memory for allocation, and this can
-         --  yield misaligned storage (and we cannot rely on the bootstrap
-         --  compiler supporting specifically disabling alignment checks, so we
-         --  need to suppress all range checks). It is safe to suppress this
-         --  check here because we know that a (possibly misaligned) object
-         --  of that type does actually exist at that address.
-         --  ??? We should really improve the allocation circuitry here to
-         --  guarantee proper alignment.
-
-         Need_Realloc : constant Boolean := Int (Index) > Max;
-         --  True if this operation requires storage reallocation (which may
-         --  involve moving table contents around).
-
-      begin
-         --  If we're going to reallocate, check whether Item references an
-         --  element of the currently allocated table.
-
-         if Need_Realloc
-           and then Allocated_Table'Address <= Item'Address
-           and then Item'Address <
-                      Allocated_Table (Table_Index_Type (Max + 1))'Address
-         then
-            --  If so, save a copy on the stack because Increment_Last will
-            --  reallocate storage and might deallocate the current table.
-
-            declare
-               Item_Copy : constant Table_Component_Type := Item;
-            begin
-               Set_Last (Index);
-               Table (Index) := Item_Copy;
-            end;
-
-         else
-            --  Here we know that either we won't reallocate (case of Index <
-            --  Max) or that Item is not in the currently allocated table.
-
-            if Int (Index) > Last_Val then
-               Set_Last (Index);
-            end if;
-
-            Table (Index) := Item;
-         end if;
-      end Set_Item;
-
-      --------------
-      -- Set_Last --
-      --------------
-
-      procedure Set_Last (New_Val : Table_Index_Type) is
-      begin
-         if Int (New_Val) < Last_Val then
-            Last_Val := Int (New_Val);
-
-         else
-            Last_Val := Int (New_Val);
-
-            if Last_Val > Max then
-               Reallocate;
-            end if;
-         end if;
-      end Set_Last;
-
       ----------------------------
       -- Tree_Get_Table_Address --
       ----------------------------
 
       function Tree_Get_Table_Address return Address is
       begin
-         if Length = 0 then
+         if Is_Empty then
             return Null_Address;
          else
             return Table (First)'Address;
@@ -418,15 +65,15 @@ package body Table is
       --  does an implicit Release.
 
       procedure Tree_Read is
+         Last : Int;
       begin
-         Tree_Read_Int (Max);
-         Last_Val := Max;
-         Length := Max - Min + 1;
-         Reallocate;
+         Init;
+         Tree_Read_Int (Last);
+         Set_Last (Table_Last_Type (Last));
 
          Tree_Read_Data
            (Tree_Get_Table_Address,
-             (Last_Val - Int (First) + 1) *
+             (Last - Int (First) + 1) *
 
                --  Note the importance of parenthesizing the following division
                --  to avoid the possibility of intermediate overflow.
@@ -446,11 +93,9 @@ package body Table is
          Tree_Write_Int (Int (Last));
          Tree_Write_Data
            (Tree_Get_Table_Address,
-            (Last_Val - Int (First) + 1) *
+            (Int (Last - First) + 1) *
               (Table_Type'Component_Size / Storage_Unit));
       end Tree_Write;
 
-   begin
-      Init;
    end Table;
 end Table;
diff --git a/gcc/ada/table.ads b/gcc/ada/table.ads
index 29b6fb0..7062665 100644
--- a/gcc/ada/table.ads
+++ b/gcc/ada/table.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,16 +29,20 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package provides an implementation of dynamically resizable one
---  dimensional arrays. The idea is to mimic the normal Ada semantics for
---  arrays as closely as possible with the one additional capability of
---  dynamically modifying the value of the Last attribute.
+--  This package is a wrapper for GNAT.Table, for use in the compiler front
+--  end. It adds the Tree_Write/Tree_Read functionality; everything else is
+--  just a renaming of GNAT.Table. See GNAT.Table (g-table.ads) and
+--  GNAT.Dynamic_Tables (g-dyntab.ads) for documentation.
 
---  Note that this interface should remain synchronized with those in
---  GNAT.Table and GNAT.Dynamic_Tables to keep coherency between these
---  three related units.
+--  Note that these three interfaces should remain synchronized to keep as much
+--  coherency as possible among these related units:
+--
+--     GNAT.Dynamic_Tables
+--     GNAT.Table
+--     Table (the compiler unit)
 
 with Types; use Types;
+with GNAT.Table;
 
 package Table is
    pragma Elaborate_Body;
@@ -50,83 +54,30 @@ package Table is
       Table_Low_Bound   : Table_Index_Type;
       Table_Initial     : Pos;
       Table_Increment   : Nat;
-      Table_Name        : String;
+      Table_Name        : String; -- for debugging printouts
       Release_Threshold : Nat := 0;
 
    package Table is
 
-      --  Table_Component_Type and Table_Index_Type specify the type of the
-      --  array, Table_Low_Bound is the lower bound. Table_Index_Type must be
-      --  an integer type. The effect is roughly to declare:
-
-      --    Table : array (Table_Index_Type range Table_Low_Bound .. <>)
-      --                       of Table_Component_Type;
-
-      --    Note: since the upper bound can be one less than the lower
-      --    bound for an empty array, the table index type must be able
-      --    to cover this range, e.g. if the lower bound is 1, then the
-      --    Table_Index_Type should be Natural rather than Positive.
-
-      --  Table_Component_Type may be any Ada type, except that controlled
-      --  types are not supported. Note however that default initialization
-      --  will NOT occur for array components.
-
-      --  The Table_Initial values controls the allocation of the table when
-      --  it is first allocated, either by default, or by an explicit Init
-      --  call. The value used is Opt.Table_Factor * Table_Initial.
-
-      --  The Table_Increment value controls the amount of increase, if the
-      --  table has to be increased in size. The value given is a percentage
-      --  value (e.g. 100 = increase table size by 100%, i.e. double it).
-
-      --  The Table_Name parameter is simply use in debug output messages it
-      --  has no other usage, and is not referenced in non-debugging mode.
-
-      --  The Last and Set_Last subprograms provide control over the current
-      --  logical allocation. They are quite efficient, so they can be used
-      --  freely (expensive reallocation occurs only at major granularity
-      --  chunks controlled by the allocation parameters).
-
-      --  Note: We do not make the table components aliased, since this would
-      --  restrict the use of table for discriminated types. If it is necessary
-      --  to take the access of a table element, use Unrestricted_Access.
-
-      --  WARNING: On HPPA, the virtual addressing approach used in this unit
-      --  is incompatible with the indexing instructions on the HPPA. So when
-      --  using this unit, compile your application with -mdisable-indexing.
-
-      --  WARNING: If the table is reallocated, then the address of all its
-      --  components will change. So do not capture the address of an element
-      --  and then use the address later after the table may be reallocated.
-      --  One tricky case of this is passing an element of the table to a
-      --  subprogram by reference where the table gets reallocated during
-      --  the execution of the subprogram. The best rule to follow is never
-      --  to pass a table element as a parameter except for the case of IN
-      --  mode parameters with scalar values.
-
-      type Table_Type is
-        array (Table_Index_Type range <>) of Table_Component_Type;
-
-      subtype Big_Table_Type is
-        Table_Type (Table_Low_Bound .. Table_Index_Type'Last);
-      --  We work with pointers to a bogus array type that is constrained
-      --  with the maximum possible range bound. This means that the pointer
-      --  is a thin pointer, which is more efficient. Since subscript checks
-      --  in any case must be on the logical, rather than physical bounds,
-      --  safety is not compromised by this approach.
-
-      type Table_Ptr is access all Big_Table_Type;
-      for Table_Ptr'Storage_Size use 0;
-      --  The table is actually represented as a pointer to allow reallocation
-
-      Table : aliased Table_Ptr := null;
-      --  The table itself. The lower bound is the value of Low_Bound.
-      --  Logically the upper bound is the current value of Last (although
-      --  the actual size of the allocated table may be larger than this).
-      --  The program may only access and modify Table entries in the range
-      --  First .. Last.
-
-      Locked : Boolean := False;
+      package Tab is new GNAT.Table
+        (Table_Component_Type,
+         Table_Index_Type,
+         Table_Low_Bound,
+         Positive (Table_Initial),
+         Natural (Table_Increment),
+         Table_Name,
+         Natural (Release_Threshold));
+
+      subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type;
+      subtype Table_Last_Type is Tab.Table_Last_Type;
+      subtype Table_Type is Tab.Table_Type;
+      subtype Big_Table_Type is Tab.Big_Table_Type;
+
+      subtype Table_Ptr is Tab.Table_Ptr;
+
+      Table : Table_Ptr renames Tab.Table;
+
+      Locked : Boolean renames Tab.Locked;
       --  Table expansion is permitted only if this switch is set to False. A
       --  client may set Locked to True, in which case any attempt to expand
       --  the table will cause an assertion failure. Note that while a table
@@ -136,110 +87,39 @@ package Table is
       --  not move during processing, which means that they cannot be expanded.
       --  The Locked flag is used to enforce this restriction.
 
-      procedure Init;
-      --  This procedure allocates a new table of size Initial (freeing any
-      --  previously allocated larger table). It is not necessary to call
-      --  Init when a table is first instantiated (since the instantiation does
-      --  the same initialization steps). However, it is harmless to do so, and
-      --  Init is convenient in reestablishing a table for new use.
-
-      function Last return Table_Index_Type;
-      pragma Inline (Last);
-      --  Returns the current value of the last used entry in the table, which
-      --  can then be used as a subscript for Table. Note that the only way to
-      --  modify Last is to call the Set_Last procedure. Last must always be
-      --  used to determine the logically last entry.
-
-      procedure Release;
-      --  Storage is allocated in chunks according to the values given in the
-      --  Initial and Increment parameters. If Release_Threshold is 0 or the
-      --  length of the table does not exceed this threshold then a call to
-      --  Release releases all storage that is allocated, but is not logically
-      --  part of the current array value; otherwise the call to Release leaves
-      --  the current array value plus 0.1% of the current table length free
-      --  elements located at the end of the table (this parameter facilitates
-      --  reopening large tables and adding a few elements without allocating a
-      --  chunk of memory). In both cases current array values are not affected
-      --  by this call.
-
-      procedure Free;
-      --  Free all allocated memory for the table. A call to init is required
-      --  before any use of this table after calling Free.
-
-      First : constant Table_Index_Type := Table_Low_Bound;
-      --  Export First as synonym for Low_Bound (parallel with use of Last)
-
-      procedure Set_Last (New_Val : Table_Index_Type);
-      pragma Inline (Set_Last);
-      --  This procedure sets Last to the indicated value. If necessary the
-      --  table is reallocated to accommodate the new value (i.e. on return
-      --  the allocated table has an upper bound of at least Last). If Set_Last
-      --  reduces the size of the table, then logically entries are removed
-      --  from the table. If Set_Last increases the size of the table, then
-      --  new entries are logically added to the table.
-
-      procedure Increment_Last;
-      pragma Inline (Increment_Last);
-      --  Adds 1 to Last (same as Set_Last (Last + 1)
-
-      procedure Decrement_Last;
-      pragma Inline (Decrement_Last);
-      --  Subtracts 1 from Last (same as Set_Last (Last - 1)
-
-      procedure Append (New_Val : Table_Component_Type);
-      pragma Inline (Append);
-      --  Equivalent to:
-      --    x.Increment_Last;
-      --    x.Table (x.Last) := New_Val;
-      --  i.e. the table size is increased by one, and the given new item
-      --  stored in the newly created table element.
-
-      procedure Append_All (New_Vals : Table_Type);
-      --  Appends all components of New_Vals
+      function Is_Empty return Boolean renames Tab.Is_Empty;
 
-      procedure Set_Item
-        (Index : Table_Index_Type;
-         Item  : Table_Component_Type);
-      pragma Inline (Set_Item);
-      --  Put Item in the table at position Index. The table is expanded if
-      --  current table length is less than Index and in that case Last is set
-      --  to Index. Item will replace any value already present in the table
-      --  at this position.
+      procedure Init renames Tab.Init;
 
-      type Saved_Table is private;
-      --  Type used for Save/Restore subprograms
+      function First return Table_Index_Type renames Tab.First;
+      function Last return Table_Last_Type renames Tab.Last;
 
-      function Save return Saved_Table;
-      --  Resets table to empty, but saves old contents of table in returned
-      --  value, for possible later restoration by a call to Restore.
+      procedure Release renames Tab.Release;
 
-      procedure Restore (T : Saved_Table);
-      --  Given a Saved_Table value returned by a prior call to Save, restores
-      --  the table to the state it was in at the time of the Save call.
+      procedure Free renames Tab.Free;
 
-      procedure Tree_Write;
-      --  Writes out contents of table using Tree_IO
+      procedure Set_Last (New_Val : Table_Last_Type) renames Tab.Set_Last;
 
-      procedure Tree_Read;
-      --  Initializes table by reading contents previously written with the
-      --  Tree_Write call (also using Tree_IO).
+      procedure Increment_Last renames Tab.Increment_Last;
+      procedure Decrement_Last renames Tab.Decrement_Last;
 
-   private
+      procedure Append (New_Val : Table_Component_Type) renames Tab.Append;
+      procedure Append_All (New_Vals : Table_Type) renames Tab.Append_All;
 
-      Last_Val : Int;
-      --  Current value of Last. Note that we declare this in the private part
-      --  because we don't want the client to modify Last except through one of
-      --  the official interfaces (since a modification to Last may require a
-      --  reallocation of the table).
+      procedure Set_Item
+        (Index : Valid_Table_Index_Type;
+         Item  : Table_Component_Type) renames Tab.Set_Item;
 
-      Max : Int;
-      --  Subscript of the maximum entry in the currently allocated table
+      subtype Saved_Table is Tab.Saved_Table;
+      function Save return Saved_Table renames Tab.Save;
+      procedure Restore (T : in out Saved_Table) renames Tab.Restore;
 
-      type Saved_Table is record
-         Last_Val : Int;
-         Max      : Int;
-         Table    : Table_Ptr;
-      end record;
+      procedure Tree_Write;
+      --  Writes out contents of table using Tree_IO
+
+      procedure Tree_Read;
+      --  Initializes table by reading contents previously written with the
+      --  Tree_Write call, also using Tree_IO.
 
    end Table;
 end Table;
diff --git a/gcc/ada/uintp.h b/gcc/ada/uintp.h
index fafa139..5263b1b 100644
--- a/gcc/ada/uintp.h
+++ b/gcc/ada/uintp.h
@@ -6,7 +6,7 @@
  *                                                                          *
  *                              C Header File                               *
  *                                                                          *
- *            Copyright (C) 1992-2016, Free Software Foundation, Inc.       *
+ *            Copyright (C) 1992-2017, Free Software Foundation, Inc.       *
  *                                                                          *
  * GNAT is free software;  you can  redistribute it  and/or modify it under *
  * terms of the  GNU General Public License as published  by the Free Soft- *
@@ -101,11 +101,11 @@ extern Boolean UI_Lt			(Uint, Uint);
    the integer value itself.  The origin of the Uints_Ptr table is adjusted so
    that a Uint value of Uint_Bias indexes the first element.  */
 
-#define Uints_Ptr (uintp__uints__table - Uint_Table_Start)
-extern struct Uint_Entry *uintp__uints__table;
+#define Uints_Ptr (uintp__uints__tab__the_instance - Uint_Table_Start)
+extern struct Uint_Entry *uintp__uints__tab__the_instance;
 
-#define Udigits_Ptr uintp__udigits__table
-extern int *uintp__udigits__table;
+#define Udigits_Ptr uintp__udigits__tab__the_instance
+extern int *uintp__udigits__tab__the_instance;
 
 #ifdef __cplusplus
 }
diff --git a/gcc/ada/xoscons.adb b/gcc/ada/xoscons.adb
index 8eecb29..39a39f3 100644
--- a/gcc/ada/xoscons.adb
+++ b/gcc/ada/xoscons.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2008-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 2008-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -26,7 +26,7 @@
 --  The base name of the template file is given by Argument (1). This program
 --  generates the spec for this specified unit (let's call it UNIT_NAME).
 
---  It works in conjunction with a C template file which must be pre-processed
+--  It works in conjunction with a C template file which must be preprocessed
 --  and compiled using the cross compiler. Two input files are used:
 --    - the preprocessed C file: UNIT_NAME-tmplt.i
 --    - the generated assembly file: UNIT_NAME-tmplt.s