gnat1drv.adb (Adjust_Global_Switches): Suppress warnings in codepeer mode here unless -gnateC is specified.

gcc/ada/

2017-11-09  Arnaud Charlet  <charlet@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Suppress warnings in codepeer
	mode here unless -gnateC is specified.
	* switch-c.adb (Scan_Front_End_Switches): Do not suppress warnings with
	-gnatC here.

2017-11-09  Piotr Trojanek  <trojanek@adacore.com>

	* lib-writ.adb (Write_ALI): Remove processing of the frontend xrefs as
	part of the ALI writing; they are now processed directly from memory
	when requested by the backend.
	* lib-xref.ads (Collect_SPARK_Xrefs): Remove.
	(Iterate_SPARK_Xrefs): New routine for iterating over frontend xrefs.
	* lib-xref-spark_specific.adb (Traverse_Compilation_Unit): Remove.
	(Add_SPARK_File): Remove.
	(Add_SPARK_Xref): Refactored from removed code; filters xref entries
	that are trivially uninteresting to the SPARK backend.
	* spark_xrefs.ads: Remove code that is no longer needed.
	* spark_xrefs.adb (dspark): Adapt to use Iterate_SPARK_Xrefs.

2017-11-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb: Update the documentation on adding a new elaboration
	schenario. Add new hash table Recorded_Top_Level_Scenarios.
	(Is_Check_Emitting_Scenario): Removed.
	(Is_Recorded_Top_Level_Scenario): New routine.
	(Kill_Elaboration_Scenario): Reimplemented.
	(Record_Elaboration_Scenario): Mark the scenario as recorded.
	(Set_Is_Recorded_Top_Level_Scenario): New routine.
	(Update_Elaboration_Scenario): Reimplemented.
	* sinfo.adb (Is_Recorded_Scenario): Removed.
	(Set_Is_Recorded_Scenario): Removed.
	* sinfo.ads: Remove attribute Is_Recorded_Scenario along with
	occurrences in nodes.
	(Is_Recorded_Scenario): Removed along with pragma Inline.
	(Set_Is_Recorded_Scenario): Removed along with pragma Inline.

2017-11-09  Piotr Trojanek  <trojanek@adacore.com>

	* sem_prag.adb (Analyze_Part_Of): Change "designate" to "denote" in
	error message.

2017-11-09  Justin Squirek  <squirek@adacore.com>

	* sem_res.adb (Resolve_Allocator): Add warning messages corresponding
	to the allocation of an anonymous access-to-controlled object.

gcc/testsuite/

2017-11-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* gnat.dg/elab3.adb, gnat.dg/elab3.ads, gnat.dg/elab3_pkg.adb,
	gnat.dg/elab3_pkg.ads: New testcase.

2017-11-09  Pierre-Marie de Rodat  <derodat@adacore.com>

    * gnat.dg/controlled2.adb, gnat.dg/controlled4.adb, gnat.dg/finalized.adb:
    Disable the new warning from GNAT.

From-SVN: r254568

1 files changed, 31 insertions, 1044 deletions

diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index a30cb84..5295832 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -27,8 +27,6 @@ with Einfo;       use Einfo;
 with Nmake;       use Nmake;
 with SPARK_Xrefs; use SPARK_Xrefs;
 
-with GNAT.HTable;
-
 separate (Lib.Xref)
 package body SPARK_Specific is
 
@@ -59,9 +57,6 @@ package body SPARK_Specific is
       's'    => True,
       others => False);
 
-   type Entity_Hashed_Range is range 0 .. 255;
-   --  Size of hash table headers
-
    ---------------------
    -- Local Variables --
    ---------------------
@@ -78,187 +73,13 @@ package body SPARK_Specific is
    --  "Heap". These references are added to the regular references when
    --  computing SPARK cross-references.
 
