[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

19 files changed, 377 insertions, 122 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9e85818..bec26bc 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,85 @@
+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.
+
 2017-04-25  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* sem_util.adb (New_Copy_Tree): Put back the declarations of the
diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb
index 8ada7c1..5544c82 100644
--- a/gcc/ada/bindgen.adb
+++ b/gcc/ada/bindgen.adb
@@ -1120,8 +1120,8 @@ package body Bindgen is
                --  where we increment the elaboration entity if one exists.
 
                --  Likewise for lone specs with an elaboration entity defined
-               --  despite No_Elaboration_Code, e.g. when requested to
-               --  preserve control flow.
+               --  despite No_Elaboration_Code, e.g. when requested to preserve
+               --  control flow.
 
                if (U.Utype = Is_Body or else U.Utype = Is_Spec_Only)
                  and then Units.Table (Unum_Spec).Set_Elab_Entity
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 118e09f..5638bc0 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -620,7 +620,7 @@ package body Einfo is
    --    Body_Needed_For_Inlining        Flag299
 
    --    Has_Private_Extension           Flag300
-   --    (unused)                        Flag301
+   --    Ignore_SPARK_Mode_Pragmas       Flag301
    --    (unused)                        Flag302
    --    (unused)                        Flag303
    --    (unused)                        Flag304
@@ -1981,6 +1981,29 @@ package body Einfo is
       return Node4 (Id);
    end Homonym;
 
+   function Ignore_SPARK_Mode_Pragmas (Id : E) return B is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type)
+          or else
+         Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Operator,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Flag301 (Id);
+   end Ignore_SPARK_Mode_Pragmas;
+
    function Import_Pragma (Id : E) return E is
    begin
       pragma Assert (Is_Subprogram (Id));
@@ -5073,6 +5096,29 @@ package body Einfo is
       Set_Elist24 (Id, V);
    end Set_Incomplete_Actuals;
 
+   procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type)
+          or else
+         Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Operator,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      Set_Flag301 (Id, V);
+   end Set_Ignore_SPARK_Mode_Pragmas;
+
    procedure Set_Import_Pragma (Id : E; V : E) is
    begin
       pragma Assert (Is_Subprogram (Id));
@@ -9402,6 +9448,7 @@ package body Einfo is
       W ("Has_Visible_Refinement",          Flag263 (Id));
       W ("Has_Volatile_Components",         Flag87  (Id));
       W ("Has_Xref_Entry",                  Flag182 (Id));
