[Ada] Forbid the use of aspect/pragma SPARK_Mode in generics

[Arnaud Charlet <charlet at adacore dot com>]

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  <kirtchev@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.

Attachment: difs
Description: Text document