-   -----------------------
-   -- Local Subprograms --
-   -----------------------
-
-   procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat);
-   --  Add file and corresponding scopes for unit to the tables
-   --  SPARK_File_Table and SPARK_Scope_Table. When two units are present
-   --  for the same compilation unit, as it happens for library-level
-   --  instantiations of generics, then Ubody is the number of the body
-   --  unit; otherwise it is No_Unit.
-
-   procedure Add_SPARK_Xrefs;
-   --  Filter table Xrefs to add all references used in SPARK to the table
-   --  SPARK_Xref_Table.
-
-   function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
-   --  Hash function for hash table
-
-   generic
-      with procedure Process (N : Node_Id) is <>;
-   procedure Traverse_Compilation_Unit (CU : Node_Id);
-   --  Call Process on all declarations within compilation unit CU. Bodies
-   --  of stubs are also traversed, but generic declarations are ignored.
-
-   --------------------
-   -- Add_SPARK_File --
-   --------------------
-
-   procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is
-      File : constant Source_File_Index := Source_Index (Uspec);
-      From : constant Scope_Index       := SPARK_Scope_Table.Last + 1;
-
-      Scope_Id : Pos := 1;
-
-      procedure Add_SPARK_Scope (N : Node_Id);
-      --  Add scope N to the table SPARK_Scope_Table
-
-      procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
-      --  Call Add_SPARK_Scope on scopes
-
-      ---------------------
-      -- Add_SPARK_Scope --
-      ---------------------
-
-      procedure Add_SPARK_Scope (N : Node_Id) is
-         E : constant Entity_Id := Defining_Entity (N);
-
-      begin
-         --  Ignore scopes without a proper location
-
-         if Sloc (N) = No_Location then
-            return;
-         end if;
-
-         case Ekind (E) is
-            when E_Entry
-               | E_Entry_Family
-               | E_Function
-               | E_Generic_Function
-               | E_Generic_Package
-               | E_Generic_Procedure
-               | E_Package
-               | E_Package_Body
-               | E_Procedure
-               | E_Protected_Body
-               | E_Protected_Type
-               | E_Task_Body
-               | E_Task_Type
-               | E_Subprogram_Body
-            =>
-               null;
-
-            when E_Void =>
-
-               --  Compilation of prj-attr.adb with -gnatn creates a node with
-               --  entity E_Void for the package defined at a-charac.ads16:13.
-               --  ??? TBD
-
-               return;
-
-            when others =>
-               raise Program_Error;
-         end case;
-
-         --  File_Num and Scope_Num are filled later. From_Xref and To_Xref
-         --  are filled even later, but are initialized to represent an empty
-         --  range.
-
-         SPARK_Scope_Table.Append
-           ((Entity    => E,
-             Scope_Num => Scope_Id,
-             From_Xref => 1,
-             To_Xref   => 0));
-
-         Scope_Id := Scope_Id + 1;
-      end Add_SPARK_Scope;
-
-      --------------------------------
-      -- Detect_And_Add_SPARK_Scope --
-      --------------------------------
-
-      procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
-      begin
-         --  Entries
-
-         if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
-
-           --  Packages
-
-           or else Nkind_In (N, N_Package_Body,
-                                N_Package_Declaration)
-           --  Protected units
-
-           or else Nkind_In (N, N_Protected_Body,
-                                N_Protected_Type_Declaration)
-
-           --  Subprograms
-
-           or else Nkind_In (N, N_Subprogram_Body,
-                                N_Subprogram_Declaration)
-
-           --  Task units
-
-           or else Nkind_In (N, N_Task_Body,
-                                N_Task_Type_Declaration)
-         then
-            Add_SPARK_Scope (N);
-         end if;
-      end Detect_And_Add_SPARK_Scope;
-
-      procedure Traverse_Scopes is new
-        Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
-
-   --  Start of processing for Add_SPARK_File
-
-   begin
-      --  Source file could be inexistant as a result of an error, if option
-      --  gnatQ is used.
-
-      if File <= No_Source_File then
-         return;
-      end if;
-
-      --  Subunits are traversed as part of the top-level unit to which they
-      --  belong.
-
-      if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
-         return;
-      end if;
-
-      Traverse_Scopes (CU => Cunit (Uspec));
-
-      --  When two units are present for the same compilation unit, as it
-      --  happens for library-level instantiations of generics, then add all
-      --  scopes to the same SPARK file.
-
-      if Ubody /= No_Unit then
-         Traverse_Scopes (CU => Cunit (Ubody));
-      end if;
-
-      SPARK_File_Table.Append (
-        (File_Num   => Dspec,
-         From_Scope => From,
-         To_Scope   => SPARK_Scope_Table.Last));
-   end Add_SPARK_File;
-
-   ---------------------
-   -- Add_SPARK_Xrefs --
-   ---------------------
-
-   procedure Add_SPARK_Xrefs is
-      function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
-      --  Return the entity which maps to the input scope index
+   -------------------------
+   -- Iterate_SPARK_Xrefs --
+   -------------------------
 
-      function Get_Scope_Num (E : Entity_Id) return Nat;
-      --  Return the scope number associated with the entity E
+   procedure Iterate_SPARK_Xrefs is
 
