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, 4 insertions, 114 deletions

diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index df1d8e89..25af902 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -23,48 +23,13 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package defines tables used to store information needed for the SPARK
---  mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
---  SPARK-specific cross-reference information.
+--  This package defines data structures used to expose frontend
+--  cross-references to the SPARK backend.
 
-with Table;
 with Types; use Types;
 
 package SPARK_Xrefs is
 
-   --  SPARK cross-reference information is stored internally using three
-   --  tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which
-   --  are defined in this unit.
-
-   --  Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
-   --  cross-reference information from the complete set of cross-references
-   --  generated during compilation.
-
-   --  -------------------------------
-   --  -- Generated Globals Section --
-   --  -------------------------------
-
-   --  The Generated Globals section is located at the end of the ALI file
-
-   --  All lines with information related to the Generated Globals begin with
-   --  string "GG". This string should therefore not be used in the beginning
-   --  of any line not related to Generated Globals.
-
-   --  The processing (reading and writing) of this section happens in package
-   --  Flow_Generated_Globals (from the SPARK 2014 sources), for further
-   --  information please refer there.
-
-   ----------------
-   -- Xref Table --
-   ----------------
-
-   --  The following table records SPARK cross-references
-
-   type Xref_Index is new Nat;
-   --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed; value 0 is used temporarily
-   --  until a proper value is determined.
-
    type SPARK_Xref_Record is record
       Entity : Entity_Id;
       --  Referenced entity
@@ -78,80 +43,8 @@ package SPARK_Xrefs is
       --    m = modification
       --    s = call
    end record;
-
-   package SPARK_Xref_Table is new Table.Table (
-     Table_Component_Type => SPARK_Xref_Record,
-     Table_Index_Type     => Xref_Index,
-     Table_Low_Bound      => 1,
-     Table_Initial        => 2000,
-     Table_Increment      => 300,
-     Table_Name           => "Xref_Table");
-
-   -----------------
-   -- Scope Table --
-   -----------------
-
-   --  This table keeps track of the scopes and the corresponding starting and
-   --  ending indexes (From, To) in the Xref table.
-
-   type Scope_Index is new Nat;
-   --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed; value 0 indicates that no
-   --  entries have been constructed and is also used until a proper value is
-   --  determined.
-
-   type SPARK_Scope_Record is record
-      Entity : Entity_Id;
-      --  Entity that is represented by the scope
-
-      Scope_Num : Pos;
-      --  Set to the scope number within the enclosing unit
-
-      From_Xref : Xref_Index;
-      --  Starting index in Xref table for this scope
-
-      To_Xref : Xref_Index;
-      --  Ending index in Xref table for this scope
-   end record;
-
-   package SPARK_Scope_Table is new Table.Table (
-     Table_Component_Type => SPARK_Scope_Record,
-     Table_Index_Type     => Scope_Index,
-     Table_Low_Bound      => 1,
-     Table_Initial        => 200,
-     Table_Increment      => 300,
-     Table_Name           => "Scope_Table");
-
-   ----------------
-   -- File Table --
-   ----------------
-
-   --  This table keeps track of the units and the corresponding starting and
-   --  ending indexes (From, To) in the Scope table.
-
-   type File_Index is new Nat;
-   --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed; value 0 indicates that no
-   --  entries have been constructed.
-
-   type SPARK_File_Record is record
-      File_Num : Nat;
-      --  Dependency number in ALI file
-
-      From_Scope : Scope_Index;
-      --  Starting index in Scope table for this unit
-
-      To_Scope : Scope_Index;
-      --  Ending index in Scope table for this unit
-   end record;
-
-   package SPARK_File_Table is new Table.Table (
-     Table_Component_Type => SPARK_File_Record,
-     Table_Index_Type     => File_Index,
-     Table_Low_Bound      => 1,
-     Table_Initial        => 20,
-     Table_Increment      => 200,
-     Table_Name           => "File_Table");
+   --  This type holds a subset of the frontend xref entry that is needed by
+   --  the SPARK backend.
 
    ---------------
    -- Constants --
@@ -170,9 +63,6 @@ package SPARK_Xrefs is
    -- Subprograms --
    -----------------
 
-   procedure Initialize_SPARK_Tables;
-   --  Reset tables for a new compilation
-
    procedure dspark;
    --  Debug routine to dump internal SPARK cross-reference tables. This is a
    --  raw format dump showing exactly what the tables contain.