contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Add a warning about SPARK mode management.

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

	* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
	Add a warning about SPARK mode management. The routine now
	saves and restores both the mode and associated pragma.
	(Analyze_Entry_Or_Subprogram_Contract): Add a warning about
	SPARK mode management. The routine now saves and restores both
	the mode and associated pragma.
	(Analyze_Object_Contract):
	Add a warning about SPARK mode management. The routine
	now saves and restores both the mode and associated pragma.
	(Analyze_Package_Body_Contract): Add a warning about SPARK mode
	management.  The routine now saves and restores both the mode
	and associated pragma.	(Analyze_Package_Contract): Add a warning
	about SPARK mode management. The routine now saves and restores
	both the mode and associated pragma.
	(Analyze_Task_Contract):
	Add a warning about SPARK mode management. The routine now saves
	and restores both the mode and associated pragma.
	* expander.adb (Expand): Change the way the Ghost mode is saved
	and restored.
	* exp_ch3.adb (Freeze_Type): Change the way the Ghost mode is
	saved and restored.
	* exp_disp.adb (Make_DT): Change the way the Ghost mode is saved
	and restored.
	* exp_util.adb (Build_DIC_Procedure_Body):
	Change the way the Ghost mode is saved and restored.
	(Build_DIC_Procedure_Declaration): Change the way the Ghost
	mode is saved and restored.
	(Build_Invariant_Procedure_Body):
	Change the way the Ghost mode is saved and restored.
	(Build_Invariant_Procedure_Declaration): Change the way the Ghost
	mode is saved and restored.
	(Make_Predicate_Call): Change the
	way the Ghost mode is saved and restored.
	* freeze.adb (Freeze_Entity): Change the way the Ghost mode is
	saved and restored.
	* ghost.adb (Mark_And_Set_Ghost_Assignment): Remove parameter Mode
	and its assignment.
	(Mark_And_Set_Ghost_Body): Remove parameter
	Mode and its assignment.
	(Mark_And_Set_Ghost_Completion):
	Remove parameter Mode and its assignment.
	(Mark_And_Set_Ghost_Declaration): Remove parameter Mode and its
	assignment.
	(Mark_And_Set_Ghost_Instantiation): Remove parameter
	Mode and its assignment.
	(Mark_And_Set_Ghost_Procedure_Call):
	Remove parameter Mode and its assignment.
	(Set_Ghost_Mode):
	Remove parameter Mode and its assignment.
	* ghost.ads (Mark_And_Set_Ghost_Assignment): Remove parameter Mode
	and update the comment on usage.
	(Mark_And_Set_Ghost_Body):
	Remove parameter Mode and update the comment on usage.
	(Mark_And_Set_Ghost_Completion): Remove parameter Mode and
	update the comment on usage.
	(Mark_And_Set_Ghost_Declaration):
	Remove parameter Mode and update the comment on usage.
	(Mark_And_Set_Ghost_Instantiation): Remove parameter Mode and
	update the comment on usage.
	(Mark_And_Set_Ghost_Procedure_Call):
	Remove parameter Mode and update the comment on usage.
	(Set_Ghost_Mode): Remove parameter Mode and update the comment
	on usage.
	* lib.ads Remove obsolete fields SPARK_Mode_Pragma from various
	types.
	* lib-load.adb (Create_Dummy_Package_Unit): Remove the assignment
	of obsolete field SPARK_Mode_Pragma.
	(Load_Main_Source): Remove
	the assignment of obsolete field SPARK_Mode_Pragma.
	(Load_Unit): Remove the assignment of obsolete field SPARK_Mode_Pragma.
	* lib-writ.adb (Add_Preprocessing_Dependency): Remove
	the assignment of obsolete field SPARK_Mode_Pragma.
	(Ensure_System_Dependency): Remove the assignment of obsolete
	field SPARK_Mode_Pragma.
	* rtsfind.adb (Load_RTU): Add a warning about Ghost and SPARK
	mode management. Change the way Ghost and SPARK modes are saved
	and restored.
	* sem.adb (Analyze): Change the way the Ghost mode is saved
	and restored.
	* sem_ch3.adb (Analyze_Object_Declaration): Change the way the
	Ghost mode is saved and restored.
	(Process_Full_View): Change
	the way the Ghost mode is saved and restored.
	* sem_ch5.adb (Analyze_Assignment): Change the way the Ghost
	mode is saved and restored.
	* sem_ch6.adb (Analyze_Procedure_Call): Change the way the Ghost
	mode is saved and restored.
	(Analyze_Subprogram_Body_Helper):
	Change the way the Ghost mode is saved and restored.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Change the way the
	Ghost mode is saved and restored.
	* sem_ch10.adb (Analyze_Subunit): Add a warning about SPARK mode
	management. Save the SPARK mode-related data prior to any changes
	to the scope stack and contexts. The mode is then reinstalled
	before the subunit is analyzed in order to restore the original
	view of the subunit.
	* sem_ch12.adb (Analyze_Package_Instantiation): Update the
	warning on region management.  Change the way the Ghost and
	SPARK modes are saved and restored.
	(Inline_Instance_Body):
	Add a warning about SPARK mode management. Code clean up.
	(Analyze_Subprogram_Instantiation): Update the warning on region
	management.  Change the way the Ghost and SPARK modes are saved
	and restored.
	(Instantiate_Package_Body): Update the warning
	on region management. Change the way the Ghost and SPARK modes
	are saved and restored.
	(Instantiate_Subprogram_Body): Update
	the warning on region management. Change the way the Ghost and
	SPARK modes are saved and restored.
	(Set_Instance_Env): Add a
	warning about SPARK mode management. Change the way SPARK mode
	is saved and restored.
	* sem_ch13.adb (Build_Predicate_Functions):
	Change the way the Ghost mode is saved and restored.
	(Build_Predicate_Function_Declaration): Change the way the Ghost
	mode is saved and restored.
	* sem_elab.adb (Check_Elab_Calls): Add a warning about SPARK
	mode management. Change the way SPARK mode is saved and restored.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Change the way the Ghost mode is saved and restored.
	(Analyze_Initial_Condition_In_Decl_Part): Change the way
	the Ghost mode is saved and restored.
	(Analyze_Pragma):
	Change the way the Ghost mode is saved and restored.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Change the way the
	Ghost mode is saved and restored.
	* sem_util.adb (Install_SPARK_Mode): New routine.
	(Restore_SPARK_Mode): New routine.
	(Save_SPARK_Mode_And_Set): Removed.
	(Set_SPARK_Mode): New routine.
	* sem_util.ads (Install_SPARK_Mode): New routine.
	(Restore_SPARK_Mode): New routine.
	(Save_SPARK_Mode_And_Set): Removed.
	(Set_SPARK_Mode): New routine.

