2013-07-08 Robert Dewar <dewar@adacore.com>

	* par-prag.adb (Process_Restrictions_Or_Restriction_Warnings):
	Recognize SPARK_05 as synonym for SPARK in restrictions pragma.
	* restrict.ads, restrict.adb (SPARK_Hides): Table moved to body, only
	referenced there.
	* scng.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch8.adb,
	sem_res.adb, sem_util.adb: Use restriction SPARK_05 instead of SPARK.
	* snames.ads-tmpl (Name_No_Obsolescent_Features): New entry.

2013-07-08  Vincent Celier  <celier@adacore.com>

	* gnatcmd.adb (Check_Files): Use a response file for gnatls
	when possible.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@200764 138bc75d-0d04-0410-961f-82ee72b054a4

13 files changed, 82 insertions, 61 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 65e59773a1e..8810c253f81 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2013-07-08  Robert Dewar  <dewar@adacore.com>
+
+	* par-prag.adb (Process_Restrictions_Or_Restriction_Warnings):
+	Recognize SPARK_05 as synonym for SPARK in restrictions pragma.
+	* restrict.ads, restrict.adb (SPARK_Hides): Table moved to body, only
+	referenced there.
+	* scng.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch8.adb,
+	sem_res.adb, sem_util.adb: Use restriction SPARK_05 instead of SPARK.
+	* snames.ads-tmpl (Name_No_Obsolescent_Features): New entry.
+
+2013-07-08  Vincent Celier  <celier@adacore.com>
+
+	* gnatcmd.adb (Check_Files): Use a response file for gnatls
+	when possible.
+
 2013-07-08  Gary Dismukes  <dismukes@adacore.com>
 
 	* freeze.adb: Minor typo fixes.
diff --git a/gcc/ada/gnatcmd.adb b/gcc/ada/gnatcmd.adb
index be1567089af..d1ea2be3e04 100644
--- a/gcc/ada/gnatcmd.adb
+++ b/gcc/ada/gnatcmd.adb
@@ -418,6 +418,7 @@ procedure GNATCmd is
          if The_Command = Check  or else
             The_Command = Pretty or else
             The_Command = Metric or else
+            The_Command = List   or else
             The_Command = Stack
          then
             Tempdir.Create_Temp_File (FD, Temp_File_Name);
@@ -552,12 +553,10 @@ procedure GNATCmd is
                         end if;
 
                         if not Subunit then
-                           Last_Switches.Increment_Last;
-                           Last_Switches.Table (Last_Switches.Last) :=
-                             new String'
-                               (Get_Name_String
-                                    (Unit.File_Names
-                                         (Impl).Display_File));
+                           Add_To_Response_File
+                             (Get_Name_String
+                                (Unit.File_Names (Impl).Display_File),
+                              Check_File => False);
                         end if;
                      end if;
 
@@ -570,10 +569,10 @@ procedure GNATCmd is
                      if All_Projects or else
                         Unit.File_Names (Spec).Project = Project
                      then
-                        Last_Switches.Increment_Last;
-                        Last_Switches.Table (Last_Switches.Last) :=
-                          new String'(Get_Name_String
-                                       (Unit.File_Names (Spec).Display_File));
+                        Add_To_Response_File
+                          (Get_Name_String
+                             (Unit.File_Names (Spec).Display_File),
+                           Check_File => False);
                      end if;
                   end if;
 
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 07242fb4596..762f433ca89 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -235,15 +235,15 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is
          if Id = No_Name
            and then Nkind (Expr) = N_Identifier
          then
-            case Get_Restriction_Id (Chars (Expr)) is
-               when No_Obsolescent_Features =>
+            case  Chars (Expr) is
+               when Name_No_Obsolescent_Features =>
                   Set_Restriction (No_Obsolescent_Features, Pragma_Node);
                   Restriction_Warnings (No_Obsolescent_Features) :=
                     Prag_Id = Pragma_Restriction_Warnings;
 
-               when SPARK =>
-                  Set_Restriction (SPARK, Pragma_Node);
-                  Restriction_Warnings (SPARK) :=
+               when Name_SPARK | Name_SPARK_05 =>
+                  Set_Restriction (SPARK_05, Pragma_Node);
+                  Restriction_Warnings (SPARK_05) :=
                     Prag_Id = Pragma_Restriction_Warnings;
 
                when others =>
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 7bd97b95168..f78236a3645 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -41,6 +41,38 @@ with Uname;    use Uname;
 
 package body Restrict is
 
