[Ada] Spurious error on SPARK_Mode in generic package instantiation

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the generic instantiation to ensure that a context with a
missing SPARK_Mode annotation is treated as having SPARK_Mode set to Off. This
ensures that the following SPARK UG rule 9.4.1

   Code where SPARK_Mode is Off shall not enclose code where Spark_Mode is
   On. However, if an instance of a generic unit is enclosed by code where
   SPARK_Mode is Off and if any SPARK_Mode specifications occur within the
   generic unit, then the corresponding SPARK_Mode specifications occurring
   within the instance have no semantic effect.

does not lead to spurious errors.

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

--  gen_pack.ads

generic
  type T is private;

package Gen_Pack with SPARK_Mode is
   procedure Force_Body;

   generic
      type Inner_T is private;

   package Inner_Gen_Pack with SPARK_Mode => Off is
      type Inner_T_Ptr is access Inner_T;
   end Inner_Gen_Pack;

   package Inner_Inst is new Inner_Gen_Pack (Inner_T => T);

   type T_Ptr is private;

private
   pragma SPARK_Mode (Off);
   type T_Ptr is new Inner_Inst.Inner_T_Ptr;
end Gen_Pack;

--  gen_pack.adb

package body Gen_Pack with SPARK_Mode => Off is
   procedure Force_Body is begin null; end Force_Body;
end Gen_Pack;

--  main.adb

with Gen_Pack;

procedure Main is
   package Inst is new Gen_Pack (T => Integer);
begin
   null;
end Main;

-----------------
-- Compilation --
-----------------

$ gcc -c main.adb

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

2015-10-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch12.adb (Analyze_Package_Instantiation):
	Treat a missing SPARK_Mode annotation as having mode "Off".
	(Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode
	annotation as having mode "Off".
	(Instantiate_Package_Body): Code
	reformatting. Treat a missing SPARK_Mode annotation as having mode
	"Off".
	(Instantiate_Subprogram_Body): Code reformatting. Treat
	a missing SPARK_Mode annotation as having mode "Off".

Attachment: difs
Description: Text document