From-SVN: r247230

1 files changed, 139 insertions, 145 deletions

diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 2f2262d..e598137 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3598,49 +3598,17 @@ package body Sem_Ch12 is
    -- Analyze_Package_Instantiation --
    -----------------------------------
 
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
+   --  WARNING: This routine manages Ghost and SPARK regions. Return statements
+   --  must be replaced by gotos which jump to the end of the routine in order
+   --  to restore the Ghost and SPARK modes.
 
    procedure Analyze_Package_Instantiation (N : Node_Id) is
-      Loc    : constant Source_Ptr := Sloc (N);
-      Gen_Id : constant Node_Id    := Name (N);
-
-      Act_Decl      : Node_Id;
-      Act_Decl_Name : Node_Id;
-      Act_Decl_Id   : Entity_Id;
-      Act_Spec      : Node_Id;
-      Act_Tree      : Node_Id;
-
-      Gen_Decl : Node_Id;
-      Gen_Spec : Node_Id;
-      Gen_Unit : Entity_Id;
-
-      Is_Actual_Pack : constant Boolean :=
-                         Is_Internal (Defining_Entity (N));
-
-      Env_Installed     : Boolean := False;
-      Parent_Installed  : Boolean := False;
-      Renaming_List     : List_Id;
-      Unit_Renaming     : Node_Id;
-      Needs_Body        : Boolean;
-      Inline_Now        : Boolean := False;
       Has_Inline_Always : Boolean := False;
 
