[Ada] Poor error message on pragma SPARK_Mode

[Arnaud Charlet]

This patch modifies the mode conformance checks of pragma SPARK_Mode to account
for the case where the pragma appears without an argument.

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

--  pack.ads

package Pack is
   procedure Error;
end Pack;

--  pack.adb

package body Pack is
   procedure Error with SPARK_Mode is
   begin null; end Error;
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnatd.F pack.adb
pack.adb:2:25: incorrect use of SPARK_Mode
pack.adb:2:25: no value was set for SPARK_Mode on "Error" at pack.ads:2

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

2015-02-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Pragma_Conformance): Add
	local variable Arg. Ensure that all errors are associated with
	the pragma if it appears without an argument. Add comments on
	various cases.

-------------- next part --------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 220439)
+++ sem_prag.adb	(working copy)
@@ -19615,42 +19615,72 @@
                Entity_Pragma  : Node_Id;
                Entity         : Entity_Id)
             is
+               Arg : Node_Id := Arg1;
+
             begin
+               --  The current pragma may appear without an argument. If this
+               --  is the case, associate all error messages with the pragma
+               --  itself.
+
+               if No (Arg) then
+                  Arg := N;
+               end if;
+
+               --  The mode of the current pragma is compared against that of
+               --  an enclosing context.
+
                if Present (Context_Pragma) then
                   pragma Assert (Nkind (Context_Pragma) = N_Pragma);
 
-                  --  New mode less restrictive than the established mode
+                  --  Issue an error if the new mode is less restrictive than
+                  --  that of the context.
 
                   if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
                     and then Get_SPARK_Mode_From_Pragma (N) = On
                   then
                      Error_Msg_N
-                       ("cannot change SPARK_Mode from Off to On", Arg1);
+                       ("cannot change SPARK_Mode from Off to On", Arg);
                      Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
-                     Error_Msg_N ("\SPARK_Mode was set to Off#", Arg1);
+                     Error_Msg_N ("\SPARK_Mode was set to Off#", Arg);
                      raise Pragma_Exit;
                   end if;
                end if;
 
+               --  The mode of the current pragma is compared against that of
+               --  an initial package/subprogram declaration.
+
                if Present (Entity) then
+
+                  --  Both the initial declaration and the completion carry
+                  --  SPARK_Mode pragmas.
+
                   if Present (Entity_Pragma) then
+                     pragma Assert (Nkind (Entity_Pragma) = N_Pragma);
+
+                     --  Issue an error if the new mode is less restrictive
+                     --  than that of the initial declaration.
+
                      if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
                        and then Get_SPARK_Mode_From_Pragma (N) = On
                      then
-                        Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+                        Error_Msg_N ("incorrect use of SPARK_Mode", Arg);
                         Error_Msg_Sloc := Sloc (Entity_Pragma);
                         Error_Msg_NE
                           ("\value Off was set for SPARK_Mode on&#",
-                           Arg1, Entity);
+                           Arg, Entity);
                         raise Pragma_Exit;
                      end if;
 
+                  --  Otherwise the initial declaration lacks a SPARK_Mode
+                  --  pragma in which case the current pragma is illegal as
+                  --  it cannot "complete".
+
                   else
-                     Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+                     Error_Msg_N ("incorrect use of SPARK_Mode", Arg);
                      Error_Msg_Sloc := Sloc (Entity);
                      Error_Msg_NE
                        ("\no value was set for SPARK_Mode on&#",
-                        Arg1, Entity);
+                        Arg, Entity);
                      raise Pragma_Exit;
                   end if;
                end if;