Patchwork [Ada] Restriction SPARK replaced by SPARK_05

login
register
mail settings
Submitter Arnaud Charlet
Date July 8, 2013, 8 a.m.
Message ID <20130708080002.GA29878@adacore.com>
Download mbox | patch
Permalink /patch/257484/
State New
Headers show

Comments

Arnaud Charlet - July 8, 2013, 8 a.m.
The restriction SPARK is replaced by SPARK_05 (since this restriction
is specifically about violating rules of SPARK 2005). The restriction
SPARK is retained for backward compatibility, but will generate a
warning that it is obsolescent if it is used.

The following program compiles giving the expected violation msg:

     1. pragma Restrictions (SPARK_05);
     2. procedure SparkRes2 (X : Integer) is
     3.    subtype R is Integer range 1 .. X;
                                      |
        >>> violation of restriction "SPARK_05" at line 1
        >>>  range should be static

     4. begin
     5.    null;
     6. end SparkRes2;

and this program compiles showing the additional warning from using
the obsolete form:

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

     2. procedure SparkRes1 (X : Integer) is
     3.    subtype R is Integer range 1 .. X;
                                      |
        >>> violation of restriction "SPARK_05" at line 1
        >>>  range should be static

     4. begin
     5.    null;
     6. end SparkRes1;

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

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

	* gnat_rm.texi: Document SPARK_05 (replaces SPARK) Document
	obsolete recognition of SPARK Document all other obsolete synonyms
	for old restrictions.
	* restrict.adb (Check_SPARK_Restriction): SPARK_05 replaces
	SPARK (Process_Restriction_Synonyms): Handle SPARK as synonym
	for SPARK_05.
	* restrict.ads: Restriction SPARK_05 replaces SPARK.
	* s-rident.ads: Replace restriction SPARK by SPARK_05 Add SPARK
	as synonym for SPARK_05.
	* sem_prag.adb: Minor reformatting.
	* snames.ads-tmpl: Add entries for Name_SPARK and Name_SPARK_05.

Patch

Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 200762)
+++ gnat_rm.texi	(working copy)
@@ -454,7 +454,7 @@ 
 * No_Implicit_Aliasing::
 * No_Obsolescent_Features::
 * No_Wide_Characters::
-* SPARK::
+* SPARK_05::
 
 The Implementation of Standard I/O
 
@@ -8951,6 +8951,12 @@ 
 restriction results in the raising of Program_Error exception at the point of
 the call.
 
+@findex Max_Entry_Queue_Depth
+The restriction @code{Max_Entry_Queue_Depth} is recognized as a
+synonym for @code{Max_Entry_Queue_Length}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node Max_Protected_Entries
 @unnumberedsubsec Max_Protected_Entries
 @findex Max_Protected_Entries
@@ -9137,6 +9143,12 @@ 
 (Is_Reserved, Is_Attached, Current_Handler, Attach_Handler, Exchange_Handler,
 Detach_Handler, and Reference).
 
+@findex No_Dynamic_Interrupts
+The restriction @code{No_Dynamic_Interrupts} is recognized as a
+synonym for @code{No_Dynamic_Attachment}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node No_Dynamic_Priorities
 @unnumberedsubsec No_Dynamic_Priorities
 @findex No_Dynamic_Priorities
@@ -9378,6 +9390,12 @@ 
 are permitted and prevents keyword @code{requeue} from being used in source
 code.
 
+@findex No_Requeue
+The restriction @code{No_Requeue} is recognized as a
+synonym for @code{No_Requeue_Statements}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on oNobsolescent features are activated).
+
 @node No_Secondary_Stack
 @unnumberedsubsec No_Secondary_Stack
 @findex No_Secondary_Stack
@@ -9459,6 +9477,12 @@ 
 [GNAT] This restriction ensures at compile time that there are no implicit or
 explicit dependencies on the package @code{Ada.Task_Attributes}.
 
+@findex No_Task_Attributes
+The restriction @code{No_Task_Attributes} is recognized as a synonym
+for @code{No_Task_Attributes_Package}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node No_Task_Hierarchy
 @unnumberedsubsec No_Task_Hierarchy
 @findex No_Task_Hierarchy
@@ -9498,6 +9522,12 @@ 
 expressions or references to simple boolean variables defined in the private
 part of the protected type.  No other form of entry barriers is permitted.
 
