diff mbox series

[Ada] Accept explicit SPARK_Mode Auto as configuration pragma

Message ID 20220912081935.GA1513026@poulhies-Precision-5550
State New, archived
Headers
Series [Ada] Accept explicit SPARK_Mode Auto as configuration pragma |

Commit Message

Marc Poulhiès Sept. 12, 2022, 8:19 a.m. UTC 
  An explicit value of Auto is now accepted for a configuration pragma
SPARK_Mode, as a way to exempt a unit from complete adherence to
SPARK rules when using a global configuration pragma file where
SPARK_Mode=>On is specified.

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

gcc/ada/

	* sem_prag.adb (Analyze_Pragma): Accept SPARK_Mode=>Auto as
	configuration pragma.
	(Get_SPARK_Mode): Make the value for Auto explicit.
	* snames.ads-tmpl (Name_Auto): Add name.
diff mbox series

Patch

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -23176,7 +23176,7 @@  package body Sem_Prag is
          -- SPARK_Mode --
          ----------------
 
-         --  pragma SPARK_Mode [(On | Off)];
+         --  pragma SPARK_Mode [(Auto | On | Off)];
 
          when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
             Mode_Id : SPARK_Mode_Type;
@@ -23662,7 +23662,7 @@  package body Sem_Prag is
             --  Check the legality of the mode (no argument = ON)
 
             if Arg_Count = 1 then
-               Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
+               Check_Arg_Is_One_Of (Arg1, Name_Auto, Name_On, Name_Off);
                Mode := Chars (Get_Pragma_Arg (Arg1));
             else
                Mode := Name_On;
@@ -23713,6 +23713,15 @@  package body Sem_Prag is
             --  the pragma resides to find a potential construct.
 
             else
+               --  An explicit mode of Auto is only allowed as a configuration
+               --  pragma. Escape "pragma" to avoid replacement with "aspect".
+
+               if Mode_Id = None then
+                  Error_Pragma_Arg
+                    ("only configuration 'p'r'a'g'm'a% can have value &",
+                     Arg1);
+               end if;
+
                Stmt := Prev (N);
                while Present (Stmt) loop
 
@@ -31169,7 +31178,9 @@  package body Sem_Prag is
 
    function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type is
    begin
-      if N = Name_On then
+      if N = Name_Auto then
+         return None;
+      elsif N = Name_On then
          return On;
       elsif N = Name_Off then
          return Off;


diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -782,6 +782,7 @@  package Snames is
    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 + $;