exp_ch3.adb (Expand_N_Full_Type_Declaration): Do not capture, set and restore the Ghost mode.

2015-10-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Full_Type_Declaration): Do not capture,
	set and restore the Ghost mode.
	(Expand_N_Object_Declaration): Do not capture, set and restore the
	Ghost mode.
	(Freeze_Type): Redo the capture and restore of the Ghost mode.
	(Restore_Globals): Removed.
	* exp_ch5.adb (Expand_N_Assignment_Statement): Redo the capture
	and restore of the Ghost mode.
	(Restore_Globals): Removed.
	* exp_ch6.adb (Expand_N_Procedure_Call_Statement):
	Redo the capture and restore of the Ghost mode.
	(Expand_N_Subprogram_Body): Redo the capture, set and restore
	of the Ghost mode.
	(Expand_N_Subprogram_Declaration): Do not
	capture, set and restore the Ghost mode.
	(Restore_Globals): Removed.
	* exp_ch7.adb (Expand_N_Package_Body): Redo the capture, set
	and restore of the Ghost mode.
	(Expand_N_Package_Declaration): Do not capture, set and restore the
	Ghost mode.
	* exp_ch8.adb (Expand_N_Exception_Renaming_Declaration):
	Redo the capture and restore of the Ghost mode.
	(Expand_N_Object_Renaming_Declaration): Redo
	the capture and restore of the Ghost mode.
	(Expand_N_Package_Renaming_Declaration):
	Redo the capture and restore of the Ghost mode.
	(Expand_N_Subprogram_Renaming_Declaration): Redo the capture
	and restore of the Ghost mode.
	* exp_ch11.adb Remove with and use clauses for Ghost.
	(Expand_N_Exception_Declaration): Do not capture, set and restore
	the Ghost mode.
	* exp_disp.adb (Make_DT): Redo the capture and restore of the
	Ghost mode.
	(Restore_Globals): Removed.
	* exp_prag.adb (Expand_Pragma_Check): Do not capture, set
	and restore the Ghost mode.
	(Expand_Pragma_Contract_Cases):
	Redo the capture and restore of the Ghost mode.  Preserve the
	original context of contract cases by setting / resetting the
	In_Assertion_Expr counter.
	(Expand_Pragma_Initial_Condition):
	Redo the capture and restore of the Ghost mode.
	(Expand_Pragma_Loop_Variant): Redo the capture and restore of
	the Ghost mode.
	(Restore_Globals): Removed.
	* exp_util.adb (Make_Predicate_Call): Redo the capture and
	restore of the Ghost mode.
	(Restore_Globals): Removed.
	* freeze.adb (Freeze_Entity): Redo the capture and restore of
	the Ghost mode.
	(Restore_Globals): Removed.
	* ghost.adb (Check_Ghost_Context): Remove the RM reference from
	the error message.
	(Is_OK_Statement): Account for statements
	that appear in assertion expressions.
	(Is_Subject_To_Ghost):
	Moved from spec.
	* ghost.ads (Is_Subject_To_Ghost): Moved to body.
	* rtsfind.ads (Load_RTU): Redo the capture and restore of the
	Ghost mode.
	* sem.adb Add with and use clauses for Ghost.
	(Analyze): Redo
	the capture and restore of the Ghost mode. Set the Ghost mode
	when analyzing a declaration.
	(Do_Analyze): Redo the capture
	and restore of the Ghost mode.
	* sem_ch3.adb (Analyze_Full_Type_Declaration): Do not capture, set
	and restore the Ghost mode.
	(Analyze_Incomplete_Type_Decl):
	Do not capture, set and restore the Ghost mode.
	(Analyze_Number_Declaration): Do not capture, set and restore the
	Ghost mode.
	(Analyze_Object_Declaration): Do not capture, set and
	restore the Ghost mode.
	(Analyze_Private_Extension_Declaration):
	Do not capture, set and restore the Ghost mode.
	(Analyze_Subtype_Declaration): Do not capture, set and restore
	the Ghost mode.
	(Restore_Globals): Removed.
	* sem_ch5.adb (Analyze_Assignment): Redo the capture and restore
	of the Ghost mode.
	(Restore_Globals): Removed.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
	Do not capture, set and restore the Ghost mode.
	(Analyze_Procedure_Call): Redo the capture and restore of the
	Ghost mode.
	(Analyze_Subprogram_Body_Helper): Redo the capture
	and restore of the Ghost mode.	(Analyze_Subprogram_Declaration):
	Do not capture, set and restore the Ghost mode.
	(Restore_Globals): Removed.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Redo the capture and
	restore of the Ghost mode.
	(Analyze_Package_Declaration):
	Do not capture, set and restore the Ghost mode.
	(Analyze_Private_Type_Declaration): Do not capture, set and
	restore the Ghost mode.
	(Restore_Globals): Removed.
	* sem_ch8.adb (Analyze_Exception_Renaming): Do not capture,
	set and restore the Ghost mode.
	(Analyze_Generic_Renaming): Do not capture, set and restore the Ghost
	mode.
	(Analyze_Object_Renaming): Do not capture, set and restore the
	Ghost mode.
	(Analyze_Package_Renaming): Do not capture, set and restore the Ghost
	mode.
	(Analyze_Subprogram_Renaming): Do not capture, set and restore the
	Ghost mode.
	(Restore_Globals): Removed.
	* sem_ch11.adb (Analyze_Exception_Declaration): Do not capture,
	set and restore the Ghost mode.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration):
	Do not capture, set and restore the Ghost mode.
	(Analyze_Generic_Subprogram_Declaration): Do not capture, set
	and restore the Ghost mode.
	* sem_ch13.adb (Build_Invariant_Procedure_Declaration): Redo
	the capture and restore of the Ghost mode.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Redo the capture and restore of the Ghost mode.
	(Analyze_External_Property_In_Decl_Part):
	Redo the capture and restore of the Ghost mode.
	(Analyze_Initial_Condition_In_Decl_Part): Redo the
	capture and restore of the Ghost mode.	(Analyze_Pragma):
	Do not capture, set and restore the Ghost mode for Assert.
	Redo the capture and restore of the Ghost mode for Check. Do
	not capture and restore the Ghost mode for Invariant.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Redo the capture and
	restore of the Ghost mode.
	* sem_res.adb (Resolve): Capture, set and restore the Ghost mode
	when resolving a declaration.
	* sem_util.adb (Build_Default_Init_Cond_Procedure_Body):
	Redo the capture and restore of the Ghost mode.
	(Build_Default_Init_Cond_Procedure_Declaration): Redo the capture
	and restore of the Ghost mode.

