Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 247177)
+++ sem_ch7.adb	(working copy)
@@ -539,6 +539,8 @@
 
       --  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 @@
          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 @@
          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 @@
          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
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 247177)
+++ einfo.adb	(working copy)
@@ -620,7 +620,7 @@
    --    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 @@
       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 @@
       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 @@
       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));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 247177)
+++ einfo.ads	(working copy)
@@ -2164,6 +2164,13 @@
 --       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 @@
    --    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)
+   --    Has_Expanded_Contract               (Flag240)
+   --    Ignore_SPARK_Mode_Pragmas           (Flag301)
+   --    Is_Entry_Wrapper                    (Flag297)
+   --    Needs_No_Actuals                    (Flag22)
    --    Sec_Stack_Needed_For_Return         (Flag167)
-   --    Has_Expanded_Contract               (Flag240)
    --    SPARK_Pragma_Inherited              (Flag265)  (protected kind)
-   --    Is_Entry_Wrapper                    (Flag297)
+   --    Uses_Sec_Stack                      (Flag95)
    --    Address_Clause                      (synth)
    --    Entry_Index_Type                    (synth)
    --    First_Formal                        (synth)
@@ -6056,6 +6064,7 @@
    --    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 @@
    --    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 @@
    --    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 @@
    --    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 @@
    --    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 @@
 
    --  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 @@
    --    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 @@
    --  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 @@
    --    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 @@
    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 @@
    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 @@
    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 @@
    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);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 247179)
+++ sem_prag.adb	(working copy)
@@ -21689,7 +21689,7 @@
             --  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;
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 247177)
+++ sem_ch12.adb	(working copy)
@@ -2605,8 +2605,8 @@
 
       --  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 @@
       --  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 @@
          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 @@
       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 @@
          --  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 @@
          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 @@
          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 @@
             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 @@
 
       --  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 @@
          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 @@
          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 @@
          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 @@
          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 @@
             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 @@
       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 @@
          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 @@
          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 @@
          --  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 @@
       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 @@
       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 @@
          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 @@
          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 @@
       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 @@
       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;
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 247181)
+++ sem_util.adb	(working copy)
@@ -3622,11 +3622,21 @@
       -----------------------
 
       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
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 247177)
+++ sem_ch6.adb	(working copy)
@@ -3298,8 +3298,9 @@
 
       --  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 @@
 
          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 @@
       --  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 @@
          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 @@
                                 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 @@
       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 @@
          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));
Index: opt.ads
===================================================================
--- opt.ads	(revision 247177)
+++ opt.ads	(working copy)
@@ -814,18 +814,18 @@
    --  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
