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 <kirtc...@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.
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;