+   -------------------------------
+   -- SPARK Restriction Control --
+   -------------------------------
+
+   --  SPARK HIDE directives allow the effect of the SPARK_05 restriction to be
+   --  turned off for a specified region of code, and the following tables are
+   --  the data structures used to keep track of these regions.
+
+   --  The table contains pairs of source locations, the first being the start
+   --  location for hidden region, and the second being the end location.
+
+   --  Note that the start location is included in the hidden region, while
+   --  the end location is excluded from it. (It typically corresponds to the
+   --  next token during scanning.)
+
+   type SPARK_Hide_Entry is record
+      Start : Source_Ptr;
+      Stop  : Source_Ptr;
+   end record;
+
+   package SPARK_Hides is new Table.Table (
+     Table_Component_Type => SPARK_Hide_Entry,
+     Table_Index_Type     => Natural,
+     Table_Low_Bound      => 1,
+     Table_Initial        => 100,
+     Table_Increment      => 200,
+     Table_Name           => "SPARK Hides");
+
+   --------------------------------
+   -- Package Local Declarations --
+   --------------------------------
+
    Config_Cunit_Boolean_Restrictions : Save_Cunit_Boolean_Restrictions;
    --  Save compilation unit restrictions set by config pragma files
 
@@ -163,9 +195,9 @@ package body Restrict is
    is
       Msg_Issued          : Boolean;
       Save_Error_Msg_Sloc : Source_Ptr;
+
    begin
       if Force or else Comes_From_Source (Original_Node (N)) then
-
          if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
@@ -189,11 +221,11 @@ package body Restrict is
    procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
       Msg_Issued          : Boolean;
       Save_Error_Msg_Sloc : Source_Ptr;
+
    begin
       pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
 
       if Comes_From_Source (Original_Node (N)) then
-
          if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads
index 9c4b3b4dd33..7d6dcc1eb5d 100644
--- a/gcc/ada/restrict.ads
+++ b/gcc/ada/restrict.ads
@@ -176,34 +176,6 @@ package Restrict is
      Table_Increment      => 200,
      Table_Name           => "Name_No_Dependences");
 
-   -------------------------------
-   -- SPARK Restriction Control --
-   -------------------------------
-
-   --  SPARK HIDE directives allow the effect of the SPARK_05 restriction to be
-   --  turned off for a specified region of code, and the following tables are
-   --  the data structures used to keep track of these regions.
-
-   --  The table contains pairs of source locations, the first being the start
-   --  location for hidden region, and the second being the end location.
-
-   --  Note that the start location is included in the hidden region, while
-   --  the end location is excluded from it. (It typically corresponds to the
-   --  next token during scanning.)
-
-   type SPARK_Hide_Entry is record
-      Start : Source_Ptr;
-      Stop  : Source_Ptr;
-   end record;
-
-   package SPARK_Hides is new Table.Table (
-     Table_Component_Type => SPARK_Hide_Entry,
-     Table_Index_Type     => Natural,
-     Table_Low_Bound      => 1,
-     Table_Initial        => 100,
-     Table_Increment      => 200,
-     Table_Name           => "SPARK Hides");
-
    -----------------
    -- Subprograms --
    -----------------
@@ -380,7 +352,9 @@ package Restrict is
    --  restrictions are set.
 
    procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr);