+      W ("Ignore_SPARK_Mode_Pragmas",       Flag301 (Id));
       W ("In_Package_Body",                 Flag48  (Id));
       W ("In_Private_Part",                 Flag45  (Id));
       W ("In_Use",                          Flag8   (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index dc63408..9d8a33c 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2164,6 +2164,13 @@ package Einfo is
 --       scopes. Homonyms in the same scope are overloaded. Used for name
 --       resolution and for the generation of debugging information.
 
+--    Ignore_SPARK_Mode_Pragmas (Flag301)
+--       Present in concurrent type, entry, operator, [generic] package,
+--       package body, [generic] subprogram, and subprogram body entities.
+--       Set when the entity appears in an instance subject to SPARK_Mode
+--       "off" and indicates that all SPARK_Mode pragmas found within must
+--       be ignored.
+
 --    Implementation_Base_Type (synthesized)
 --       Applies to all entities. For types, similar to Base_Type, but never
 --       returns a private type when applied to a non-private type. Instead in
@@ -5922,14 +5929,15 @@ package Einfo is
    --    Extra_Formals                       (Node28)
    --    Contract                            (Node34)
    --    SPARK_Pragma                        (Node40)   (protected kind)
-   --    Needs_No_Actuals                    (Flag22)
-   --    Uses_Sec_Stack                      (Flag95)
    --    Default_Expressions_Processed       (Flag108)
    --    Entry_Accepted                      (Flag152)
-   --    Sec_Stack_Needed_For_Return         (Flag167)
    --    Has_Expanded_Contract               (Flag240)
-   --    SPARK_Pragma_Inherited              (Flag265)  (protected kind)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Is_Entry_Wrapper                    (Flag297)
+   --    Needs_No_Actuals                    (Flag22)
+   --    Sec_Stack_Needed_For_Return         (Flag167)
+   --    SPARK_Pragma_Inherited              (Flag265)  (protected kind)
+   --    Uses_Sec_Stack                      (Flag95)
    --    Address_Clause                      (synth)
    --    Entry_Index_Type                    (synth)
    --    First_Formal                        (synth)
@@ -6056,6 +6064,7 @@ package Einfo is
    --    Has_Nested_Subprogram               (Flag282)
    --    Has_Out_Or_In_Out_Parameter         (Flag110)
    --    Has_Recursive_Call                  (Flag143)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Is_Abstract_Subprogram              (Flag19)   (non-generic case only)
    --    Is_Called                           (Flag102)  (non-generic case only)
    --    Is_Constructor                      (Flag76)
@@ -6209,6 +6218,7 @@ package Einfo is
    --    SPARK_Pragma                        (Node40)
    --    Default_Expressions_Processed       (Flag108)
    --    Has_Nested_Subprogram               (Flag282)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Is_Intrinsic_Subprogram             (Flag64)
    --    Is_Machine_Code_Subprogram          (Flag137)
    --    Is_Primitive                        (Flag218)
@@ -6272,6 +6282,7 @@ package Einfo is
    --    Has_Forward_Instantiation           (Flag175)
    --    Has_Master_Entity                   (Flag21)
    --    Has_RACW                            (Flag214)  (non-generic case only)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    In_Package_Body                     (Flag48)
    --    In_Use                              (Flag8)
    --    Is_Instantiated                     (Flag126)
@@ -6299,6 +6310,7 @@ package Einfo is
    --    SPARK_Aux_Pragma                    (Node41)
    --    Contains_Ignored_Ghost_Code         (Flag279)
    --    Delay_Subprogram_Descriptors        (Flag50)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    SPARK_Aux_Pragma_Inherited          (Flag266)
    --    SPARK_Pragma_Inherited              (Flag265)
    --    Scope_Depth                         (synth)
@@ -6367,6 +6379,7 @@ package Einfo is
    --    Has_Master_Entity                   (Flag21)
    --    Has_Nested_Block_With_Handler       (Flag101)
    --    Has_Nested_Subprogram               (Flag282)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Is_Abstract_Subprogram              (Flag19)   (non-generic case only)
    --    Is_Asynchronous                     (Flag81)
    --    Is_Called                           (Flag102)  (non-generic case only)
@@ -6406,6 +6419,7 @@ package Einfo is
 
    --  E_Protected_Body
    --    SPARK_Pragma                        (Node40)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    SPARK_Pragma_Inherited              (Flag265)
    --    (any others??? First/Last Entity, Scope_Depth???)
 
@@ -6427,6 +6441,7 @@ package Einfo is
    --    Entry_Max_Queue_Lengths_Array       (Node35)
    --    SPARK_Pragma                        (Node40)
    --    SPARK_Aux_Pragma                    (Node41)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Sec_Stack_Needed_For_Return         (Flag167)  ???
    --    SPARK_Aux_Pragma_Inherited          (Flag266)
    --    SPARK_Pragma_Inherited              (Flag265)
@@ -6557,6 +6572,7 @@ package Einfo is
    --  E_Task_Body
    --    Contract                            (Node34)
    --    SPARK_Pragma                        (Node40)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    SPARK_Pragma_Inherited              (Flag265)
    --    (any others??? First/Last Entity, Scope_Depth???)
 
@@ -6580,6 +6596,7 @@ package Einfo is
    --    Delay_Cleanups                      (Flag114)
    --    Has_Master_Entity                   (Flag21)
    --    Has_Storage_Size_Clause             (Flag23)   (base type only)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Sec_Stack_Needed_For_Return         (Flag167)  ???
    --    SPARK_Aux_Pragma_Inherited          (Flag266)
    --    SPARK_Pragma_Inherited              (Flag265)
@@ -7103,6 +7120,7 @@ package Einfo is
    function Has_Xref_Entry                      (Id : E) return B;
    function Hiding_Loop_Variable                (Id : E) return E;
    function Homonym                             (Id : E) return E;
+   function Ignore_SPARK_Mode_Pragmas           (Id : E) return B;
    function Import_Pragma                       (Id : E) return E;
    function Incomplete_Actuals                  (Id : E) return L;
    function In_Package_Body                     (Id : E) return B;
@@ -7788,6 +7806,7 @@ package Einfo is
    procedure Set_Has_Xref_Entry                  (Id : E; V : B := True);
    procedure Set_Hiding_Loop_Variable            (Id : E; V : E);
    procedure Set_Homonym                         (Id : E; V : E);
+   procedure Set_Ignore_SPARK_Mode_Pragmas       (Id : E; V : B := True);
    procedure Set_Import_Pragma                   (Id : E; V : E);
    procedure Set_Incomplete_Actuals              (Id : E; V : L);
    procedure Set_In_Package_Body                 (Id : E; V : B := True);
@@ -8587,6 +8606,7 @@ package Einfo is
    pragma Inline (Has_Xref_Entry);
    pragma Inline (Hiding_Loop_Variable);
    pragma Inline (Homonym);
+   pragma Inline (Ignore_SPARK_Mode_Pragmas);
    pragma Inline (Import_Pragma);
    pragma Inline (Incomplete_Actuals);
    pragma Inline (In_Package_Body);
@@ -9109,6 +9129,7 @@ package Einfo is
    pragma Inline (Set_Has_Xref_Entry);
    pragma Inline (Set_Hiding_Loop_Variable);
    pragma Inline (Set_Homonym);
+   pragma Inline (Set_Ignore_SPARK_Mode_Pragmas);
    pragma Inline (Set_Import_Pragma);
    pragma Inline (Set_Incomplete_Actuals);
    pragma Inline (Set_In_Package_Body);
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index d2c41fc..2d26d07 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -508,10 +508,12 @@ package body Errout is
                      Error_Msg_Internal
                        ("info: in inlined body #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   elsif Is_Warning_Msg or Is_Style_Msg then
                      Error_Msg_Internal
                        (Warn_Insertion & "in inlined body #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   else
                      Error_Msg_Internal
                        ("error in inlined body #",
@@ -525,10 +527,12 @@ package body Errout is
                      Error_Msg_Internal
                        ("info: in instantiation #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   elsif Is_Warning_Msg or else Is_Style_Msg then
                      Error_Msg_Internal
                        (Warn_Insertion & "in instantiation #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   else
                      Error_Msg_Internal
                        ("instantiation error #",
diff --git a/gcc/ada/exp_atag.adb b/gcc/ada/exp_atag.adb
index bd5f9e2..dd25237 100644
--- a/gcc/ada/exp_atag.adb
+++ b/gcc/ada/exp_atag.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2006-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2006-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -178,7 +178,7 @@ package body Exp_Atag is
       --    Typ_TSD  : constant Type_Specific_Data_Ptr
       --                          := Build_TSD (Address!(Typ_Tag));
       --    Index    : constant Integer := Obj_TSD.Idepth - Typ_TSD.Idepth
-      --    Index > 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
+      --    Index >= 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
 
       Insert_Action (Related_Nod,
         Make_Object_Declaration (Loc,
@@ -199,7 +199,8 @@ package body Exp_Atag is
           Constant_Present    => True,
           Object_Definition   => New_Occurrence_Of
                                    (RTE (RE_Type_Specific_Data_Ptr), Loc),
-          Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))));
+          Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))),
+        Suppress => All_Checks);
 
       Insert_Action (Related_Nod,
         Make_Object_Declaration (Loc,
@@ -209,7 +210,8 @@ package body Exp_Atag is
                                    (RTE (RE_Type_Specific_Data_Ptr), Loc),
           Expression => Build_TSD (Loc,
                           Unchecked_Convert_To (RTE (RE_Address),
-                            Typ_Tag_Node))));
+                            Typ_Tag_Node))),
+        Suppress => All_Checks);
 
       Insert_Action (Related_Nod,
         Make_Object_Declaration (Loc,
@@ -230,7 +232,8 @@ package body Exp_Atag is
                    Prefix        => New_Occurrence_Of (Typ_TSD, Loc),
                    Selector_Name =>
                      New_Occurrence_Of
-                       (RTE_Record_Component (RE_Idepth), Loc)))));
+                       (RTE_Record_Component (RE_Idepth), Loc)))),
+        Suppress => All_Checks);
 
       New_Node :=
         Make_And_Then (Loc,
diff --git a/gcc/ada/exp_atag.ads b/gcc/ada/exp_atag.ads
index 6551f15..d53466f 100644
--- a/gcc/ada/exp_atag.ads
+++ b/gcc/ada/exp_atag.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2006-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 2006-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -54,7 +54,7 @@ package Exp_Atag is
    --  computed in constant time by the formula:
    --
    --   Index := TSD (Obj'Tag).Idepth - TSD (Typ'Tag).Idepth;
-   --   Index > 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
+   --   Index >= 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
    --
    --  Related_Nod is the node where the implicit declaration of variable Index
    --  is inserted. Obj_Tag_Node is relocated.
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 1fdc50c..8a2698b 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -5859,7 +5859,8 @@ package body Exp_Ch4 is
                if Tagged_Type_Expansion then
                   Tagged_Membership (N, SCIL_Node, New_N);
                   Rewrite (N, New_N);
-                  Analyze_And_Resolve (N, Restyp);
+                  Analyze_And_Resolve
+                    (N, Restyp, Suppress => All_Checks);
 
                   --  Update decoration of relocated node referenced by the
                   --  SCIL node.
@@ -10908,7 +10909,8 @@ package body Exp_Ch4 is
                Insert_Action (N,
                  Make_Raise_Constraint_Error (Loc,
                    Condition => Cond,
-                   Reason    => CE_Tag_Check_Failed));
+                   Reason    => CE_Tag_Check_Failed),
+                 Suppress => All_Checks);
             end Make_Tag_Check;
 
          --  Start of processing for Tagged_Conversion
diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb
index d2cad88..ede7e2e 100644
--- a/gcc/ada/exp_dbug.adb
+++ b/gcc/ada/exp_dbug.adb
@@ -343,8 +343,10 @@ package body Exp_Dbug is
 
       begin
          Enable :=
-           Enable or else (Ekind (T) in Array_Kind
-                            and then Present (Packed_Array_Impl_Type (T)));
+           Enable
+             or else
+               (Ekind (T) in Array_Kind
+                 and then Present (Packed_Array_Impl_Type (T)));
       end Enable_If_Packed_Array;
 
       ----------------------
@@ -359,7 +361,7 @@ package body Exp_Dbug is
          elsif Nkind (N) = N_Identifier
            and then Scope_Contains (Scope (Entity (N)), Ent)
            and then (Ekind (Entity (N)) = E_Constant
-                     or else Ekind (Entity (N)) = E_In_Parameter)
+                      or else Ekind (Entity (N)) = E_In_Parameter)
          then
             Prepend_String_To_Buffer (Get_Name_String (Chars (Entity (N))));
 
@@ -375,25 +377,25 @@ package body Exp_Dbug is
       -- Scope_Contains --
       --------------------
 
-      function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean
-      is
+      function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean is
          Cur : Node_Id := Scope (Ent);
