[Ada] Remove AUTO mode for SPARK_Mode pragma
Arnaud Charlet
charlet@adacore.com
Mon Jan 27 16:40:00 GMT 2014
The latest SPARK spec removes AUTO as a possibility for the
SPARK_Mode pragma. The message for inconsistent SPARK modes
is also simplified, since the only case to worry about now
is trying to turn it ON when it is OFF. The following test
is compiled with -gnatj60:
1. pragma SPARK_Mode (Auto);
|
>>> argument for pragma "Spark_Mode" must be "On"
or "Off"
2. pragma SPARK_Mode (Off);
3. procedure NoAutoSM is
4. pragma SPARK_Mode (On);
|
>>> cannot change SPARK_Mode from Off to On,
SPARK_Mode was set to Off at line 2
5. begin
6. null;
7. end;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-27 Robert Dewar <dewar@adacore.com>
* opt.adb (SPARK_Mode): Default for library units is None rather
than Off.
* opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is
no longer ordered.
* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO
possibility.
* snames.ads-tmpl (Name_Auto): Removed, no longer used.
-------------- next part --------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207138)
+++ sem_prag.adb (working copy)
@@ -18587,7 +18587,7 @@
-- SPARK_Mode --
----------------
- -- pragma SPARK_Mode [(On | Off | Auto)];
+ -- pragma SPARK_Mode [(On | Off)];
when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
Body_Id : Entity_Id;
@@ -18609,9 +18609,6 @@
procedure Check_Library_Level_Entity (E : Entity_Id);
-- Verify that pragma is applied to library-level entity E
- function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
- -- Convert a value of type SPARK_Mode_Type to corresponding name
-
------------------------------
-- Check_Pragma_Conformance --
------------------------------
@@ -18623,15 +18620,13 @@
-- New mode less restrictive than the established mode
- if Get_SPARK_Mode_From_Pragma (Old_Pragma) < Mode_Id then
- Error_Msg_Name_1 := Mode;
- Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1);
-
- Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode);
- Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+ if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off
+ and then Mode_Id = On
+ then
Error_Msg_N
- ("\mode is less restrictive than mode "
- & "% defined #", Arg1);
+ ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1);
+ Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+ Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1);
raise Pragma_Exit;
end if;
end if;
@@ -18665,28 +18660,6 @@
end if;
end Check_Library_Level_Entity;
- -------------------------
- -- Get_SPARK_Mode_Name --
- -------------------------
-
- function Get_SPARK_Mode_Name
- (Id : SPARK_Mode_Type) return Name_Id
- is
- begin
- if Id = On then
- return Name_On;
- elsif Id = Off then
- return Name_Off;
- elsif Id = Auto then
- return Name_Auto;
-
- -- Mode "None" should never be used in error message generation
-
- else
- raise Program_Error;
- end if;
- end Get_SPARK_Mode_Name;
-
-- Start of processing for Do_SPARK_Mode
begin
@@ -18697,7 +18670,7 @@
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
- Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
+ Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
Mode := Chars (Get_Pragma_Arg (Arg1));
else
Mode := Name_On;
@@ -18732,14 +18705,6 @@
-- The pragma applies to a [library unit] subprogram or package
else
- -- Mode "Auto" can only be used in a configuration pragma
-
- if Mode_Id = Auto then
- Error_Pragma_Arg
- ("mode `Auto` is only allowed when pragma % appears as "
- & "a configuration pragma", Arg1);
- end if;
-
-- Verify the placement of the pragma with respect to package
-- or subprogram declarations and detect duplicates.
@@ -23513,8 +23478,6 @@
return On;
elsif N = Name_Off then
return Off;
- elsif N = Name_Auto then
- return Auto;
-- Any other argument is erroneous
Index: opt.adb
===================================================================
--- opt.adb (revision 207120)
+++ opt.adb (working copy)
@@ -186,7 +186,7 @@
Assertions_Enabled := False;
Assume_No_Invalid_Values := False;
Check_Policy_List := Empty;
- SPARK_Mode := Off;
+ SPARK_Mode := None;
SPARK_Mode_Pragma := Empty;
end if;
Index: opt.ads
===================================================================
--- opt.ads (revision 207120)
+++ opt.ads (working copy)
@@ -1264,9 +1264,9 @@
-- GNAT
-- Set True if a pragma Short_Descriptors applies to the current unit.
- type SPARK_Mode_Type is (None, Off, Auto, On);
- pragma Ordered (SPARK_Mode_Type);
- -- Possible legal modes that can be set by aspect/pragma SPARK_Mode
+ type SPARK_Mode_Type is (None, Off, On);
+ -- Possible legal modes that can be set by aspect/pragma SPARK_Mode, as
+ -- well as the value None, which indicates no such pragma/aspect applies.
SPARK_Mode : SPARK_Mode_Type := None;
-- GNAT
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 207138)
+++ snames.ads-tmpl (working copy)
@@ -688,7 +688,6 @@
Name_Assertion : constant Name_Id := N + $;
Name_Assertions : constant Name_Id := N + $;
Name_Attribute_Name : constant Name_Id := N + $;
- Name_Auto : constant Name_Id := N + $;
Name_Body_File_Name : constant Name_Id := N + $;
Name_Boolean_Entry_Barriers : constant Name_Id := N + $;
Name_By_Any : constant Name_Id := N + $;
More information about the Gcc-patches
mailing list