-      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;
-      --  Save the SPARK_Mode-related data for restore on exit
-
-      Save_Style_Check : constant Boolean := Style_Check;
-      --  Save style check mode for restore on exit
-
       procedure Delay_Descriptors (E : Entity_Id);
       --  Delay generation of subprogram descriptors for given entity
 
-      function Might_Inline_Subp return Boolean;
+      function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean;
       --  If inlining is active and the generic contains inlined subprograms,
       --  we instantiate the body. This may cause superfluous instantiations,
       --  but it is simpler than detecting the need for the body at the point
@@ -3662,7 +3630,7 @@ package body Sem_Ch12 is
       -- Might_Inline_Subp --
       -----------------------
 
-      function Might_Inline_Subp return Boolean is
+      function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean is
          E : Entity_Id;
 
       begin
@@ -3691,8 +3659,35 @@ package body Sem_Ch12 is
 
       --  Local declarations
 
-      Mode     : Ghost_Mode_Type;
-      Mode_Set : Boolean := False;
+      Gen_Id         : constant Node_Id    := Name (N);
+      Is_Actual_Pack : constant Boolean    :=
+                         Is_Internal (Defining_Entity (N));
+      Loc            : constant Source_Ptr := Sloc (N);
+
+      Saved_GM   : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_ISMP : constant Boolean         :=
+                     Ignore_SPARK_Mode_Pragmas_In_Instance;
+      Saved_SM   : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP  : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the Ghost and SPARK mode-related data to restore on exit
+
+      Saved_Style_Check : constant Boolean := Style_Check;
+      --  Save style check mode for restore on exit
+
+      Act_Decl         : Node_Id;
+      Act_Decl_Name    : Node_Id;
+      Act_Decl_Id      : Entity_Id;
+      Act_Spec         : Node_Id;
+      Act_Tree         : Node_Id;
+      Env_Installed    : Boolean := False;
+      Gen_Decl         : Node_Id;
+      Gen_Spec         : Node_Id;
+      Gen_Unit         : Entity_Id;
+      Inline_Now       : Boolean := False;
+      Needs_Body       : Boolean;
+      Parent_Installed : Boolean := False;
+      Renaming_List    : List_Id;
+      Unit_Renaming    : Node_Id;
 
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
@@ -3771,8 +3766,7 @@ package body Sem_Ch12 is
       --  any nodes generated during analysis and expansion are marked as
       --  Ghost.
 
-      Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
-      Mode_Set := True;
+      Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
 
       --  Verify that it is the name of a generic package
 
@@ -4049,7 +4043,7 @@ package body Sem_Ch12 is
             if Expander_Active
               and then (not Is_Child_Unit (Gen_Unit)
                          or else not Is_Generic_Unit (Scope (Gen_Unit)))
-              and then Might_Inline_Subp
+              and then Might_Inline_Subp (Gen_Unit)
               and then not Is_Actual_Pack
             then
                if not Back_End_Inlining
@@ -4098,7 +4092,8 @@ package body Sem_Ch12 is
               (Unit_Requires_Body (Gen_Unit)
                 or else Enclosing_Body_Present
                 or else Present (Corresponding_Body (Gen_Decl)))
