[Ada] Spurious error on missing SPARK_Mode annotation with inlining

[Arnaud Charlet <charlet at adacore dot com>]

This patch augments the generic instantiation machinery to preserve a key
property of a package or subprogram spec for the corresponding body which
may be instantiated or inlined later. Whenever a generic is instantiated in an
environment where the SPARK_Mode is Off, any SPARK_Mode pragma found within the
spec and body must be ignored. Due to late instantiation or inlining of bodies,
this property was previously lost which in turn led to spurious errors about
missing SPARK_Mode annotations in specs.

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

--  gen.ads

generic
package Gen is
   task type Tsk;
end Gen;

--  gen.adb

with Ada.Real_Time; use Ada.Real_Time;

package body Gen is
   task body Tsk is
      Now   : constant Time := Time_Of (0, Time_Span_First);
      Later : Time;

   begin
      Later := Now + Milliseconds (1);
   end Tsk;
end Gen;

--  pack.ads

with Gen;

package Pack is
   package Inst is new Gen;
end Pack;

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

$ gcc -c -gnatn pack.ads

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

2017-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
	(Ignore_SPARK_Mode_Pragmas): New routine.
	(Set_Ignore_SPARK_Mode_Pragmas): New routine.
	(Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
	* einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
	related entities.
	(Ignore_SPARK_Mode_Pragmas): New routine
	along with pragma Inline.
	(Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
	* opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
	Ignore_SPARK_Mode_Pragmas_In_Instance.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
	Save and restore the value of global flag
	Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
	the corresponding spec or the body must ignore all SPARK_Mode
	pragmas found within.
	(Analyze_Subprogram_Declaration): Mark
	the spec when it needs to ignore all SPARK_Mode pragmas found
	within to allow the body to infer this property in case it is
	instantiated or inlined later.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
	value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
	the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
	when the corresponding spec also ignored all SPARK_Mode pragmas
	found within.
	(Analyze_Package_Declaration): Mark the spec when
	it needs to ignore all SPARK_Mode pragmas found within to allow
	the body to infer this property in case it is instantiated or
	inlined later.
	* sem_ch12.adb (Analyze_Formal_Package_Declaration):
	Save and restore the value of flag
	Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
	formal spec when it needs to ignore all SPARK_Mode
	pragmas found within to allow the body to infer this
	property in case it is instantiated or inlined later.
	(Analyze_Package_Instantiation): Save and restore the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
	the instance spec when it needs to ignore all SPARK_Mode
	pragmas found within to allow the body to infer this
	property in case it is instantiated or inlined later.
	(Analyze_Subprogram_Instantiation): Save and restore the value
	of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
	instance spec and anonymous package when they need to ignore
	all SPARK_Mode pragmas found within to allow the body to infer
	this property in case it is instantiated or inlined later.
	(Instantiate_Package_Body): Save and restore the value of global
	flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
	global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
	corresponding instance spec also ignored all SPARK_Mode pragmas
	found within.
	(Instantiate_Subprogram_Body): Save and restore the
	value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
	the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
	when the corresponding instance spec also ignored all SPARK_Mode
	pragmas found within.
	* sem_prag.adb (Analyze_Pragma): Update the reference to
	Ignore_Pragma_SPARK_Mode.
	* sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
	all SPARK_Mode pragmas defined within yields mode "off".

Attachment: difs
Description: Text document