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, 74 insertions, 32 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 61f05c5..e4dc59e 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -444,11 +444,18 @@ package body Contracts is
    -- Analyze_Entry_Or_Subprogram_Body_Contract --
    -----------------------------------------------
 
+   --  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 Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
       Body_Decl : constant Node_Id   := Unit_Declaration_Node (Body_Id);
       Items     : constant Node_Id   := Contract (Body_Id);
       Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
-      Mode      : SPARK_Mode_Type;
+
+      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
 
    begin
       --  When a subprogram body declaration is illegal, its defining entity is
@@ -473,7 +480,7 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related subprogram body.
 
-      Save_SPARK_Mode_And_Set (Body_Id, Mode);
+      Set_SPARK_Mode (Body_Id);
 
       --  Ensure that the contract cases or postconditions mention 'Result or
       --  define a post-state.
@@ -499,7 +506,7 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      Restore_SPARK_Mode (Mode);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
 
       --  Capture all global references in a generic subprogram body now that
       --  the contract has been analyzed.
@@ -523,6 +530,10 @@ package body Contracts is
    -- Analyze_Entry_Or_Subprogram_Contract --
    ------------------------------------------
 
+   --  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 Analyze_Entry_Or_Subprogram_Contract
      (Subp_Id   : Entity_Id;
       Freeze_Id : Entity_Id := Empty)
@@ -530,6 +541,10 @@ package body Contracts is
       Items     : constant Node_Id := Contract (Subp_Id);
       Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
 
+      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
+
       Skip_Assert_Exprs : constant Boolean :=
                             Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
                               and then not ASIS_Mode
@@ -537,7 +552,6 @@ package body Contracts is
 
       Depends  : Node_Id := Empty;
       Global   : Node_Id := Empty;
-      Mode     : SPARK_Mode_Type;
       Prag     : Node_Id;
       Prag_Nam : Name_Id;
 
@@ -557,7 +571,7 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related subprogram body.
 
-      Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+      Set_SPARK_Mode (Subp_Id);
 
       --  All subprograms carry a contract, but for some it is not significant
       --  and should not be processed.
@@ -667,7 +681,7 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      Restore_SPARK_Mode (Mode);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
 
       --  Capture all global references in a generic subprogram now that the
       --  contract has been analyzed.
@@ -683,21 +697,28 @@ package body Contracts is
    -- Analyze_Object_Contract --
    -----------------------------
 
+   --  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 Analyze_Object_Contract
      (Obj_Id    : Entity_Id;
       Freeze_Id : Entity_Id := Empty)
    is
-      Obj_Typ      : constant Entity_Id := Etype (Obj_Id);
-      AR_Val       : Boolean := False;
-      AW_Val       : Boolean := False;
-      ER_Val       : Boolean := False;
-      EW_Val       : Boolean := False;
-      Items        : Node_Id;
-      Mode         : SPARK_Mode_Type;
-      Prag         : Node_Id;
-      Ref_Elmt     : Elmt_Id;
-      Restore_Mode : Boolean := False;
-      Seen         : Boolean := False;
+      Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+
+      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
+
+      AR_Val   : Boolean := False;
+      AW_Val   : Boolean := False;
+      ER_Val   : Boolean := False;
+      EW_Val   : Boolean := False;
+      Items    : Node_Id;
+      Prag     : Node_Id;
+      Ref_Elmt : Elmt_Id;
+      Seen     : Boolean := False;
 
    begin
       --  The loop parameter in an element iterator over a formal container
@@ -728,8 +749,7 @@ package body Contracts is
       if Is_Single_Concurrent_Object (Obj_Id)
         and then Present (SPARK_Pragma (Obj_Id))
       then
-         Restore_Mode := True;
-         Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+         Set_SPARK_Mode (Obj_Id);
       end if;
 
       --  Constant-related checks
@@ -929,15 +949,17 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      if Restore_Mode then
-         Restore_SPARK_Mode (Mode);
-      end if;
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
    end Analyze_Object_Contract;
 
    -----------------------------------
    -- Analyze_Package_Body_Contract --
    -----------------------------------
 
+   --  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 Analyze_Package_Body_Contract
      (Body_Id   : Entity_Id;
       Freeze_Id : Entity_Id := Empty)
@@ -945,7 +967,11 @@ package body Contracts is
       Body_Decl : constant Node_Id   := Unit_Declaration_Node (Body_Id);
       Items     : constant Node_Id   := Contract (Body_Id);
       Spec_Id   : constant Entity_Id := Spec_Entity (Body_Id);
-      Mode      : SPARK_Mode_Type;
+
+      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
+
       Ref_State : Node_Id;
 
    begin
@@ -964,7 +990,7 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related package body.
 
-      Save_SPARK_Mode_And_Set (Body_Id, Mode);
+      Set_SPARK_Mode (Body_Id);
 
       Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
 
@@ -978,7 +1004,7 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      Restore_SPARK_Mode (Mode);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
 
       --  Capture all global references in a generic package body now that the
       --  contract has been analyzed.
@@ -994,12 +1020,20 @@ package body Contracts is
    -- Analyze_Package_Contract --
    ------------------------------
 
+   --  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 Analyze_Package_Contract (Pack_Id : Entity_Id) is
       Items     : constant Node_Id := Contract (Pack_Id);
       Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
+
+      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
+
       Init      : Node_Id := Empty;
       Init_Cond : Node_Id := Empty;
-      Mode      : SPARK_Mode_Type;
       Prag      : Node_Id;
       Prag_Nam  : Name_Id;
 
@@ -1019,7 +1053,7 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related package.
 
-      Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+      Set_SPARK_Mode (Pack_Id);
 
       if Present (Items) then
 
@@ -1066,7 +1100,7 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      Restore_SPARK_Mode (Mode);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
 
       --  Capture all global references in a generic package now that the
       --  contract has been analyzed.
@@ -1204,10 +1238,18 @@ package body Contracts is
    -- Analyze_Task_Contract --
    ---------------------------
 
+   --  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 Analyze_Task_Contract (Task_Id : Entity_Id) is
       Items : constant Node_Id := Contract (Task_Id);
-      Mode  : SPARK_Mode_Type;
-      Prag  : Node_Id;
+
+      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
+
+      Prag : Node_Id;
 
    begin
       --  Do not analyze a contract multiple times
@@ -1225,7 +1267,7 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related task unit.
 
-      Save_SPARK_Mode_And_Set (Task_Id, Mode);
+      Set_SPARK_Mode (Task_Id);
 
       --  Analyze Global first, as Depends may mention items classified in the
       --  global categorization.
@@ -1248,7 +1290,7 @@ package body Contracts is
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
-      Restore_SPARK_Mode (Mode);
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
    end Analyze_Task_Contract;
 
    -------------------------------------------------