-               and then (Is_In_Main_Unit (N) or else Might_Inline_Subp)
+               and then (Is_In_Main_Unit (N)
+                          or else Might_Inline_Subp (Gen_Unit))
                and then not Is_Actual_Pack
                and then not Inline_Now
                and then (Operating_Mode = Generate_Code
@@ -4466,14 +4461,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;
-      Style_Check       := Save_Style_Check;
-
-      if Mode_Set then
-         Restore_Ghost_Mode (Mode);
-      end if;
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Mode (Saved_GM);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+      Style_Check := Saved_Style_Check;
 
    exception
       when Instantiation_Error =>
@@ -4485,20 +4476,20 @@ package body Sem_Ch12 is
             Restore_Env;
          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;
+         Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+         Restore_Ghost_Mode (Saved_GM);
+         Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+         Style_Check := Saved_Style_Check;
    end Analyze_Package_Instantiation;
 
    --------------------------
    -- Inline_Instance_Body --
    --------------------------
 
+   --  WARNING: This routine manages SPARK regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  SPARK mode.
+
    procedure Inline_Instance_Body
      (N        : Node_Id;
       Gen_Unit : Entity_Id;
@@ -4509,26 +4500,27 @@ package body Sem_Ch12 is
       Gen_Comp  : constant Entity_Id :=
                     Cunit_Entity (Get_Source_Unit (Gen_Unit));
 
-      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
-      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
-      --  Save all SPARK_Mode-related attributes as removing enclosing scopes
-      --  to provide a clean environment for analysis of the inlined body will
-      --  eliminate any previously set SPARK_Mode.
+      Saved_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK mode-related data to restore on exit. Removing
+      --  enclosing scopes to provide a clean environment for analysis of
+      --  the inlined body will eliminate any previously set SPARK_Mode.
 
       Scope_Stack_Depth : constant Pos :=
                             Scope_Stack.Last - Scope_Stack.First + 1;
 
-      Use_Clauses  : array (1 .. Scope_Stack_Depth) of Node_Id;
-      Instances    : array (1 .. Scope_Stack_Depth) of Entity_Id;
       Inner_Scopes : array (1 .. Scope_Stack_Depth) of Entity_Id;
-      Curr_Scope   : Entity_Id := Empty;
-      List         : Elist_Id;
-      Num_Inner    : Nat := 0;
-      Num_Scopes   : Nat := 0;
-      N_Instances  : Nat := 0;
-      Removed      : Boolean := False;
-      S            : Entity_Id;
-      Vis          : Boolean;
+      Instances    : array (1 .. Scope_Stack_Depth) of Entity_Id;
+      Use_Clauses  : array (1 .. Scope_Stack_Depth) of Node_Id;
+
+      Curr_Scope  : Entity_Id := Empty;
+      List        : Elist_Id;
+      N_Instances : Nat := 0;
+      Num_Inner   : Nat := 0;
+      Num_Scopes  : Nat := 0;
+      Removed     : Boolean := False;
+      S           : Entity_Id;
+      Vis         : Boolean;
 
    begin
       --  Case of generic unit defined in another unit. We must remove the
@@ -4672,8 +4664,8 @@ package body Sem_Ch12 is
                Version                  => Ada_Version,
                Version_Pragma           => Ada_Version_Pragma,
                Warnings                 => Save_Warnings,
-               SPARK_Mode               => Save_SM,
-               SPARK_Mode_Pragma        => Save_SMP)),
+               SPARK_Mode               => Saved_SM,
+               SPARK_Mode_Pragma        => Saved_SMP)),
             Inlined_Body => True);
 
          Pop_Scope;
@@ -4812,7 +4804,6 @@ package body Sem_Ch12 is
      (N    : Node_Id;
       Subp : Entity_Id) return Boolean
    is
-
       function Is_Inlined_Or_Child_Of_Inlined (E : Entity_Id) return Boolean;
       --  Return True if E is an inlined subprogram, an inlined renaming or a
       --  subprogram nested in an inlined subprogram. The inlining machinery