-   --  Insert a new hidden region range in the SPARK hides table
+   --  Insert a new hidden region range in the SPARK hides table. The effect
+   --  is to hide any SPARK violation messages which are in the range Loc1 to
+   --  Loc2-1 (i.e. Loc2 is the first location for reenabling checks).
 
    procedure Set_Profile_Restrictions
      (P    : Profile_Name;
diff --git a/gcc/ada/scng.adb b/gcc/ada/scng.adb
index e27c91d14f2..e05d1d692ad 100644
--- a/gcc/ada/scng.adb
+++ b/gcc/ada/scng.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1796,7 +1796,7 @@ package body Scng is
                --  If the SPARK restriction is set for this unit, then generate
                --  a token Tok_SPARK_Hide for a SPARK HIDE directive.
 
-               if Restriction_Check_Required (SPARK)
+               if Restriction_Check_Required (SPARK_05)
                  and then Source (Start_Of_Comment) = '#'
                then
                   declare
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 7cbb9b92fee..f07f083463a 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2077,7 +2077,7 @@ package body Sem_Ch3 is
    --  Start of processing for Analyze_Declarations
 
    begin
-      if Restriction_Check_Required (SPARK) then
+      if Restriction_Check_Required (SPARK_05) then
          Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
       end if;
 
@@ -3242,7 +3242,7 @@ package body Sem_Ch3 is
 
            --  Only call test if needed
 
-           and then Restriction_Check_Required (SPARK)
+           and then Restriction_Check_Required (SPARK_05)
            and then not Is_SPARK_Initialization_Expr (E)
          then
             Check_SPARK_Restriction
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 530fd007f05..1459ec22f95 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -991,7 +991,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Call
 
    begin
-      if Restriction_Check_Required (SPARK) then
+      if Restriction_Check_Required (SPARK_05) then
          Check_Mixed_Parameter_And_Named_Associations;
       end if;
 
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 5b34ecc347b..2f8eced6fc9 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2867,7 +2867,7 @@ package body Sem_Ch5 is
             --  we are in formal mode where goto statements are not allowed.
 
             if Nkind (Nxt) = N_Label
-              and then not Restriction_Check_Required (SPARK)
+              and then not Restriction_Check_Required (SPARK_05)
             then
                return;
 
@@ -2924,7 +2924,7 @@ package body Sem_Ch5 is
 
                   --  Now issue the warning (or error in formal mode)
 
-                  if Restriction_Check_Required (SPARK) then
+                  if Restriction_Check_Required (SPARK_05) then
                      Check_SPARK_Restriction
                        ("unreachable code is not allowed", Error_Node);
                   else
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index e9505d680f5..27ccc2d3d1e 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -5882,7 +5882,7 @@ package body Sem_Ch8 is
       --  Selector name cannot be a character literal or an operator symbol in
       --  SPARK, except for the operator symbol in a renaming.
 
-      if Restriction_Check_Required (SPARK) then
+      if Restriction_Check_Required (SPARK_05) then
          if Nkind (Selector_Name (N)) = N_Character_Literal then
             Check_SPARK_Restriction
               ("character literal cannot be prefixed", N);
@@ -6222,7 +6222,7 @@ package body Sem_Ch8 is
          --  Selector name is restricted in SPARK
 
          if Nkind (N) = N_Expanded_Name
-           and then Restriction_Check_Required (SPARK)
+           and then Restriction_Check_Required (SPARK_05)
          then
             if Is_Subprogram (P_Name) then
                Check_SPARK_Restriction
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index b4a654a24cc..95cc437224c 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7028,7 +7028,7 @@ package body Sem_Res is
             --  Protect call to Matching_Static_Array_Bounds to avoid costly
             --  operation if not needed.
 
-            if Restriction_Check_Required (SPARK)
+            if Restriction_Check_Required (SPARK_05)
               and then Base_Type (T) /= Standard_String
               and then Base_Type (Etype (L)) = Base_Type (Etype (R))
               and then Etype (L) /= Any_Composite  --  or else L in error
@@ -7738,7 +7738,7 @@ package body Sem_Res is
             --  Protect call to Matching_Static_Array_Bounds to avoid costly
             --  operation if not needed.
 
-            if Restriction_Check_Required (SPARK)
+            if Restriction_Check_Required (SPARK_05)
               and then Base_Type (Left_Typ) = Base_Type (Right_Typ)
               and then Left_Typ /= Any_Composite  --  or Left_Opnd in error
               and then Right_Typ /= Any_Composite  --  or Right_Opnd in error
@@ -8483,7 +8483,7 @@ package body Sem_Res is
       --  Protect call to Matching_Static_Array_Bounds to avoid costly
       --  operation if not needed.
 
-      if Restriction_Check_Required (SPARK)
+      if Restriction_Check_Required (SPARK_05)
         and then Is_Array_Type (Target_Typ)
         and then Is_Array_Type (Etype (Expr))
         and then Etype (Expr) /= Any_Composite  --  or else Expr in error
@@ -9625,7 +9625,7 @@ package body Sem_Res is
       --  Protect call to Matching_Static_Array_Bounds to avoid costly
       --  operation if not needed.
 
-      if Restriction_Check_Required (SPARK)
+      if Restriction_Check_Required (SPARK_05)
         and then Is_Array_Type (Target_Typ)
         and then Is_Array_Type (Operand_Typ)
         and then Operand_Typ /= Any_Composite  --  or else Operand in error
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 623d3c4f8e8..dcad44f1bba 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4582,7 +4582,7 @@ package body Sem_Util is
       --  Declaring a homonym is not allowed in SPARK ...
 
       if Present (C)
-        and then Restriction_Check_Required (SPARK)
+        and then Restriction_Check_Required (SPARK_05)
       then
          declare
             Enclosing_Subp : constant Node_Id := Enclosing_Subprogram (Def_Id);
@@ -12982,7 +12982,7 @@ package body Sem_Util is
          --  subprogram bodies. Detect those cases by testing whether
          --  Process_End_Label was called for a body (Typ = 't') or a package.
 
-         if Restriction_Check_Required (SPARK)
+         if Restriction_Check_Required (SPARK_05)
            and then (Typ = 't' or else Ekind (Ent) = E_Package)
          then
             Error_Msg_Node_1 := Endl;
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 2f8057698e5..40823d43331 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -733,6 +733,7 @@ package Snames is
    Name_No_Dynamic_Attachment          : constant Name_Id := N + $;
    Name_No_Dynamic_Interrupts          : constant Name_Id := N + $;
    Name_No_Implementation_Extensions   : constant Name_Id := N + $;
+   Name_No_Obsolescent_Features        : constant Name_Id := N + $;
    Name_No_Requeue                     : constant Name_Id := N + $;
    Name_No_Requeue_Statements          : constant Name_Id := N + $;
    Name_No_Specification_Of_Aspect     : constant Name_Id := N + $;