+
       begin
          while Present (Cur) loop
             if Cur = Sc then
                return True;
             end if;
+
             Cur := Scope (Cur);
          end loop;
+
          return False;
       end Scope_Contains;
 
    --  Start of processing for Debug_Renaming_Declaration
 
    begin
-      if not Comes_From_Source (N)
-        and then not Needs_Debug_Info (Ent)
-      then
+      if not Comes_From_Source (N) and then not Needs_Debug_Info (Ent) then
          return Empty;
       end if;
 
diff --git a/gcc/ada/expander.ads b/gcc/ada/expander.ads
index 6c8c649..9276476 100644
--- a/gcc/ada/expander.ads
+++ b/gcc/ada/expander.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -66,9 +66,9 @@
 --      always the case).
 
 --  In both these cases, Replace or Rewrite must be used to achieve the
---  of the node, since the Expander routine is only passed the Node_Id
---  of the node to be expanded, and the resulting expanded Node_Id must
---  be the same (the parameter to Expand is mode in, not mode in-out).
+--  expansion of the node, since the Expander routine is only passed the
+--  Node_Id of the node to be expanded, and the resulting expanded Node_Id
+--  must be the same (the parameter to Expand is mode in, not mode in-out).
 
 --  For nodes other than subexpressions, it is not necessary to preserve the
 --  original tree in the Expand routines, unlike the case for modifications
diff --git a/gcc/ada/fname.adb b/gcc/ada/fname.adb
index 5acd813..0487085 100644
--- a/gcc/ada/fname.adb
+++ b/gcc/ada/fname.adb
@@ -59,14 +59,13 @@ package body Fname is
 
    function Has_Internal_Extension (Fname : String) return Boolean;
    pragma Inline (Has_Internal_Extension);
-   --  True if the extension is appropriate for an internal/predefined
-   --  unit. That means ".ads" or ".adb" for source files, and ".ali" for
-   --  ALI files.
+   --  True if the extension is appropriate for an internal/predefined unit.
+   --  That means ".ads" or ".adb" for source files, and ".ali" for ALI files.
 
    function Has_Prefix (X, Prefix : String) return Boolean;
    pragma Inline (Has_Prefix);
    --  True if Prefix is at the beginning of X. For example,
-   --  Has_Prefix("a-filename.ads", Prefix => "a-") is True.
+   --  Has_Prefix ("a-filename.ads", Prefix => "a-") is True.
 
    ----------------------------
    -- Has_Internal_Extension --
@@ -145,14 +144,14 @@ package body Fname is
       subtype Str8 is String (1 .. 8);
 
       Renaming_Names : constant array (1 .. 8) of Str8 :=