@@ -4882,9 +4873,9 @@ package body Sem_Ch12 is
    -- Analyze_Subprogram_Instantiation --
    --------------------------------------
 
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
+   --  WARNING: This routine manages Ghost and SPARK regions. Return statements
+   --  must be replaced by gotos which jump to the end of the routine in order
+   --  to restore the Ghost and SPARK modes.
 
    procedure Analyze_Subprogram_Instantiation
      (N : Node_Id;
@@ -5130,15 +5121,12 @@ package body Sem_Ch12 is
 
       --  Local variables
 
-      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;
-      --  Save the SPARK_Mode-related data for restore on exit
-
-      Mode     : Ghost_Mode_Type;
-      Mode_Set : Boolean := False;
+      Saved_GM   : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_ISMP : constant Boolean         :=
+                     Ignore_SPARK_Mode_Pragmas_In_Instance;
+      Saved_SM   : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP  : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the Ghost and SPARK mode-related data to restore on exit
 
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
@@ -5180,8 +5168,7 @@ package body Sem_Ch12 is
       --  that any nodes generated during analysis and expansion are marked as
       --  Ghost.
 
-      Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
-      Mode_Set := True;
+      Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
 
       Generate_Reference (Gen_Unit, Gen_Id);
 
@@ -5446,13 +5433,9 @@ 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;
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Mode (Saved_GM);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
 
    exception
       when Instantiation_Error =>
@@ -5464,13 +5447,9 @@ package body Sem_Ch12 is
             Restore_Env;
          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;
+         Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+         Restore_Ghost_Mode (Saved_GM);
+         Restore_SPARK_Mode (Saved_SM, Saved_SMP);
    end Analyze_Subprogram_Instantiation;
 
    -------------------------
@@ -10847,9 +10826,9 @@ package body Sem_Ch12 is
    -- Instantiate_Package_Body --
    ------------------------------
 
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
+   --  WARNING: This routine manages Ghost and SPARK regions. Return statements
+   --  must be replaced by gotos which jump to the end of the routine in order
+   --  to restore the Ghost and SPARK modes.
 
    procedure Instantiate_Package_Body
      (Body_Info     : Pending_Body_Info;
@@ -10865,9 +10844,9 @@ package body Sem_Ch12 is
       Gen_Decl    : constant Node_Id    := Unit_Declaration_Node (Gen_Unit);
       Loc         : constant Source_Ptr := Sloc (Inst_Node);
 
-      Save_ISMP        : constant Boolean :=
+      Saved_ISMP        : constant Boolean :=
                            Ignore_SPARK_Mode_Pragmas_In_Instance;
-      Save_Style_Check : constant Boolean := Style_Check;
+      Saved_Style_Check : constant Boolean := Style_Check;
 
       procedure Check_Initialized_Types;
       --  In a generic package body, an entity of a generic private type may
@@ -10939,15 +10918,18 @@ package body Sem_Ch12 is
 
       --  Local variables
 
-      Act_Body      : Node_Id;
-      Act_Body_Id   : Entity_Id;
-      Act_Body_Name : Node_Id;
-      Gen_Body      : Node_Id;
-      Gen_Body_Id   : Node_Id;
-      Mode          : Ghost_Mode_Type;
-      Par_Ent       : Entity_Id := Empty;
-      Par_Vis       : Boolean   := False;
-
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the Ghost and SPARK mode-related data to restore on exit
+
+      Act_Body         : Node_Id;
+      Act_Body_Id      : Entity_Id;
+      Act_Body_Name    : Node_Id;
+      Gen_Body         : Node_Id;
+      Gen_Body_Id      : Node_Id;
+      Par_Ent          : Entity_Id := Empty;
+      Par_Vis          : Boolean   := False;
       Parent_Installed : Boolean := False;
 
       Vis_Prims_List : Elist_Id := No_Elist;
@@ -10970,7 +10952,7 @@ package body Sem_Ch12 is
       --  the mode now to ensure that any nodes generated during instantiation
       --  are properly marked as Ghost.
 
-      Set_Ghost_Mode (Act_Decl_Id, Mode);
+      Set_Ghost_Mode (Act_Decl_Id);
 
       Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
 
@@ -10984,8 +10966,10 @@ package body Sem_Ch12 is
       Opt.Ada_Version          := Body_Info.Version;
       Opt.Ada_Version_Pragma   := Body_Info.Version_Pragma;
       Restore_Warnings (Body_Info.Warnings);
-      Opt.SPARK_Mode           := Body_Info.SPARK_Mode;
-      Opt.SPARK_Mode_Pragma    := Body_Info.SPARK_Mode_Pragma;
+
+      --  Install the SPARK mode which applies to the package body
+
+      Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
 
       if No (Gen_Body_Id) then
 
@@ -11264,19 +11248,19 @@ 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);
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Mode (Saved_GM);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+      Style_Check := Saved_Style_Check;
    end Instantiate_Package_Body;
 
    ---------------------------------
    -- Instantiate_Subprogram_Body --
    ---------------------------------
 
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
+   --  WARNING: This routine manages Ghost and SPARK regions. Return statements
+   --  must be replaced by gotos which jump to the end of the routine in order
+   --  to restore the Ghost and SPARK modes.
 
    procedure Instantiate_Subprogram_Body
      (Body_Info     : Pending_Body_Info;
@@ -11292,16 +11276,20 @@ package body Sem_Ch12 is
       Pack_Id     : constant Entity_Id  :=
                       Defining_Unit_Name (Parent (Act_Decl));
 
-      Saved_ISMP        : constant Boolean :=
-                            Ignore_SPARK_Mode_Pragmas_In_Instance;
-      Saved_Style_Check : constant Boolean := Style_Check;
+      Saved_GM   : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_ISMP : constant Boolean         :=
+                     Ignore_SPARK_Mode_Pragmas_In_Instance;
+      Saved_SM   : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP  : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the Ghost and SPARK mode-related data to restore on exit
+
+      Saved_Style_Check : constant Boolean        := Style_Check;
       Saved_Warnings    : constant Warning_Record := Save_Warnings;
 
       Act_Body    : Node_Id;
       Act_Body_Id : Entity_Id;
       Gen_Body    : Node_Id;
       Gen_Body_Id : Node_Id;
-      Mode        : Ghost_Mode_Type;
       Pack_Body   : Node_Id;
       Par_Ent     : Entity_Id := Empty;
       Par_Vis     : Boolean   := False;
@@ -11324,7 +11312,7 @@ package body Sem_Ch12 is
       --  the mode now to ensure that any nodes generated during instantiation
       --  are properly marked as Ghost.
 
-      Set_Ghost_Mode (Act_Decl_Id, Mode);
+      Set_Ghost_Mode (Act_Decl_Id);
 
       Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
 
@@ -11338,8 +11326,10 @@ package body Sem_Ch12 is
       Opt.Ada_Version          := Body_Info.Version;
       Opt.Ada_Version_Pragma   := Body_Info.Version_Pragma;
       Restore_Warnings (Body_Info.Warnings);
-      Opt.SPARK_Mode           := Body_Info.SPARK_Mode;
-      Opt.SPARK_Mode_Pragma    := Body_Info.SPARK_Mode_Pragma;
+
+      --  Install the SPARK mode which applies to the subprogram body
+
+      Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
 
       if No (Gen_Body_Id) then
 
@@ -11575,9 +11565,9 @@ package body Sem_Ch12 is
 
    <<Leave>>
       Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Mode (Saved_GM);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
       Style_Check := Saved_Style_Check;
-
-      Restore_Ghost_Mode (Mode);
    end Instantiate_Subprogram_Body;
 
    ----------------------
@@ -15413,13 +15403,18 @@ package body Sem_Ch12 is
    -- Set_Instance_Env --
    ----------------------
 
+   --  WARNING: This routine manages SPARK regions
+
    procedure Set_Instance_Env
      (Gen_Unit : Entity_Id;
       Act_Unit : Entity_Id)
    is
-      Assertion_Status       : constant Boolean := Assertions_Enabled;
-      Save_SPARK_Mode        : constant SPARK_Mode_Type := SPARK_Mode;
-      Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma;
+      Saved_AE  : constant Boolean         := Assertions_Enabled;
+      Saved_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK mode-related data because utilizing the configuration
+      --  values of pragmas and switches will eliminate any previously set
+      --  SPARK_Mode.
 
    begin
       --  Regardless of the current mode, predefined units are analyzed in the
@@ -15440,14 +15435,13 @@ package body Sem_Ch12 is
          --  as is already the case for some numeric libraries.
 
          if Ada_Version >= Ada_2012 then
-            Assertions_Enabled := Assertion_Status;
+            Assertions_Enabled := Saved_AE;
          end if;
 
-         --  SPARK_Mode for an instance is the one applicable at the point of
+         --  Reinstall the SPARK_Mode which was in effect at the point of
          --  instantiation.
 
-         SPARK_Mode := Save_SPARK_Mode;
-         SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
+         Install_SPARK_Mode (Saved_SM, Saved_SMP);
       end if;
 
       Current_Instantiated_Parent :=