[multiple changes]

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.

From-SVN: r200764

1 files changed, 34 insertions, 2 deletions

diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 7bd97b9..f78236a 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