-        ("calendar",       -- Calendar
-         "machcode",       -- Machine_Code
-         "unchconv",       -- Unchecked_Conversion
-         "unchdeal",       -- Unchecked_Deallocation
-         "directio",       -- Direct_IO
-         "ioexcept",       -- IO_Exceptions
-         "sequenio",       -- Sequential_IO
-         "text_io.");      -- Text_IO
+        ("calendar",   --  Calendar
+         "machcode",   --  Machine_Code
+         "unchconv",   --  Unchecked_Conversion
+         "unchdeal",   --  Unchecked_Deallocation
+         "directio",   --  Direct_IO
+         "ioexcept",   --  IO_Exceptions
+         "sequenio",   --  Sequential_IO
+         "text_io.");  --  Text_IO
 
       --  Note: the implementation is optimized to perform uniform comparisons
       --  on string slices whose length is known at compile time and at most 8
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 94fdd8a..bb6c5b3 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -814,18 +814,18 @@ package Opt is
    --  default value appropriate to the system (in Osint.Initialize), and then
    --  reset if a command line switch is used to change the setting.
 
-   Ignore_Pragma_SPARK_Mode : Boolean := False;
-   --  GNAT
-   --  Set True to ignore the semantics and effects of pragma SPARK_Mode when
-   --  the pragma appears inside an instance whose enclosing context is subject
-   --  to SPARK_Mode "off".
-
    Ignore_Rep_Clauses : Boolean := False;
    --  GNAT
    --  Set True to ignore all representation clauses. Useful when compiling
    --  code from foreign compilers for checking or ASIS purposes. Can be
    --  set True by use of -gnatI.
 
+   Ignore_SPARK_Mode_Pragmas_In_Instance : Boolean := False;
+   --  GNAT
+   --  Set True to ignore the semantics and effects of pragma SPARK_Mode when
+   --  the pragma appears inside an instance whose enclosing context is subject
+   --  to SPARK_Mode "off". This property applies to nested instances.
+
    Ignore_Style_Checks_Pragmas : Boolean := False;
    --  GNAT
    --  Set True to ignore all Style_Checks pragmas. Can be set True by use
diff --git a/gcc/ada/s-taprop-linux.adb b/gcc/ada/s-taprop-linux.adb
index 00cf9ce..a435617 100644
--- a/gcc/ada/s-taprop-linux.adb
+++ b/gcc/ada/s-taprop-linux.adb
@@ -849,8 +849,8 @@ package body System.Task_Primitives.Operations is
                end if;
             end loop;
 
-            --  Cover the odd situtation if someone decides to change
-            --  Parameters.Max_Task_Image_Length to less than 16 characters
+            --  Cover the odd situation where someone decides to change
+            --  Parameters.Max_Task_Image_Length to less than 16 characters.
 
             if Len > Parameters.Max_Task_Image_Length then
                Len := Parameters.Max_Task_Image_Length;
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index 6cd050e..be5bc33 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -165,7 +165,7 @@
 ------------------
 
 --  For certain kind of expressions, such as aggregates, we need to defer
---  expansion of the aggregate and its inner expressions after the whole
+--  expansion of the aggregate and its inner expressions until after the whole
 --  set of expressions appearing inside the aggregate have been analyzed.
 --  Consider, for instance the following example:
 --
@@ -177,17 +177,17 @@
 --  repeatedly (for instance in the above aggregate "new Thing (Function_Call)"
 --  needs to be called 100 times.)
 
---  The reason why this mechanism does not work is that the expanded code for
---  the children is typically inserted above the parent and thus when the
---  father gets expanded no re-evaluation takes place. For instance in the case
---  of aggregates if "new Thing (Function_Call)" is expanded before of the
---  aggregate the expanded code will be placed outside of the aggregate and
---  when expanding the aggregate the loop from 1 to 100 will not surround the
+--  The reason this mechanism does not work is that the expanded code for the
+--  children is typically inserted above the parent and thus when the father
+--  gets expanded no re-evaluation takes place. For instance in the case of
+--  aggregates if "new Thing (Function_Call)" is expanded before the aggregate
+--  the expanded code will be placed outside of the aggregate and when
+--  expanding the aggregate the loop from 1 to 100 will not surround the
 --  expanded code for "new Thing (Function_Call)".
 
---  To remedy this situation we introduce a new flag which signals whether we
---  want a full analysis (i.e. expansion is enabled) or a pre-analysis which
---  performs Analysis and Resolution but no expansion.
+--  To remedy this situation we introduce a flag that signals whether we want a
+--  full analysis (i.e. expansion is enabled) or a pre-analysis which performs
+--  Analysis and Resolution but no expansion.
 
 --  After the complete pre-analysis of an expression has been carried out we
 --  can transform the expression and then carry out the full three stage
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index bc82410..3a450eb 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -2605,8 +2605,8 @@ package body Sem_Ch12 is
 
       --  Local variables
 
-      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+      Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+      --  Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
 
       Associations     : Boolean := True;
       New_N            : Node_Id;
@@ -2782,7 +2782,12 @@ package body Sem_Ch12 is
       --  all SPARK_Mode pragmas within the generic_package_name.
 
       if SPARK_Mode /= On then
