The following patch modifies the analysis of generic packages and subprograms
to flag aspect/pragma SPARK_Mode as illegal.
------------
-- Source --
------------
-- in_function.ads
pragma SPARK_Mode (On);
generic
Val : Integer;
function In_Function return Integer with SPARK_Mode;
-- in_function.adb
function In_Function return Integeris
pragma SPARK_Mode (On);
begin return 1; end In_Function;
-- in_procedure.ads
pragma SPARK_Mode (On);
generic
Val : Integer;
procedure In_Procedure with SPARK_Mode;
-- in_procedure.adb
procedure In_Procedure is
pragma SPARK_Mode (On);
begin null; end In_Procedure;
-- in_spec.ads
pragma SPARK_Mode;
generic
Var : Integer;
package In_Spec is
pragma SPARK_Mode;
procedure Proc with SPARK_Mode => On;
end In_Spec;
-- in_spec.adb
package body In_Spec is
procedure Proc is begin null; end Proc;
end In_Spec;
-- instances.ads
with In_Function;
with In_Procedure;
with In_Spec;
package Instances is
function Inst_3 is new In_Function (3);
procedure Inst_4 is new In_Procedure (4);
package Inst_5 is new In_Spec (5);
generic
Val : Integer;
function Nested_Func return Integer with SPARK_Mode;
generic
Val : Integer;
package Nested_Pack with SPARK_Mode is
procedure Proc;
pragma SPARK_Mode (On);
end Nested_Pack;
generic
Val : Integer;
procedure Nested_Proc with SPARK_Mode;
function Inst_6 is new Nested_Func (6);
package Inst_7 is new Nested_Pack (7);
procedure Inst_8 is new Nested_Proc (8);
end Instances;
-- instances.adb
package body Instances is
function Nested_Func return Integer is
pragma SPARK_Mode (On);
begin return 1; end Nested_Func;
package body Nested_Pack with SPARK_Mode is
procedure Proc is
pragma SPARK_Mode (On);
begin null; end Proc;
end Nested_Pack;
procedure Nested_Proc with SPARK_Mode is
begin null; end Nested_Proc;
end Instances;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c instances.adb
instances.adb:3:07: incorrect placement of pragma "Spark_Mode" in a generic
instances.adb:6:34: incorrect placement of aspect "Spark_Mode" in a generic
instances.adb:8:10: incorrect placement of pragma "Spark_Mode" in a generic
instances.adb:12:31: incorrect placement of aspect "Spark_Mode" on a generic
instances.ads:13:45: incorrect placement of aspect "Spark_Mode" on a generic
instances.ads:18:29: incorrect placement of aspect "Spark_Mode" on a generic
instances.ads:20:07: incorrect placement of pragma "Spark_Mode" in a generic
instances.ads:26:31: incorrect placement of aspect "Spark_Mode" on a generic
in_function.ads:1:01: incorrect placement of pragma "Spark_Mode" in a generic
in_function.ads:6:42: incorrect placement of aspect "Spark_Mode" on a generic
in_procedure.ads:1:01: incorrect placement of pragma "Spark_Mode" in a generic
in_procedure.ads:6:29: incorrect placement of aspect "Spark_Mode" on a generic
in_spec.ads:1:01: incorrect placement of pragma "Spark_Mode" in a generic
in_spec.ads:7:04: incorrect placement of pragma "Spark_Mode" in a generic
in_spec.ads:9:24: incorrect placement of aspect "Spark_Mode" in a generic
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-06 Hristian Kirtchev <kirtc...@adacore.com>
* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Flag illegal
use of SPARK_Mode.
* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Flag
illegal use of SPARK_Mode.
(Instantiate_Subprogram_Body): Flag illegal use of SPARK_Mode.
* sem_prag.adb (Analyze_Pragma): Code reformatting.
* sem_util.adb Add with and use clause for Aspects.
(Check_SPARK_Mode_In_Generic): New routine.
* sem_util.ads (Check_SPARK_Mode_In_Generic): New routine.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207535)
+++ sem_prag.adb (working copy)
@@ -19217,10 +19217,6 @@
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- if Inside_A_Generic then
- Error_Pragma ("incorrect placement of pragma% in a generic");
- end if;
-
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
@@ -19233,9 +19229,15 @@
Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
+ -- Packages and subprograms declared in a generic unit cannot be
+ -- subject to the pragma.
+
+ if Inside_A_Generic then
+ Error_Pragma ("incorrect placement of pragma% in a generic");
+
-- The pragma appears in a configuration pragmas file
- if No (Context) then
+ elsif No (Context) then
Check_Valid_Configuration_Pragma;
if Present (SPARK_Mode_Pragma) then
@@ -19258,8 +19260,7 @@
and then Nkind (Unit (Library_Unit (Context))) in
N_Generic_Declaration)
then
- Error_Pragma
- ("incorrect placement of pragma% in a generic unit");
+ Error_Pragma ("incorrect placement of pragma% in a generic");
end if;
SPARK_Mode_Pragma := N;
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 207533)
+++ sem_ch12.adb (working copy)
@@ -3118,6 +3118,8 @@
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
+ Check_SPARK_Mode_In_Generic (N);
+
-- The aspect specifications are not attached to the tree, and must
-- be copied and attached to the generic copy explicitly.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 207534)
+++ sem_util.adb (working copy)
@@ -23,6 +23,7 @@
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
@@ -2699,6 +2700,31 @@
end if;
end Check_Result_And_Post_State;
+ ---------------------------------
+ -- Check_SPARK_Mode_In_Generic --
+ ---------------------------------
+
+ procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is
+ Aspect : Node_Id;
+
+ begin
+ -- Try to find aspect SPARK_Mode and flag it as illegal
+
+ if Has_Aspects (N) then
+ Aspect := First (Aspect_Specifications (N));
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
+ Error_Msg_Name_1 := Name_SPARK_Mode;
+ Error_Msg_N
+ ("incorrect placement of aspect % on a generic", Aspect);
+ exit;
+ end if;
+
+ Next (Aspect);
+ end loop;
+ end if;
+ end Check_SPARK_Mode_In_Generic;
+
------------------------------
-- Check_Unprotected_Access --
------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 207533)
+++ sem_util.ads (working copy)
@@ -62,6 +62,7 @@
-- Precondition
-- Refined_Depends
-- Refined_Global
+ -- Refined_Post
-- Refined_States
-- Test_Case
@@ -289,6 +290,10 @@
-- and post-state. Prag is a [refined] postcondition or a contract-cases
-- pragma. Result_Seen is set when the pragma mentions attribute 'Result.
+ procedure Check_SPARK_Mode_In_Generic (N : Node_Id);
+ -- Given a generic package [body] or a generic subprogram [body], inspect
+ -- the aspect specifications (if any) and flag SPARK_Mode as illegal.
+
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 207533)
+++ sem_ch6.adb (working copy)
@@ -1193,6 +1193,8 @@
end loop;
end;
+ Check_SPARK_Mode_In_Generic (N);
+
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
