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, 30 insertions, 14 deletions

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 05295a0..7380d9a 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -67,6 +67,12 @@ package body Ghost is
    --  Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
    --  a reference to a Ghost entity. Return Empty if there is no such entity.
 
+   function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
+   --  Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
+   --  declaration or body N is subject to aspect or pragma Ghost. Use this
+   --  routine in cases where [source] pragma Ghost has not been analyzed yet,
+   --  but the context needs to establish the "ghostness" of N.
+
    procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
    --  Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
    --  Signal all enclosing scopes that they now contain ignored Ghost code.
@@ -407,15 +413,27 @@ package body Ghost is
 
             --  Special cases
 
-            --  An if statement is a suitable context for a Ghost entity if it
-            --  is the byproduct of assertion expression expansion.
+            elsif Nkind (Stmt) = N_If_Statement then
 
-            elsif Nkind (Stmt) = N_If_Statement
-              and then Nkind (Original_Node (Stmt)) = N_Pragma
-              and then Assertion_Expression_Pragma
-                         (Get_Pragma_Id (Original_Node (Stmt)))
-            then
-               return True;
+               --  An if statement is a suitable context for a Ghost entity if
+               --  it is the byproduct of assertion expression expansion. Note
+               --  that the assertion expression may not be related to a Ghost
+               --  entity, but it may still contain references to Ghost
+               --  entities.
+
+               if Nkind (Original_Node (Stmt)) = N_Pragma
+                 and then Assertion_Expression_Pragma
+                            (Get_Pragma_Id (Original_Node (Stmt)))
+               then
+                  return True;
+
+               --  The expansion of pragma Contract_Cases produces various if
+               --  statements to evaluate all case guards. This is a suitable
+               --  context as Contract_Cases is an assertion expression.
+
+               elsif In_Assertion_Expr > 0 then
+                  return True;
+               end if;
             end if;
 
             return False;
@@ -517,12 +535,10 @@ package body Ghost is
          Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
 
       --  Otherwise the Ghost entity appears in a non-Ghost context and affects
-      --  its behavior or value.
+      --  its behavior or value (SPARK RM 6.9(11,12)).
 
       else
-         Error_Msg_N
-           ("ghost entity cannot appear in this context (SPARK RM 6.9(11))",
-            Ghost_Ref);
+         Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
       end if;
    end Check_Ghost_Context;
 
@@ -701,8 +717,8 @@ package body Ghost is
             Expr := Get_Pragma_Arg (Expr);
          end if;
 
-         --  Determine whether the expression of the aspect is static and
-         --  denotes True.
+         --  Determine whether the expression of the aspect or pragma is static
+         --  and denotes True.
 
          if Present (Expr) then
             Preanalyze_And_Resolve (Expr);