-         Ignore_Pragma_SPARK_Mode := True;
+         Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+         --  Mark the formal spec in case the body is instantiated at a later
+         --  pass. This preserves the original context in effect for the body.
+
+         Set_Ignore_SPARK_Mode_Pragmas (Formal);
       end if;
 
       Analyze (Specification (N));
@@ -2843,7 +2848,7 @@ package body Sem_Ch12 is
          Analyze_Aspect_Specifications (N, Pack_Id);
       end if;
 
-      Ignore_Pragma_SPARK_Mode := Save_IPSM;
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
    end Analyze_Formal_Package_Declaration;
 
    ---------------------------------
@@ -3622,8 +3627,8 @@ package body Sem_Ch12 is
       Inline_Now        : Boolean := False;
       Has_Inline_Always : Boolean := False;
 
-      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+      Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+      --  Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
 
       Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
       Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
@@ -3865,7 +3870,13 @@ package body Sem_Ch12 is
          --  the instance.
 
          if SPARK_Mode /= On then
-            Ignore_Pragma_SPARK_Mode := True;
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+            --  Mark the instance spec in case the body is instantiated at a
+            --  later pass. This preserves the original context in effect for
+            --  the body.
+
+            Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
          end if;
 
          Gen_Decl := Unit_Declaration_Node (Gen_Unit);
@@ -4433,11 +4444,6 @@ package body Sem_Ch12 is
          Set_Defining_Identifier (N, Act_Decl_Id);
       end if;
 
-      Ignore_Pragma_SPARK_Mode := Save_IPSM;
-      SPARK_Mode               := Save_SM;
-      SPARK_Mode_Pragma        := Save_SMP;
-      Style_Check              := Save_Style_Check;
-
       --  Check that if N is an instantiation of System.Dim_Float_IO or
       --  System.Dim_Integer_IO, the formal type has a dimension system.
 
@@ -4460,6 +4466,11 @@ package body Sem_Ch12 is
          Analyze_Aspect_Specifications (N, Act_Decl_Id);
       end if;
 
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+      SPARK_Mode        := Save_SM;
+      SPARK_Mode_Pragma := Save_SMP;
+      Style_Check       := Save_Style_Check;
+
       if Mode_Set then
          Restore_Ghost_Mode (Mode);
       end if;
@@ -4474,10 +4485,10 @@ package body Sem_Ch12 is
             Restore_Env;
          end if;
 
-         Ignore_Pragma_SPARK_Mode := Save_IPSM;
-         SPARK_Mode               := Save_SM;
-         SPARK_Mode_Pragma        := Save_SMP;
-         Style_Check              := Save_Style_Check;
+         Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+         SPARK_Mode        := Save_SM;
+         SPARK_Mode_Pragma := Save_SMP;
+         Style_Check       := Save_Style_Check;
 
          if Mode_Set then
             Restore_Ghost_Mode (Mode);
@@ -5119,8 +5130,8 @@ package body Sem_Ch12 is
 
       --  Local variables
 
-      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+      Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+      --  Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
 
       Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
       Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
@@ -5201,15 +5212,6 @@ package body Sem_Ch12 is
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
       else
-         --  If the context of the instance is subject to SPARK_Mode "off" or
-         --  the annotation is altogether missing, set the global flag which
-         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-         --  the instance.
-
-         if SPARK_Mode /= On then
-            Ignore_Pragma_SPARK_Mode := True;
-         end if;
-
          Set_Entity (Gen_Id, Gen_Unit);
          Set_Is_Instantiated (Gen_Unit);
 
@@ -5348,6 +5350,22 @@ package body Sem_Ch12 is
          Set_Has_Pragma_Inline_Always
            (Anon_Id,     Has_Pragma_Inline_Always (Gen_Unit));
 
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
+
+         if SPARK_Mode /= On then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+            --  Mark both the instance spec and the anonymous package in case
+            --  the body is instantiated at a later pass. This preserves the
+            --  original context in effect for the body.
+
+            Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
+            Set_Ignore_SPARK_Mode_Pragmas (Anon_Id);
+         end if;
+
          if not Is_Intrinsic_Subprogram (Gen_Unit) then
             Check_Elab_Instantiation (N);
          end if;
@@ -5421,10 +5439,6 @@ package body Sem_Ch12 is
          Env_Installed := False;
          Generic_Renamings.Set_Last (0);
          Generic_Renamings_HTable.Reset;
-
-         Ignore_Pragma_SPARK_Mode := Save_IPSM;
-         SPARK_Mode               := Save_SM;
-         SPARK_Mode_Pragma        := Save_SMP;
       end if;
 
    <<Leave>>