+@findex Boolean_Entry_Barriers
+The restriction @code{Boolean_Entry_Barriers} is recognized as a
+synonym for @code{Simple_Barriers}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node Static_Priorities
 @unnumberedsubsec Static_Priorities
 @findex Static_Priorities
@@ -9533,7 +9563,7 @@ 
 * No_Implicit_Aliasing::
 * No_Obsolescent_Features::
 * No_Wide_Characters::
-* SPARK::
+* SPARK_05::
 @end menu
 
 @node No_Elaboration_Code
@@ -9663,13 +9693,19 @@ 
 appear in the program (that is literals representing characters not in
 type @code{Character}).
 
-@node SPARK
-@unnumberedsubsec SPARK
-@findex SPARK
+@node SPARK_05
+@unnumberedsubsec SPARK_05
+@findex SPARK_05
 [GNAT] This restriction checks at compile time that some constructs
 forbidden in SPARK 2005 are not present. Error messages related to
 SPARK restriction have the form:
 
+@findex SPARK
+The restriction @code{SPARK} is recognized as a
+synonym for @code{SPARK_05}. This is retained for historical
+compatibility purposes (and an unconditional warning will be generated
+for its use, advising replacement by @code{SPARK}.
+
 @smallexample
 violation of restriction "SPARK" at <file>
  <error message>
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200753)
+++ sem_prag.adb	(working copy)
@@ -7016,7 +7016,7 @@ 
       --  Start of processing for Process_Restrictions_Or_Restriction_Warnings
 
       begin
-         --  Ignore all Restrictions pragma in CodePeer mode
+         --  Ignore all Restrictions pragmas in CodePeer mode
 
          if CodePeer_Mode then
             return;
Index: restrict.adb
===================================================================
--- restrict.adb	(revision 200688)
+++ restrict.adb	(working copy)
@@ -166,7 +166,7 @@ 
    begin
       if Force or else Comes_From_Source (Original_Node (N)) then
 
-         if Restriction_Check_Required (SPARK)
+         if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
             return;
@@ -177,7 +177,7 @@ 
          --  restore the previous value of the global variable around the call.
 
          Save_Error_Msg_Sloc := Error_Msg_Sloc;
-         Check_Restriction (Msg_Issued, SPARK, First_Node (N));
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
          Error_Msg_Sloc := Save_Error_Msg_Sloc;
 
          if Msg_Issued then
@@ -194,7 +194,7 @@ 
 
       if Comes_From_Source (Original_Node (N)) then
 
-         if Restriction_Check_Required (SPARK)
+         if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
             return;
@@ -205,7 +205,7 @@ 
          --  restore the previous value of the global variable around the call.
 
          Save_Error_Msg_Sloc := Error_Msg_Sloc;
-         Check_Restriction (Msg_Issued, SPARK, First_Node (N));
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
          Error_Msg_Sloc := Save_Error_Msg_Sloc;
 
          if Msg_Issued then
@@ -880,10 +880,22 @@ 
          when Name_No_Task_Attributes =>
             New_Name := Name_No_Task_Attributes_Package;
 
+         --  SPARK is special in that we unconditionally warn
+
+         when Name_SPARK =>
+            Error_Msg_Name_1 := Name_SPARK;
+            Error_Msg_N ("restriction identifier % is obsolescent??", N);
+            Error_Msg_Name_1 := Name_SPARK_05;
+            Error_Msg_N ("|use restriction identifier % instead??", N);
+            return Name_SPARK_05;
+
          when others =>
             return Old_Name;
       end case;
 
+      --  Output warning if we are warning on obsolescent features for all
+      --  cases other than SPARK.
+
       if Warn_On_Obsolescent_Feature then
          Error_Msg_Name_1 := Old_Name;
          Error_Msg_N ("restriction identifier % is obsolescent?j?", N);
@@ -983,10 +995,10 @@ 
 
       procedure Id_Case (S : String; Quotes : Boolean := True);
       --  Given a string S, case it according to current identifier casing,
