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);
 

Reply via email to