@@ -5432,6 +5446,10 @@ package body Sem_Ch12 is
          Analyze_Aspect_Specifications (N, Act_Decl_Id);
       end if;
 
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+      SPARK_Mode        := Save_SM;
+      SPARK_Mode_Pragma := Save_SMP;
+
       if Mode_Set then
          Restore_Ghost_Mode (Mode);
       end if;
@@ -5446,9 +5464,9 @@ package body Sem_Ch12 is
             Restore_Env;
          end if;
 
-         Ignore_Pragma_SPARK_Mode := Save_IPSM;
-         SPARK_Mode               := Save_SM;
-         SPARK_Mode_Pragma        := Save_SMP;
+         Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+         SPARK_Mode        := Save_SM;
+         SPARK_Mode_Pragma := Save_SMP;
 
          if Mode_Set then
             Restore_Ghost_Mode (Mode);
@@ -10847,7 +10865,8 @@ package body Sem_Ch12 is
       Gen_Decl    : constant Node_Id    := Unit_Declaration_Node (Gen_Unit);
       Loc         : constant Source_Ptr := Sloc (Inst_Node);
 
-      Save_IPSM        : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      Save_ISMP        : constant Boolean :=
+                           Ignore_SPARK_Mode_Pragmas_In_Instance;
       Save_Style_Check : constant Boolean := Style_Check;
 
       procedure Check_Initialized_Types;
@@ -11009,13 +11028,16 @@ package body Sem_Ch12 is
          Save_Env (Gen_Unit, Act_Decl_Id);
          Style_Check := False;
 
-         --  If the context of the instance is subject to SPARK_Mode "off" or
-         --  the annotation is altogether missing, set the global flag which
-         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-         --  the instance.
+         --  If the context of the instance is subject to SPARK_Mode "off", the
+         --  annotation is missing, or the body is instantiated at a later pass
+         --  and its spec ignored SPARK_Mode pragma, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+         --  instance.
 
-         if SPARK_Mode /= On then
-            Ignore_Pragma_SPARK_Mode := True;
+         if SPARK_Mode /= On
+           or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+         then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
          end if;
 
          Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@@ -11186,8 +11208,6 @@ package body Sem_Ch12 is
          end if;
 
          Restore_Env;
-         Ignore_Pragma_SPARK_Mode := Save_IPSM;
-         Style_Check := Save_Style_Check;
 
       --  If we have no body, and the unit requires a body, then complain. This
       --  complaint is suppressed if we have detected other errors (since a
@@ -11209,7 +11229,7 @@ package body Sem_Ch12 is
          --  was already detected, since this can cause blowups.
 
          else
-            return;
+            goto Leave;
          end if;
 
       --  Case of package that does not need a body
@@ -11244,6 +11264,9 @@ package body Sem_Ch12 is
       Expander_Mode_Restore;
 
    <<Leave>>
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+      Style_Check := Save_Style_Check;
+
       Restore_Ghost_Mode (Mode);
    end Instantiate_Package_Body;
 
@@ -11269,8 +11292,9 @@ package body Sem_Ch12 is
       Pack_Id     : constant Entity_Id  :=
                       Defining_Unit_Name (Parent (Act_Decl));
 
-      Saved_IPSM        : constant Boolean        := Ignore_Pragma_SPARK_Mode;
-      Saved_Style_Check : constant Boolean        := Style_Check;
+      Saved_ISMP        : constant Boolean :=
+                            Ignore_SPARK_Mode_Pragmas_In_Instance;
+      Saved_Style_Check : constant Boolean := Style_Check;
       Saved_Warnings    : constant Warning_Record := Save_Warnings;
 
       Act_Body    : Node_Id;
@@ -11363,13 +11387,16 @@ package body Sem_Ch12 is
          Save_Env (Gen_Unit, Act_Decl_Id);
          Style_Check := False;
 
-         --  If the context of the instance is subject to SPARK_Mode "off" or
-         --  the annotation is altogether missing, set the global flag which
-         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
-         --  the instance.
+         --  If the context of the instance is subject to SPARK_Mode "off", the
+         --  annotation is missing, or the body is instantiated at a later pass
+         --  and its spec ignored SPARK_Mode pragma, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+         --  instance.
 
-         if SPARK_Mode /= On then
-            Ignore_Pragma_SPARK_Mode := True;
+         if SPARK_Mode /= On
+           or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+         then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
          end if;
 
          Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@@ -11473,8 +11500,6 @@ package body Sem_Ch12 is
          end if;
 
          Restore_Env;
-         Ignore_Pragma_SPARK_Mode := Saved_IPSM;
-         Style_Check := Saved_Style_Check;
          Restore_Warnings (Saved_Warnings);
 
       --  Body not found. Error was emitted already. If there were no previous
@@ -11549,6 +11574,9 @@ package body Sem_Ch12 is
       Expander_Mode_Restore;
 
    <<Leave>>
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Style_Check := Saved_Style_Check;
+
       Restore_Ghost_Mode (Mode);
    end Instantiate_Subprogram_Body;
 
@@ -11562,12 +11590,12 @@ package body Sem_Ch12 is
       Analyzed_Formal : Node_Id;
       Actual_Decls    : List_Id) return List_Id
    is