From-SVN: r228871

1 files changed, 28 insertions, 56 deletions

diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index a797f23..e80b5b9 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -303,9 +303,8 @@ package body Exp_Prag is
    --------------------------
 
    procedure Expand_Pragma_Check (N : Node_Id) is
-      GM   : constant Ghost_Mode_Type := Ghost_Mode;
-      Cond : constant Node_Id         := Arg2 (N);
-      Nam  : constant Name_Id         := Chars (Arg1 (N));
+      Cond : constant Node_Id := Arg2 (N);
+      Nam  : constant Name_Id := Chars (Arg1 (N));
       Msg  : Node_Id;
 
       Loc : constant Source_Ptr := Sloc (First_Node (Cond));
@@ -329,16 +328,6 @@ package body Exp_Prag is
          return;
       end if;
 
-      --  Set the Ghost mode in effect from the pragma. In general both the
-      --  assertion policy and the Ghost policy of pragma Check must agree,
-      --  but there are cases where this can be circumvented. For instance,
-      --  a living subtype with an ignored predicate may be declared in one
-      --  packade, an ignored Ghost object in another and the compilation may
-      --  use -gnata to enable assertions.
-      --  ??? Ghost predicates are under redesign
-
-      Set_Ghost_Mode (N);
-
       --  Since this check is active, we rewrite the pragma into a
       --  corresponding if statement, and then analyze the statement.
 
@@ -502,11 +491,6 @@ package body Exp_Prag is
             Error_Msg_N ("?A?check will fail at run time", N);
          end if;
       end if;
-
-      --  Restore the original Ghost mode once analysis and expansion have
-      --  taken place.
-
-      Ghost_Mode := GM;
    end Expand_Pragma_Check;
 
    ---------------------------------
@@ -992,7 +976,8 @@ package body Exp_Prag is
 
       Aggr : constant Node_Id :=
                Expression (First (Pragma_Argument_Associations (CCs)));
-      GM   : constant Ghost_Mode_Type := Ghost_Mode;
+
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
 
       Case_Guard    : Node_Id;
       CG_Checks     : Node_Id;
@@ -1027,12 +1012,20 @@ package body Exp_Prag is
          return;
       end if;
 
