diff mbox

[Ada] Make sure hides works with SPARK and SPARK_05

Message ID 20130708080320.GA13891@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet July 8, 2013, 8:03 a.m. UTC 
This is a followup patch that ensures that the hides directives
work with both SPARK_05 and the obsolete synonym SPARK (the latter
was broken by the previous patch).

The following programs compile as shown:

     1. pragma Restrictions (SPARK);
                             |
        >>> warning: restriction identifier "Spark" is obsolescent
        >>> warning: use restriction identifier "Spark_05" instead

     2. procedure SparkRes1a (X : Integer) is
     3.    --# hide SparkRes1a
     4.    subtype R is Integer range 1 .. X;
     5. begin
     6.    null;
     7. end SparkRes1a;

     1. pragma Restrictions (SPARK_05);
     2. procedure SparkRes2a (X : Integer) is
     3. --# hide SparkRes2a;
     4.    subtype R is Integer range 1 .. X;
     5. begin
     6.    null;
     7. end SparkRes2a;

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 200705)
+++ sem_ch3.adb	(working copy)
@@ -2077,7 +2077,7 @@ 
    --  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 @@ 
 
            --  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
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 200688)
+++ sem_ch5.adb	(working copy)
@@ -2867,7 +2867,7 @@ 
             --  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 @@ 
 
                   --  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
Index: scng.adb
===================================================================
--- scng.adb	(revision 200688)
+++ scng.adb	(working copy)
@@ -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 @@ 
                --  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
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 200756)
+++ sem_util.adb	(working copy)
@@ -4582,7 +4582,7 @@ 
       --  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 @@ 
          --  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;
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 200688)
+++ sem_res.adb	(working copy)
@@ -7028,7 +7028,7 @@ 
             --  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 @@ 
             --  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 @@ 
       --  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 @@ 
       --  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
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 200761)
+++ sem_ch4.adb	(working copy)
@@ -991,7 +991,7 @@ 
    --  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;
 
Index: restrict.adb
===================================================================
--- restrict.adb	(revision 200763)
+++ restrict.adb	(working copy)
@@ -41,6 +41,38 @@ 
 
 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 @@ 
    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 @@ 
    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
Index: restrict.ads
===================================================================
--- restrict.ads	(revision 200763)
+++ restrict.ads	(working copy)
@@ -176,34 +176,6 @@ 
      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 @@ 
    --  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;
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 200711)
+++ par-prag.adb	(working copy)
@@ -235,15 +235,15 @@ 
          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 =>
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb	(revision 200760)
+++ sem_ch8.adb	(working copy)
@@ -5882,7 +5882,7 @@ 
       --  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 @@ 
          --  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
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 200763)
+++ snames.ads-tmpl	(working copy)
@@ -733,6 +733,7 @@ 
    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 + $;