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 <de...@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.
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 + $;