-      --  The contract cases may be subject to pragma Ghost with policy Ignore.
-      --  Set the mode now to ensure that any nodes generated during expansion
-      --  are properly flagged as ignored Ghost.
+      --  The contract cases is Ghost when it applies to a Ghost entity. Set
+      --  the mode now to ensure that any nodes generated during expansion are
+      --  properly flagged as Ghost.
 
       Set_Ghost_Mode (CCs);
 
+      --  The expansion of contract cases is quite distributed as it produces
+      --  various statements to evaluate the case guards and consequences. To
+      --  preserve the original context, set the Is_Assertion_Expr flag. This
+      --  aids the Ghost legality checks when verifying the placement of a
+      --  reference to a Ghost entity.
+
+      In_Assertion_Expr := In_Assertion_Expr + 1;
+
       Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
 
       --  Create the counter which tracks the number of case guards that
@@ -1258,10 +1251,8 @@ package body Exp_Prag is
 
       Append_To (Stmts, Conseq_Checks);
 
-      --  Restore the original Ghost mode once analysis and expansion have
-      --  taken place.
-
-      Ghost_Mode := GM;
+      In_Assertion_Expr := In_Assertion_Expr - 1;
+      Ghost_Mode := Save_Ghost_Mode;
    end Expand_Pragma_Contract_Cases;
 
    ---------------------------------------
@@ -1361,22 +1352,6 @@ package body Exp_Prag is
    -------------------------------------
 
    procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
-      GM : constant Ghost_Mode_Type := Ghost_Mode;
-
-      procedure Restore_Globals;
-      --  Restore the values of all saved global variables
-
-      ---------------------
-      -- Restore_Globals --
-      ---------------------
-
-      procedure Restore_Globals is
-      begin
-         Ghost_Mode := GM;
-      end Restore_Globals;
-
-      --  Local variables
-
       Loc       : constant Source_Ptr := Sloc (Spec_Or_Body);
       Check     : Node_Id;
       Expr      : Node_Id;
@@ -1384,7 +1359,7 @@ package body Exp_Prag is
       List      : List_Id;
       Pack_Id   : Entity_Id;
 
-   --  Start of processing for Expand_Pragma_Initial_Condition
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
 
    begin
       if Nkind (Spec_Or_Body) = N_Package_Body then
@@ -1424,9 +1399,9 @@ package body Exp_Prag is
 
       Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
 
-      --  The initial condition be subject to pragma Ghost with policy Ignore.
-      --  Set the mode now to ensure that any nodes generated during expansion
-      --  are properly flagged as ignored Ghost.
+      --  The initial condition is Ghost when it applies to a Ghost entity. Set
+      --  the mode now to ensure that any nodes generated during expansion are
+      --  properly flagged as Ghost.
 
       Set_Ghost_Mode (Init_Cond);
 
@@ -1442,7 +1417,7 @@ package body Exp_Prag is
       --  runtime check as it will repeat the illegality.
 
       if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
-         Restore_Globals;
+         Ghost_Mode := Save_Ghost_Mode;
          return;
       end if;
 
@@ -1461,7 +1436,7 @@ package body Exp_Prag is
       Append_To (List, Check);
       Analyze (Check);
 
-      Restore_Globals;
+      Ghost_Mode := Save_Ghost_Mode;
    end Expand_Pragma_Initial_Condition;
 
    ------------------------------------
@@ -1811,7 +1786,7 @@ package body Exp_Prag is
 
       --  Local variables
 
-      GM : constant Ghost_Mode_Type := Ghost_Mode;
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
 
    --  Start of processing for Expand_Pragma_Loop_Variant
 
@@ -1825,9 +1800,9 @@ package body Exp_Prag is
          return;
       end if;
 
-      --  The loop variant may be subject to pragma Ghost with policy Ignore.
-      --  Set the mode now to ensure that any nodes generated during expansion
-      --  are properly flagged as ignored Ghost.
+      --  The loop variant is Ghost when it applies to a Ghost entity. Set
+      --  the mode now to ensure that any nodes generated during expansion
+      --  are properly flagged as Ghost.
 
       Set_Ghost_Mode (N);
 
@@ -1892,10 +1867,7 @@ package body Exp_Prag is
       --  corresponding declarations and statements. We leave it in the tree
       --  for documentation purposes. It will be ignored by the backend.
 
-      --  Restore the original Ghost mode once analysis and expansion have
-      --  taken place.
-
-      Ghost_Mode := GM;
+      Ghost_Mode := Save_Ghost_Mode;
    end Expand_Pragma_Loop_Variant;
 
    --------------------------------