-      Gen_T      : constant Entity_Id  := Defining_Identifier (Formal);
       A_Gen_T    : constant Entity_Id  :=
                      Defining_Identifier (Analyzed_Formal);
-      Ancestor   : Entity_Id := Empty;
       Def        : constant Node_Id    := Formal_Type_Definition (Formal);
+      Gen_T      : constant Entity_Id  := Defining_Identifier (Formal);
       Act_T      : Entity_Id;
+      Ancestor   : Entity_Id := Empty;
       Decl_Node  : Node_Id;
       Decl_Nodes : List_Id;
       Loc        : Source_Ptr;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 41f1e53..5bd4a7c 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3298,8 +3298,9 @@ package body Sem_Ch6 is
 
       --  Local variables
 
-      Mode     : Ghost_Mode_Type;
-      Mode_Set : Boolean := False;
+      Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+      Mode      : Ghost_Mode_Type;
+      Mode_Set  : Boolean := False;
 
    --  Start of processing for Analyze_Subprogram_Body_Helper
 
@@ -3371,7 +3372,7 @@ package body Sem_Ch6 is
 
          else
             Enter_Name (Body_Id);
-            return;
+            goto Leave;
          end if;
 
       --  Non-generic case, find the subprogram declaration, if one was seen,
@@ -3381,7 +3382,7 @@ package body Sem_Ch6 is
       --  analysis.
 
       elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
-         return;
+         goto Leave;
 
       else
          Body_Id := Analyze_Subprogram_Specification (Body_Spec);
@@ -3868,6 +3869,29 @@ package body Sem_Ch6 is
          Set_SPARK_Pragma_Inherited (Body_Id);
       end if;
 
+      --  A subprogram 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 initial declaration of the body.
+
+      if Present (Spec_Id) then
+         if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+         end if;
+
+      else
+         --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+         --  case the body 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 (Body_Id);
+
+         elsif Ignore_SPARK_Mode_Pragmas (Body_Id) then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+         end if;
+      end if;
+
       --  If this is the proper body of a stub, we must verify that the stub
       --  conforms to the body, and to the previous spec if one was present.
       --  We know already that the body conforms to that spec. This test is
@@ -4056,6 +4080,7 @@ package body Sem_Ch6 is
                                 Protected_Body_Subprogram (Spec_Id);
             Prot_Ext_Formal : Entity_Id := Extra_Formals (Spec_Id);
             Impl_Ext_Formal : Entity_Id := Extra_Formals (Impl_Subp);
+
          begin
             while Present (Prot_Ext_Formal) loop
                pragma Assert (Present (Impl_Ext_Formal));
@@ -4406,6 +4431,8 @@ package body Sem_Ch6 is
       end if;
 
    <<Leave>>
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
       if Mode_Set then
          Restore_Ghost_Mode (Mode);
       end if;
@@ -4470,6 +4497,15 @@ package body Sem_Ch6 is
          Set_SPARK_Pragma_Inherited (Designator);
       end if;
 
+      --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+      --  the body of this subprogram 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 (Designator);
+      end if;
+
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
          Write_Name (Chars (Designator));
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
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b0810d9..079e52a 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -21689,7 +21689,7 @@ package body Sem_Prag is
             --  enclosing context has SPARK_Mode set to "off", the pragma has
             --  no semantic effect.
 
-            if Ignore_Pragma_SPARK_Mode then
+            if Ignore_SPARK_Mode_Pragmas_In_Instance then
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 69ba0cb..1cadd47 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -3622,11 +3622,21 @@ package body Sem_Util is
       -----------------------
 
       function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
-         Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
+         Id   : constant Entity_Id := Defining_Entity (N);
+         Prag : constant Node_Id   := SPARK_Pragma (Id);
 
       begin
-         return
-           Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+         --  Default the mode to "off" when the context is an instance and all
+         --  SPARK_Mode pragmas found within are to be ignored.
+
+         if Ignore_SPARK_Mode_Pragmas (Id) then
+            return True;
+
+         else
+            return
+              Present (Prag)
+                and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+         end if;
       end SPARK_Mode_Is_Off;
 
    --  Start of processing for Check_State_Refinements