diff mbox

[Ada] Aspect / pragma SPARK_Mode

Message ID 20130708074126.GA23139@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet July 8, 2013, 7:41 a.m. UTC 
This patch removes the checks on mode duplication for the configuration form of
the pragma to keep the behavior in line with other configuration pragmas.

------------
-- Source --
------------

--  unit_spark_mode.ads

pragma SPARK_Mode (Auto);
pragma SPARK_Mode (On);

package Unit_SPARK_Mode is
end Unit_SPARK_Mode;

-----------------
-- Compilation --
-----------------

$ gcc -c unit_spark_mode.ads

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

2013-07-08  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Remove
	variable Unit_Prag. Remove the check on duplicate mode for the
	configuration form of the pragma.
	(Redefinition_Error): Removed.
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200752)
+++ sem_prag.adb	(working copy)
@@ -16354,16 +16354,6 @@ 
             function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id;
             --  Convert a value of type SPARK_Mode_Id into a corresponding name
 
-            procedure Redefinition_Error (Mode : SPARK_Mode_Id);
-            --  Emit an error on an attempt to redefine existing mode Mode. The
-            --  message is associated with the first argument of the current
-            --  pragma.
-
-            procedure Redefinition_Error (Prag : Node_Id);
-            --  Emit an error on an attempt to redefine the mode of Prag. The
-            --  message is associated with the first argument of the current
-            --  pragma.
-
             ------------------
             -- Chain_Pragma --
             ------------------
@@ -16474,41 +16464,14 @@ 
                end if;
             end Get_SPARK_Mode_Name;
 
-            ------------------------
-            -- Redefinition_Error --
-            ------------------------
-
-            procedure Redefinition_Error (Mode : SPARK_Mode_Id) is
-            begin
-               Error_Msg_Name_1 := Get_SPARK_Mode_Name (Mode);
-               Error_Msg_N
-                 ("cannot redefine 'S'P'A'R'K mode, already set to %", Arg1);
-            end Redefinition_Error;
-
-            ------------------------
-            -- Redefinition_Error --
-            ------------------------
-
-            procedure Redefinition_Error (Prag : Node_Id) is
-               Mode : constant Name_Id :=
-                        Chars (Get_Pragma_Arg (First
-                         (Pragma_Argument_Associations (Prag))));
-            begin
-               Error_Msg_Name_1 := Mode;
-               Error_Msg_Sloc   := Sloc (Prag);
-               Error_Msg_N
-                 ("cannot redefine 'S'P'A'R'K mode, already set to % #", Arg1);
-            end Redefinition_Error;
-
             --  Local variables
 
-            Body_Id   : Entity_Id;
-            Context   : Node_Id;
-            Mode      : Name_Id;
-            Mode_Id   : SPARK_Mode_Id;
-            Spec_Id   : Entity_Id;
-            Stmt      : Node_Id;
-            Unit_Prag : Node_Id;
+            Body_Id : Entity_Id;
+            Context : Node_Id;
+            Mode    : Name_Id;
+            Mode_Id : SPARK_Mode_Id;
+            Spec_Id : Entity_Id;
+            Stmt    : Node_Id;
 
          --  Start of processing for SPARK_Mode
 
@@ -16536,39 +16499,15 @@ 
 
             if No (Context) then
                Check_Valid_Configuration_Pragma;
+               Global_SPARK_Mode := Mode_Id;
 
-               --  Set the global mode
-
-               if Global_SPARK_Mode = None then
-                  Global_SPARK_Mode := Mode_Id;
-
-               --  Catch an attempt to redefine an existing global mode by
-               --  using multiple configuration files.
-
-               elsif Global_SPARK_Mode /= Mode_Id then
-                  Redefinition_Error (Global_SPARK_Mode);
-               end if;
-
             --  When the pragma is placed before the declaration of a unit, it
             --  configures the whole unit.
 
             elsif Nkind (Context) = N_Compilation_Unit then
                Check_Valid_Configuration_Pragma;
+               Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
 
-               Unit_Prag := SPARK_Mode_Pragma (Current_Sem_Unit);
-
-               --  Set the unit mode
-
-               if No (Unit_Prag) then
-                  Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
-
-               --  Catch an attempt to redefine the unit mode by using multiple
-               --  pragmas declared in the same region.
-
-               else
-                  Redefinition_Error (Unit_Prag);
-               end if;
-
             --  The pragma applies to a [library unit] subprogram or package
 
             else