-      function Is_Future_Scope_Entity
-        (E : Entity_Id;
-         S : Scope_Index) return Boolean;
-      --  Check whether entity E is in SPARK_Scope_Table at index S or higher
+      procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry);
 
       function Is_SPARK_Reference
         (E   : Entity_Id;
@@ -270,110 +91,29 @@ package body SPARK_Specific is
       --  Return whether the entity or reference scope meets requirements for
       --  being a SPARK scope.
 
-      function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
-      --  Comparison function for Sort call
-
-      procedure Move (From : Natural; To : Natural);
-      --  Move procedure for Sort call
-
-      procedure Set_Scope_Num (E : Entity_Id; Num : Nat);
-      --  Associate entity E with the scope number Num
-
-      procedure Update_Scope_Range
-        (S    : Scope_Index;
-         From : Xref_Index;
-         To   : Xref_Index);
-      --  Update the scope which maps to S with the new range From .. To
-
-      package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
-
-      No_Scope : constant Nat := 0;
-      --  Initial scope counter
-
-      package Scopes is new GNAT.HTable.Simple_HTable
-        (Header_Num => Entity_Hashed_Range,
-         Element    => Nat,
-         No_Element => No_Scope,
-         Key        => Entity_Id,
-         Hash       => Entity_Hash,
-         Equal      => "=");
-      --  Package used to build a correspondence between entities and scope
-      --  numbers used in SPARK cross references.
-
-      Nrefs : Nat := Xrefs.Last;
-      --  Number of references in table. This value may get reset (reduced)
-      --  when we eliminate duplicate reference entries as well as references
-      --  not suitable for local cross-references.
-
-      Nrefs_Add : constant Nat := Drefs.Last;
-      --  Number of additional references which correspond to dereferences in
-      --  the source code.
-
-      Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
-      --  This array contains numbers of references in the Xrefs table. This
-      --  list is sorted in output order. The extra 0'th entry is convenient
-      --  for the call to sort. When we sort the table, we move the indices in
-      --  Rnums around, but we do not move the original table entries.
-
-      ---------------------
-      -- Entity_Of_Scope --
-      ---------------------
-
-      function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
-      begin
-         return SPARK_Scope_Table.Table (S).Entity;
-      end Entity_Of_Scope;
-
-      -------------------
-      -- Get_Scope_Num --
-      -------------------
-
-      function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
-
-      ----------------------------
-      -- Is_Future_Scope_Entity --
-      ----------------------------
-
-      function Is_Future_Scope_Entity
-        (E : Entity_Id;
-         S : Scope_Index) return Boolean
-      is
-         function Is_Past_Scope_Entity return Boolean;
-         --  Check whether entity E is in SPARK_Scope_Table at index strictly
-         --  lower than S.
-
-         --------------------------
-         -- Is_Past_Scope_Entity --
-         --------------------------
-
-         function Is_Past_Scope_Entity return Boolean is
-         begin
-            for Index in SPARK_Scope_Table.First .. S - 1 loop
-               if SPARK_Scope_Table.Table (Index).Entity = E then
-                  return True;
-               end if;
-            end loop;
-
-            return False;
-         end Is_Past_Scope_Entity;
-
-      --  Start of processing for Is_Future_Scope_Entity
+      --------------------
+      -- Add_SPARK_Xref --
+      --------------------
 
+      procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is
+         Ref : Xref_Key renames Xref.Key;
       begin
-         for Index in S .. SPARK_Scope_Table.Last loop
-            if SPARK_Scope_Table.Table (Index).Entity = E then
-               return True;
-            end if;
-         end loop;
+         --  Eliminate entries not appropriate for SPARK
 
-         --  If this assertion fails, this means that the scope which we are
-         --  looking for has been treated already, which reveals a problem in
-         --  the order of cross-references.
-
-         pragma Assert (not Is_Past_Scope_Entity);
+         if SPARK_Entities (Ekind (Ref.Ent))
+           and then SPARK_References (Ref.Typ)
+           and then Is_SPARK_Scope (Ref.Ent_Scope)
+           and then Is_SPARK_Scope (Ref.Ref_Scope)
+           and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
+         then
+            Process
+              (Index,
+               (Entity    => Ref.Ent,
+                Ref_Scope => Ref.Ref_Scope,
+                Rtype     => Ref.Typ));
+         end if;
 
-         return False;
-      end Is_Future_Scope_Entity;
+      end Add_SPARK_Xref;
 
       ------------------------
       -- Is_SPARK_Reference --
@@ -411,440 +151,22 @@ package body SPARK_Specific is
       begin
          return Present (E)
            and then not Is_Generic_Unit (E)
-           and then (not Can_Be_Renamed or else No (Renamed_Entity (E)))
-           and then Get_Scope_Num (E) /= No_Scope;
+           and then (not Can_Be_Renamed or else No (Renamed_Entity (E)));
       end Is_SPARK_Scope;
 
-      --------
-      -- Lt --
-      --------
-
-      function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
-         T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
-         T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
-
-      begin
-         --  First test: if entity is in different unit, sort by unit. Note:
-         --  that we use Ent_Scope_File rather than Eun, as Eun may refer to
-         --  the file where the generic scope is defined, which may differ from
-         --  the file where the enclosing scope is defined. It is the latter
-         --  which matters for a correct order here.
-
-         if T1.Ent_Scope_File /= T2.Ent_Scope_File then
-            return Dependency_Num (T1.Ent_Scope_File) <
-                   Dependency_Num (T2.Ent_Scope_File);
-
-         --  Second test: within same unit, sort by location of the scope of
-         --  the entity definition.
-
-         elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
-               Get_Scope_Num (T2.Key.Ent_Scope)
-         then
-            return Get_Scope_Num (T1.Key.Ent_Scope) <
-                   Get_Scope_Num (T2.Key.Ent_Scope);
-
-         --  Third test: within same unit and scope, sort by location of
-         --  entity definition.
-
-         elsif T1.Def /= T2.Def then
-            return T1.Def < T2.Def;
-
-         else
-            --  Both entities must be equal at this point
-
-            pragma Assert (T1.Key.Ent = T2.Key.Ent);
-            pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
-            pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
-
-            --  Fourth test: if reference is in same unit as entity definition,
-            --  sort first.
-
-            if T1.Key.Lun /= T2.Key.Lun
-              and then T1.Ent_Scope_File = T1.Key.Lun
-            then
-               return True;
-
-            elsif T1.Key.Lun /= T2.Key.Lun
-              and then T2.Ent_Scope_File = T2.Key.Lun
-            then
-               return False;
-
-            --  Fifth test: if reference is in same unit and same scope as
-            --  entity definition, sort first.
-
-            elsif T1.Ent_Scope_File = T1.Key.Lun
-              and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
-              and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
-            then
-               return True;
-
-            elsif T2.Ent_Scope_File = T2.Key.Lun
-              and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
-              and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
-            then
-               return False;
-
-            --  Sixth test: for same entity, sort by reference location unit
-
-            elsif T1.Key.Lun /= T2.Key.Lun then
-               return Dependency_Num (T1.Key.Lun) <
-                      Dependency_Num (T2.Key.Lun);
-
-            --  Seventh test: for same entity, sort by reference location scope
-
-            elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
-                  Get_Scope_Num (T2.Key.Ref_Scope)
-            then
-               return Get_Scope_Num (T1.Key.Ref_Scope) <
-                      Get_Scope_Num (T2.Key.Ref_Scope);
-
-            --  Eighth test: order of location within referencing unit
-
-            elsif T1.Key.Loc /= T2.Key.Loc then
-               return T1.Key.Loc < T2.Key.Loc;
-
-            --  Finally, for two locations at the same address prefer the one
-            --  that does NOT have the type 'r', so that a modification or
-            --  extension takes preference, when there are more than one
-            --  reference at the same location. As a result, in the case of
-            --  entities that are in-out actuals, the read reference follows
-            --  the modify reference.
-
-            else
-               return T2.Key.Typ = 'r';
-            end if;
-         end if;
-      end Lt;
-
-      ----------
-      -- Move --
-      ----------
-
-      procedure Move (From : Natural; To : Natural) is
-      begin
-         Rnums (Nat (To)) := Rnums (Nat (From));
-      end Move;
-
-      -------------------
-      -- Set_Scope_Num --
-      -------------------
-
-      procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set;
-
-      ------------------------
-      -- Update_Scope_Range --
-      ------------------------
-
-      procedure Update_Scope_Range
-        (S    : Scope_Index;
-         From : Xref_Index;
-         To   : Xref_Index)
-      is
-      begin
-         SPARK_Scope_Table.Table (S).From_Xref := From;
-         SPARK_Scope_Table.Table (S).To_Xref := To;
-      end Update_Scope_Range;
-
-      --  Local variables
-
-      From_Index : Xref_Index;
-      Prev_Loc   : Source_Ptr;
-      Prev_Typ   : Character;
-      Ref_Count  : Nat;
-      Scope_Id   : Scope_Index;
-
    --  Start of processing for Add_SPARK_Xrefs
 
    begin
-      for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
-         declare
-            S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
-         begin
-            Set_Scope_Num (S.Entity, S.Scope_Num);
-         end;
-      end loop;
-
-      declare
-         Drefs_Table : Drefs.Table_Type
-                         renames Drefs.Table (Drefs.First .. Drefs.Last);
-      begin
-         Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
-         Nrefs := Nrefs + Drefs_Table'Length;
-      end;
-
-      --  Capture the definition Sloc values. As in the case of normal cross
-      --  references, we have to wait until now to get the correct value.
-
-      for Index in 1 .. Nrefs loop
-         Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
-      end loop;
-
-      --  Eliminate entries not appropriate for SPARK. Done prior to sorting
-      --  cross-references, as it discards useless references which do not have
-      --  a proper format for the comparison function (like no location).
-
-      Ref_Count := Nrefs;
-      Nrefs     := 0;
-
-      for Index in 1 .. Ref_Count loop
-         declare
-            Ref : Xref_Key renames Xrefs.Table (Index).Key;
-
-         begin
-            if SPARK_Entities (Ekind (Ref.Ent))
-              and then SPARK_References (Ref.Typ)
-              and then Is_SPARK_Scope (Ref.Ent_Scope)
-              and then Is_SPARK_Scope (Ref.Ref_Scope)
-              and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
-
-              --  Discard references from unknown scopes, e.g. generic scopes
-
-              and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
-              and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
-
-              --  Discard references to loop parameters introduced within
-              --  expression functions, as they give two references: one from
-              --  the analysis of the expression function itself and one from
-              --  the analysis of the expanded body. We don't lose any globals
-              --  by discarding them, because such loop parameters can only be
-              --  accessed locally from within the expression function body.
-              --  Note: some loop parameters are expanded into variables; they
-              --  also must be ignored.
-
-              and then not
-                (Ekind_In (Ref.Ent, E_Loop_Parameter, E_Variable)
-                  and then Scope_Within
-                             (Ref.Ent, Unique_Entity (Ref.Ref_Scope))
-                  and then Is_Expression_Function (Ref.Ref_Scope))
-            then
-               Nrefs         := Nrefs + 1;
-               Rnums (Nrefs) := Index;
-            end if;
-         end;
-      end loop;
-
-      --  Sort the references
-
-      Sorting.Sort (Integer (Nrefs));
-
-      --  Eliminate duplicate entries
-
-      --  We need this test for Ref_Count because if we force ALI file
-      --  generation in case of errors detected, it may be the case that
-      --  Nrefs is 0, so we should not reset it here.
-
-      if Nrefs >= 2 then
-         Ref_Count := Nrefs;
-         Nrefs     := 1;
-
-         for Index in 2 .. Ref_Count loop
-            if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
-               Nrefs := Nrefs + 1;
-               Rnums (Nrefs) := Rnums (Index);
-            end if;
-         end loop;
-      end if;
-
-      --  Eliminate the reference if it is at the same location as the previous
-      --  one, unless it is a read-reference indicating that the entity is an
-      --  in-out actual in a call.
-
-      Ref_Count := Nrefs;
-      Nrefs     := 0;
-      Prev_Loc  := No_Location;
-      Prev_Typ  := 'm';
-
-      for Index in 1 .. Ref_Count loop
-         declare
-            Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
-
-         begin
-            if Ref.Loc /= Prev_Loc
-              or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
-            then
-               Prev_Loc      := Ref.Loc;
-               Prev_Typ      := Ref.Typ;
-               Nrefs         := Nrefs + 1;
-               Rnums (Nrefs) := Rnums (Index);
-            end if;
-         end;
-      end loop;
-
-      --  The two steps have eliminated all references, nothing to do
-
-      if SPARK_Scope_Table.Last = 0 then
-         return;
-      end if;
-
-      Scope_Id   := 1;
-      From_Index := 1;
-
-      --  Loop to output references
+      --  Expose cross-references from private frontend tables to the backend
 
-      for Refno in 1 .. Nrefs loop
-         declare
-            Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
-            Ref       : Xref_Key   renames Ref_Entry.Key;
-
-         begin
-            --  If this assertion fails, the scope which we are looking for is
-            --  not in SPARK scope table, which reveals either a problem in the
-            --  construction of the scope table, or an erroneous scope for the
-            --  current cross-reference.
-
-            pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
-
-            --  Update the range of cross references to which the current scope
-            --  refers to. This may be the empty range only for the first scope
-            --  considered.
-
-            if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
-               Update_Scope_Range
-                 (S    => Scope_Id,
-                  From => From_Index,
-                  To   => SPARK_Xref_Table.Last);
-
-               From_Index := SPARK_Xref_Table.Last + 1;
-            end if;
-
-            while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
-               Scope_Id := Scope_Id + 1;
-               pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
-            end loop;
-
-            SPARK_Xref_Table.Append (
-              (Entity    => Unique_Entity (Ref.Ent),
-               Ref_Scope => Ref.Ref_Scope,
-               Rtype     => Ref.Typ));
-         end;
+      for Index in Drefs.First .. Drefs.Last loop
+         Add_SPARK_Xref (Index, Drefs.Table (Index));
       end loop;
 
-      --  Update the range of cross references to which the scope refers to
-
-      Update_Scope_Range
-        (S    => Scope_Id,
-         From => From_Index,
-         To   => SPARK_Xref_Table.Last);
-   end Add_SPARK_Xrefs;
-
-   -------------------------
-   -- Collect_SPARK_Xrefs --
-   -------------------------
-
-   procedure Collect_SPARK_Xrefs
-     (Sdep_Table : Unit_Ref_Table;
-      Num_Sdep   : Nat)
-   is
-      Sdep      : Pos;
-      Sdep_Next : Pos;
-      --  Index of the current and next source dependency
-
-      Sdep_File : Pos;
-      --  Index of the file to which the scopes need to be assigned; for
-      --  library-level instances of generic units this points to the unit
-      --  of the body, because this is where references are assigned to.
-
-      Ubody : Unit_Number_Type;
-      Uspec : Unit_Number_Type;
-      --  Unit numbers for the dependency spec and possibly its body (only in
-      --  the case of library-level instance of a generic package).
-
-   begin
-      --  Cross-references should have been computed first
-
-      pragma Assert (Xrefs.Last /= 0);
-
-      Initialize_SPARK_Tables;
-
-      --  Generate file and scope SPARK cross-reference information
-
-      Sdep := 1;
-      while Sdep <= Num_Sdep loop
-
-         --  Skip dependencies with no entity node, e.g. configuration files
-         --  with pragmas (.adc) or target description (.atp), since they
-         --  present no interest for SPARK cross references.
-
-         if No (Cunit_Entity (Sdep_Table (Sdep))) then
-            Sdep_Next := Sdep + 1;
-
-         --  For library-level instantiation of a generic, two consecutive
-         --  units refer to the same compilation unit node and entity (one to
-         --  body, one to spec). In that case, treat them as a single unit for
-         --  the sake of SPARK cross references by passing to Add_SPARK_File.
-
-         else
-            if Sdep < Num_Sdep
-              and then Cunit_Entity (Sdep_Table (Sdep)) =
-                       Cunit_Entity (Sdep_Table (Sdep + 1))
-            then
-               declare
-                  Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
-                  Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
-
-               begin
-                  --  Both Cunits point to compilation unit nodes
-
-                  pragma Assert
-                    (Nkind (Cunit1) = N_Compilation_Unit
-                      and then Nkind (Cunit2) = N_Compilation_Unit);
-
-                  --  Do not depend on the sorting order, which is based on
-                  --  Unit_Name, and for library-level instances of nested
-                  --  generic packages they are equal.
-
-                  --  If declaration comes before the body
-
-                  if Nkind (Unit (Cunit1)) = N_Package_Declaration
-                    and then Nkind (Unit (Cunit2)) = N_Package_Body
-                  then
-                     Uspec := Sdep_Table (Sdep);
-                     Ubody := Sdep_Table (Sdep + 1);
-
-                     Sdep_File := Sdep + 1;
-
-                  --  If body comes before declaration
-
-                  elsif Nkind (Unit (Cunit1)) = N_Package_Body
-                    and then Nkind (Unit (Cunit2)) = N_Package_Declaration
-                  then
-                     Uspec := Sdep_Table (Sdep + 1);
-                     Ubody := Sdep_Table (Sdep);
-
-                     Sdep_File := Sdep;
-
-                  --  Otherwise it is an error
-
-                  else
-                     raise Program_Error;
-                  end if;
-
-                  Sdep_Next := Sdep + 2;
-               end;
-
-            --  ??? otherwise?
-
-            else
-               Uspec := Sdep_Table (Sdep);
-               Ubody := No_Unit;
-
-               Sdep_File := Sdep;
-               Sdep_Next := Sdep + 1;
-            end if;
-
-            Add_SPARK_File
-              (Uspec => Uspec,
-               Ubody => Ubody,
-               Dspec => Sdep_File);
-         end if;
-
-         Sdep := Sdep_Next;
+      for Index in Xrefs.First .. Xrefs.Last loop
+         Add_SPARK_Xref (-Index, Xrefs.Table (Index));
       end loop;
-
-      --  Generate SPARK cross-reference information
-
-      Add_SPARK_Xrefs;
-   end Collect_SPARK_Xrefs;
+   end Iterate_SPARK_Xrefs;
 
    -------------------------------------
    -- Enclosing_Subprogram_Or_Package --
@@ -941,16 +263,6 @@ package body SPARK_Specific is
       return Context;
    end Enclosing_Subprogram_Or_Library_Package;
 
-   -----------------
-   -- Entity_Hash --
-   -----------------
-
-   function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
-   begin
-      return
-        Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
-   end Entity_Hash;
-
    --------------------------
    -- Generate_Dereference --
    --------------------------
@@ -1019,329 +331,4 @@ package body SPARK_Specific is
       end if;
    end Generate_Dereference;
 
-   -------------------------------
-   -- Traverse_Compilation_Unit --
-   -------------------------------
-
-   procedure Traverse_Compilation_Unit (CU : Node_Id) is
-      procedure Traverse_Block                      (N : Node_Id);
-      procedure Traverse_Declaration_Or_Statement   (N : Node_Id);
-      procedure Traverse_Declarations_And_HSS       (N : Node_Id);
-      procedure Traverse_Declarations_Or_Statements (L : List_Id);
-      procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
-      procedure Traverse_Package_Body               (N : Node_Id);
-      procedure Traverse_Visible_And_Private_Parts  (N : Node_Id);
-      procedure Traverse_Protected_Body             (N : Node_Id);
-      procedure Traverse_Subprogram_Body            (N : Node_Id);
-      procedure Traverse_Task_Body                  (N : Node_Id);
-
-      --  Traverse corresponding construct, calling Process on all declarations
-
-      --------------------
-      -- Traverse_Block --
-      --------------------
-
-      procedure Traverse_Block (N : Node_Id) renames
-        Traverse_Declarations_And_HSS;
-
-      ---------------------------------------
-      -- Traverse_Declaration_Or_Statement --
-      ---------------------------------------
-
-      procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
-         function Traverse_Stub (N : Node_Id) return Boolean;
-         --  Returns True iff stub N should be traversed
-
-         function Traverse_Stub (N : Node_Id) return Boolean is
-         begin
-            pragma Assert (Nkind_In (N, N_Package_Body_Stub,
-                                        N_Protected_Body_Stub,
-                                        N_Subprogram_Body_Stub,
-                                        N_Task_Body_Stub));
-
-            return Present (Library_Unit (N));
-         end Traverse_Stub;
-
-      --  Start of processing for Traverse_Declaration_Or_Statement
-
-      begin
-         case Nkind (N) is
-            when N_Package_Declaration =>
-               Traverse_Visible_And_Private_Parts (Specification (N));
-
-            when N_Package_Body =>
-               Traverse_Package_Body (N);
-
-            when N_Package_Body_Stub =>
-               if Traverse_Stub (N) then
-                  Traverse_Package_Body (Get_Body_From_Stub (N));
-               end if;
-
-            when N_Subprogram_Body =>
-               Traverse_Subprogram_Body (N);
-
-            when N_Entry_Body =>
-               Traverse_Subprogram_Body (N);
-
-            when N_Subprogram_Body_Stub =>
-               if Traverse_Stub (N) then
-                  Traverse_Subprogram_Body (Get_Body_From_Stub (N));
-               end if;
-
-            when N_Protected_Body =>
-               Traverse_Protected_Body (N);
-
-            when N_Protected_Body_Stub =>
-               if Traverse_Stub (N) then
-                  Traverse_Protected_Body (Get_Body_From_Stub (N));
-               end if;
-
-            when N_Protected_Type_Declaration =>
-               Traverse_Visible_And_Private_Parts (Protected_Definition (N));
-
-            when N_Task_Type_Declaration =>
-
-               --  Task type definition is optional (unlike protected type
-               --  definition, which is mandatory).
-
-               declare
-                  Task_Def : constant Node_Id := Task_Definition (N);
-               begin
-                  if Present (Task_Def) then
-                     Traverse_Visible_And_Private_Parts (Task_Def);
-                  end if;
-               end;
-
-            when N_Task_Body =>
-               Traverse_Task_Body (N);
-
-            when N_Task_Body_Stub =>
-               if Traverse_Stub (N) then
-                  Traverse_Task_Body (Get_Body_From_Stub (N));
-               end if;
-
-            when N_Block_Statement =>
-               Traverse_Block (N);
-
-            when N_If_Statement =>
-
-               --  Traverse the statements in the THEN part
-
-               Traverse_Declarations_Or_Statements (Then_Statements (N));
-
-               --  Loop through ELSIF parts if present
-
-               if Present (Elsif_Parts (N)) then
-                  declare
-                     Elif : Node_Id := First (Elsif_Parts (N));
-
-                  begin
-                     while Present (Elif) loop
-                        Traverse_Declarations_Or_Statements
-                          (Then_Statements (Elif));
-                        Next (Elif);
-                     end loop;
-                  end;
-               end if;
-
-               --  Finally traverse the ELSE statements if present
-
-               Traverse_Declarations_Or_Statements (Else_Statements (N));
-
-            when N_Case_Statement =>
-
-               --  Process case branches
-
-               declare
-                  Alt : Node_Id := First (Alternatives (N));
-               begin
-                  loop
-                     Traverse_Declarations_Or_Statements (Statements (Alt));
-                     Next (Alt);
-                     exit when No (Alt);
-                  end loop;
-               end;
-
-            when N_Extended_Return_Statement =>
-               Traverse_Handled_Statement_Sequence
-                 (Handled_Statement_Sequence (N));
-
-            when N_Loop_Statement =>
-               Traverse_Declarations_Or_Statements (Statements (N));
-
-               --  Generic declarations are ignored
-
-            when others =>
-               null;
-         end case;
-      end Traverse_Declaration_Or_Statement;
-
-      -----------------------------------
-      -- Traverse_Declarations_And_HSS --
-      -----------------------------------
-
-      procedure Traverse_Declarations_And_HSS (N : Node_Id) is
-      begin
-         Traverse_Declarations_Or_Statements (Declarations (N));
-         Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
-      end Traverse_Declarations_And_HSS;
-
-      -----------------------------------------
-      -- Traverse_Declarations_Or_Statements --
-      -----------------------------------------
-
-      procedure Traverse_Declarations_Or_Statements (L : List_Id) is
-         N : Node_Id;
-
-      begin
-         --  Loop through statements or declarations
-
-         N := First (L);
-         while Present (N) loop
-
-            --  Call Process on all declarations
-
-            if Nkind (N) in N_Declaration
-              or else Nkind (N) in N_Later_Decl_Item
-              or else Nkind (N) = N_Entry_Body
-            then
-               if Nkind (N) in N_Body_Stub then
-                  Process (Get_Body_From_Stub (N));
-               else
-                  Process (N);
-               end if;
-            end if;
-
-            Traverse_Declaration_Or_Statement (N);
-
-            Next (N);
-         end loop;
-      end Traverse_Declarations_Or_Statements;
-
-      -----------------------------------------
-      -- Traverse_Handled_Statement_Sequence --
-      -----------------------------------------
-
-      procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
-         Handler : Node_Id;
-
-      begin
-         if Present (N) then
-            Traverse_Declarations_Or_Statements (Statements (N));
-
-            if Present (Exception_Handlers (N)) then
-               Handler := First (Exception_Handlers (N));
-               while Present (Handler) loop
-                  Traverse_Declarations_Or_Statements (Statements (Handler));
-                  Next (Handler);
-               end loop;
-            end if;
-         end if;
-      end Traverse_Handled_Statement_Sequence;
-
-      ---------------------------
-      -- Traverse_Package_Body --
-      ---------------------------
-
-      procedure Traverse_Package_Body (N : Node_Id) is
-         Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
-
-      begin
-         case Ekind (Spec_E) is
-            when E_Package =>
-               Traverse_Declarations_And_HSS (N);
-
-            when E_Generic_Package =>
-               null;
-
-            when others =>
-               raise Program_Error;
-         end case;
-      end Traverse_Package_Body;
-
-      -----------------------------
-      -- Traverse_Protected_Body --
-      -----------------------------
-
-      procedure Traverse_Protected_Body (N : Node_Id) is
-      begin
-         Traverse_Declarations_Or_Statements (Declarations (N));
-      end Traverse_Protected_Body;
-
-      ------------------------------
-      -- Traverse_Subprogram_Body --
-      ------------------------------
-
-      procedure Traverse_Subprogram_Body (N : Node_Id) is
-         Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
-
-      begin
-         case Ekind (Spec_E) is
-            when Entry_Kind
-               | E_Function
-               | E_Procedure
-            =>
-               Traverse_Declarations_And_HSS (N);
-
-            when Generic_Subprogram_Kind =>
-               null;
-
-            when others =>
-               raise Program_Error;
-         end case;
-      end Traverse_Subprogram_Body;
-
-      ------------------------
-      -- Traverse_Task_Body --
-      ------------------------
-
-      procedure Traverse_Task_Body (N : Node_Id) renames
-        Traverse_Declarations_And_HSS;
-
-      ----------------------------------------
-      -- Traverse_Visible_And_Private_Parts --
-      ----------------------------------------
-
-      procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
-      begin
-         Traverse_Declarations_Or_Statements (Visible_Declarations (N));
-         Traverse_Declarations_Or_Statements (Private_Declarations (N));
-      end Traverse_Visible_And_Private_Parts;
-
-      --  Local variables
-
-      Lu : Node_Id;
-
-   --  Start of processing for Traverse_Compilation_Unit
-
-   begin
-      --  Get Unit (checking case of subunit)
-
-      Lu := Unit (CU);
-
-      if Nkind (Lu) = N_Subunit then
-         Lu := Proper_Body (Lu);
-      end if;
-
-      --  Do not add scopes for generic units
-
-      if Nkind (Lu) = N_Package_Body
-        and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
-      then
-         return;
-      end if;
-
-      --  Call Process on all declarations
-
-      if Nkind (Lu) in N_Declaration
-        or else Nkind (Lu) in N_Later_Decl_Item
-      then
-         Process (Lu);
-      end if;
-
-      --  Traverse the unit
-
-      Traverse_Declaration_Or_Statement (Lu);
-   end Traverse_Compilation_Unit;
-
 end SPARK_Specific;