[multiple changes]

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".

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

	* bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting.

2017-04-25  Bob Duff  <duff@adacore.com>

	* exp_atag.adb (Build_CW_Membership): Add "Suppress =>
	All_Checks" to avoid generating unnecessary checks.
	* exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress =>
	All_Checks".
	* sem.ads: Fix comment.
	* expander.ads: Fix comment.
	* exp_atag.ads: Fix comment: "Index = 0" should be
	"Index >= 0".

2017-04-25  Gary Dismukes  <dismukes@adacore.com>

	* s-taprop-linux.adb: Minor editorial fixes.

From-SVN: r247182

1 files changed, 21 insertions, 0 deletions

diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index e5879df..260f923 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -539,6 +539,8 @@ package body Sem_Ch7 is
 
       --  Local variables
 
+      Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+
       Body_Id          : Entity_Id;
       HSS              : Node_Id;
       Last_Spec_Entity : Entity_Id;
@@ -738,6 +740,14 @@ package body Sem_Ch7 is
          Set_SPARK_Aux_Pragma           (Body_Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited     (Body_Id);
          Set_SPARK_Aux_Pragma_Inherited (Body_Id);
+
+         --  A package body may be instantiated or inlined at a later pass.
+         --  Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when
+         --  it applied to the package spec.
+
+         if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+         end if;
       end if;
 
       Set_Categorization_From_Pragmas (N);
@@ -931,6 +941,8 @@ package body Sem_Ch7 is
          end if;
       end if;
 
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
       Restore_Ghost_Mode (Mode);
    end Analyze_Package_Body_Helper;
 
@@ -969,6 +981,15 @@ package body Sem_Ch7 is
          Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited     (Id);
          Set_SPARK_Aux_Pragma_Inherited (Id);
+
+         --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+         --  case the body of this package is instantiated or inlined later and
+         --  out of context. The body uses this attribute to restore the value
+         --  of the global flag.
+
+         if Ignore_SPARK_Mode_Pragmas_In_Instance then
+            Set_Ignore_SPARK_Mode_Pragmas (Id);
+         end if;
       end if;
 
       --  Analyze aspect specifications immediately, since we need to recognize