-      --  except for SPARK (an acronym) which is set all upper case, and store
-      --  in Error_Msg_String. Then append `~` to the message buffer to output
-      --  the string unchanged surrounded in quotes. The quotes are suppressed
-      --  if Quotes = False.
+      --  except for SPARK_05 (an acronym) which is set all upper case, and
+      --  store in Error_Msg_String. Then append `~` to the message buffer
+      --  to output the string unchanged surrounded in quotes. The quotes
+      --  are suppressed if Quotes = False.
 
       --------------
       -- Add_Char --
@@ -1017,7 +1029,7 @@ 
          Name_Buffer (1 .. S'Last) := S;
          Name_Len := S'Length;
 
-         if R = SPARK then
+         if R = SPARK_05 then
             Set_All_Upper_Case;
          else
             Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
Index: restrict.ads
===================================================================
--- restrict.ads	(revision 200695)
+++ restrict.ads	(working copy)
@@ -142,7 +142,7 @@ 
       No_Wide_Characters                 => True,
       Static_Priorities                  => True,
       Static_Storage_Size                => True,
-      SPARK                              => True,
+      SPARK_05                           => True,
       others                             => False);
 
    --  The following table records entries made by Restrictions pragmas
@@ -180,7 +180,7 @@ 
    -- SPARK Restriction Control --
    -------------------------------
 
-   --  SPARK HIDE directives allow the effect of the SPARK restriction to be
+   --  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.
 
@@ -282,10 +282,10 @@ 
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False);
-   --  Node N represents a construct not allowed in formal mode. If this is a
-   --  source node, or if the restriction is forced (Force = True), and the
-   --  SPARK restriction is set, then an error is issued on N. Msg is appended
-   --  to the restriction failure message.
+   --  Node N represents a construct not allowed in formal mode. If this is
+   --  a source node, or if the restriction is forced (Force = True), and
+   --  the SPARK_05 restriction is set, then an error is issued on N. Msg
+   --  is appended to the restriction failure message.
 
    procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id);
    --  Same as Check_SPARK_Restriction except there is a continuation message
Index: s-rident.ads
===================================================================
--- s-rident.ads	(revision 200688)
+++ s-rident.ads	(working copy)
@@ -175,7 +175,7 @@ 
       No_Elaboration_Code,                       -- GNAT
       No_Obsolescent_Features,                   -- Ada 2005 AI-368
       No_Wide_Characters,                        -- GNAT
-      SPARK,                                     -- GNAT
+      SPARK_05,                                  -- GNAT
 
       --  The following cases require a parameter value
 
@@ -223,13 +223,14 @@ 
    No_Dynamic_Interrupts  : Restriction_Id renames No_Dynamic_Attachment;
    No_Requeue             : Restriction_Id renames No_Requeue_Statements;
    No_Task_Attributes     : Restriction_Id renames No_Task_Attributes_Package;
+   SPARK                  : Restriction_Id renames SPARK_05;
 
    subtype All_Restrictions is Restriction_Id range
      Simple_Barriers .. Max_Storage_At_Blocking;
    --  All restrictions (excluding only Not_A_Restriction_Id)
 
    subtype All_Boolean_Restrictions is Restriction_Id range
-     Simple_Barriers .. SPARK;
+     Simple_Barriers .. SPARK_05;
    --  All restrictions which do not take a parameter
 
    subtype Partition_Boolean_Restrictions is All_Boolean_Restrictions range
@@ -240,7 +241,7 @@ 
    --  case of Boolean restrictions.
 
    subtype Cunit_Boolean_Restrictions is All_Boolean_Restrictions range
-     Immediate_Reclamation .. SPARK;
+     Immediate_Reclamation .. SPARK_05;
    --  Boolean restrictions that are not checked for partition consistency
    --  and that thus apply only to the current unit. Note that for these
    --  restrictions, the compiler does not apply restrictions found in
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 200711)
+++ snames.ads-tmpl	(working copy)
@@ -762,6 +762,8 @@ 
    Name_Semaphore                      : constant Name_Id := N + $;
    Name_Short_Descriptor               : constant Name_Id := N + $;
    Name_Simple_Barriers                : constant Name_Id := N + $;
+   Name_SPARK                          : constant Name_Id := N + $;
+   Name_SPARK_05                       : constant Name_Id := N + $;
    Name_Spec_File_Name                 : constant Name_Id := N + $;
    Name_State                          : constant Name_Id := N + $;
    Name_Statement_Assertions           : constant Name_Id := N + $;