2015-05-26 Hristian Kirtchev <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
	restore the Ghost mode.
	(Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
	(Freeze_Type): Update the call to Set_Ghost_Mode.
	(Restore_Globals): New routine.
	* exp_ch5.adb Add with and use clauses for Ghost.
	(Expand_N_Assignment_Statement): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch6.adb Add with and use clauses for Ghost.
	(Expand_N_Procedure_Call_Statement): Capture, set and
	restore the Ghost mode.
	(Expand_N_Subprogram_Body):
	Code cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Subprogram_Declaration): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch7.adb Add with and use clauses for Ghost.
	(Expand_N_Package_Body): Capture, set and restore the Ghost mode.
	(Expand_N_Package_Declaration): Capture, set and restore the
	Ghost mode.
	(Wrap_HSS_In_Block): Create a proper identifier for the block.
	* exp_ch8.adb Add with and use clauses for Ghost.
	(Expand_N_Exception_Renaming_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Object_Renaming_Declaration): Capture, set and restore
	the Ghost mode.
	(Expand_N_Package_Renaming_Declaration): Capture, set and restore the
	Ghost mode.
	(Expand_N_Subprogram_Renaming_Declaration): Capture, set and
	restore the Ghost mode.
	* exp_ch11.adb (Expand_N_Exception_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	* exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
	not initialize the dispatch table slot of a Ghost subprogram.
	* exp_prag.adb Add with and use clauses for Ghost.
	(Expand_Pragma_Check): Capture, set and restore the Ghost mode.
	(Expand_Pragma_Contract_Cases): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Initial_Condition): Capture, set and
	restore the Ghost mode.
	(Expand_Pragma_Loop_Variant): Capture,
	set and restore the Ghost mode.
	(Restore_Globals): New routine.
	* exp_util.adb Add with and use clauses for Ghost.
	(Make_Predicate_Call): Code cleanup. Capture, set and restore
	the Ghost mode.
	(Restore_Globals): New routine.
	* freeze.adb (Freeze_Entity): Code cleanup. Update the call
	to Set_Ghost_Mode.
	* ghost.adb Add with and use clause for Sem_Prag.
	(Check_Ghost_Completion): Code cleanup.
	(Check_Ghost_Overriding): New routine.
	(Check_Ghost_Policy): Code cleanup.
	(Ghost_Entity): New routine.
	(Is_Ghost_Declaration): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_OK_Context): Reimplemented.
	(Is_OK_Declaration): New routine.
	(Is_OK_Pragma): New routine.
	(Is_OK_Statement): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Propagate_Ignored_Ghost_Code): Update the comment on usage.
	(Set_From_Entity): New routine.
	(Set_From_Policy): New routine.
	(Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	(Set_Ghost_Mode_From_Policy): Removed.
	* ghost.ads (Check_Ghost_Overriding): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Set_Ghost_Mode): Update the parameter profile. Update the
	comment on usage.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	* sem_ch3.adb (Analyze_Full_Type_Declaration):
	Capture and restore the Ghost mode. Mark a type
	as Ghost regardless of whether it comes from source.
	(Analyze_Incomplete_Type_Decl): Capture, set and restore the
	Ghost mode.
	(Analyze_Number_Declaration): Capture and restore the Ghost mode.
	(Analyze_Object_Declaration): Capture and restore the Ghost mode.
	(Analyze_Private_Extension_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
	(Process_Full_View): The full view inherits all Ghost-related
	attributes from the private view.
	(Restore_Globals): New routine.
	* sem_ch5.adb (Analyze_Assignment): Capture and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
	Code cleanup. Capture and restore the Ghost mode. Mark a
	subprogram as Ghost regarless of whether it comes from source.
	(Analyze_Procedure_Call): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
	(New_Overloaded_Entity): Ensure that a
	parent subprogram and an overriding subprogram have compatible
	Ghost policies.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
	the Ghost mode.
	(Analyze_Package_Declaration): Capture and
	restore the Ghost mode. Mark a package as Ghost when it is
	declared in a Ghost region.
	(Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch8.adb (Analyze_Exception_Renaming): Code
	reformatting. Capture and restore the Ghost mode. A renaming
	becomes Ghost when its name references a Ghost entity.
	(Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Object_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Package_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Subprogram_Renaming): Capture and restore the Ghost
	mode. A renaming becomes Ghost when its name references a
	Ghost entity.
	* sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
	and restore the Ghost mode.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Generic_Subprogram_Declaration):
	Capture and restore the Ghost mode.
	* sem_ch13.adb Add with and use clauses for Ghost.
	(Add_Invariant): New routine.
	(Add_Invariants): Factor out code.
	(Add_Predicate): New routine.
	(Add_Predicates): Factor out code.
	(Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
	set and restore the Ghost mode.
	(Build_Invariant_Procedure): Code cleanup.
	(Build_Predicate_Functions): Capture, set and
	restore the Ghost mode. Mark the generated functions as Ghost.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_External_Property_In_Decl_Part): Capture, set and restore
	the Ghost mode.
	(Analyze_Initial_Condition_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_Pragma):
	Code cleanup. Capture, set and restore the Ghost mode. Flag
	pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
	Unreferenced_Objects as illegal when it applies to both Ghost
	and living arguments. Pragma Ghost cannot apply to synchronized
	objects.
	(Check_Kind): Moved to the spec of Sem_Prag.
	(Process_Inline): Flag the pragma as illegal when it applies to
	both Ghost and living arguments.
	(Restore_Globals): New routine.
	* sem_prag.ads Add pragma Default_Initial_Condition
	to table Assertion_Expression_Pragma. Add new table
	Is_Aspect_Specifying_Pragma.
	(Check_Kind): Moved from body of Sem_Prag.
	* sem_util.adb Add with and use clauses for Ghost.
	(Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
	the Ghost mode.
	(Build_Default_Init_Cond_Procedure_Declaration):
	Capture, set and restore the Ghost mode. Mark the default
	initial condition procedure as Ghost when it is declared
	in a Ghost region.
	(Is_Renaming_Declaration): New routine.
	(Policy_In_List): Account for the single argument version of
	Check_Pragma.
	* sem_util.ads (Is_Renaming_Declaration): New routine.
	* sinfo.adb (Is_Ghost_Pragma): New routine.
	(Set_Is_Ghost_Pragma): New routine.
	* sinfo.ads New attribute Is_Ghost_Pragma.
	(Is_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Ghost_Pragma): New routine along with pragma Inline.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@223684 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 74 insertions, 6 deletions

diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 4bbfbd4ce16..fab3facddc3 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -32,6 +32,7 @@ with Errout;   use Errout;
 with Exp_Ch11; use Exp_Ch11;
 with Exp_Util; use Exp_Util;
 with Expander; use Expander;
+with Ghost;    use Ghost;
 with Inline;   use Inline;
 with Namet;    use Namet;
 with Nlists;   use Nlists;
@@ -292,6 +293,7 @@ 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));
       Msg  : Node_Id;
@@ -317,6 +319,16 @@ 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.
 
@@ -480,6 +492,11 @@ 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;
 
    ---------------------------------
@@ -963,9 +980,10 @@ package body Exp_Prag is
 
       --  Local variables
 
-      Aggr          : constant Node_Id :=
-                        Expression (First
-                          (Pragma_Argument_Associations (CCs)));
+      Aggr : constant Node_Id :=
+               Expression (First (Pragma_Argument_Associations (CCs)));
+      GM   : constant Ghost_Mode_Type := Ghost_Mode;
+
       Case_Guard    : Node_Id;
       CG_Checks     : Node_Id;
       CG_Stmts      : List_Id;
@@ -999,6 +1017,12 @@ 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.
+
+      Set_Ghost_Mode (CCs);
+
       Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
 
       --  Create the counter which tracks the number of case guards that
@@ -1223,6 +1247,11 @@ package body Exp_Prag is
       end if;
 
       Append_To (Stmts, Conseq_Checks);
+
+      --  Restore the original Ghost mode once analysis and expansion have
+      --  taken place.
+
+      Ghost_Mode := GM;
    end Expand_Pragma_Contract_Cases;
 
    ---------------------------------------
@@ -1322,6 +1351,22 @@ 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;
@@ -1329,6 +1374,8 @@ package body Exp_Prag is
       List      : List_Id;
       Pack_Id   : Entity_Id;
 
+   --  Start of processing for Expand_Pragma_Initial_Condition
+
    begin
       if Nkind (Spec_Or_Body) = N_Package_Body then
          Pack_Id := Corresponding_Spec (Spec_Or_Body);
@@ -1367,6 +1414,12 @@ 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.
+
+      Set_Ghost_Mode (Init_Cond);
+
       --  The caller should check whether the package is subject to pragma
       --  Initial_Condition.
 
@@ -1379,6 +1432,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;
          return;
       end if;
 
@@ -1396,6 +1450,8 @@ package body Exp_Prag is
 
       Append_To (List, Check);
       Analyze (Check);
+
+      Restore_Globals;
    end Expand_Pragma_Initial_Condition;
 
    ------------------------------------
@@ -1524,9 +1580,8 @@ package body Exp_Prag is
    --     end loop;
 
    procedure Expand_Pragma_Loop_Variant (N : Node_Id) is
-      Loc : constant Source_Ptr := Sloc (N);
-
       Last_Var : constant Node_Id := Last (Pragma_Argument_Associations (N));
+      Loc      : constant Source_Ptr := Sloc (N);
 
       Curr_Assign : List_Id   := No_List;
       Flag_Id     : Entity_Id := Empty;
@@ -1743,6 +1798,10 @@ package body Exp_Prag is
          end if;
       end Process_Variant;
 
+      --  Local variables
+
+      GM : constant Ghost_Mode_Type := Ghost_Mode;
+
    --  Start of processing for Expand_Pragma_Loop_Variant
 
    begin
@@ -1755,6 +1814,12 @@ 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.
+
+      Set_Ghost_Mode (N);
+
       --  Locate the enclosing loop for which this assertion applies. In the
       --  case of Ada 2012 array iteration, we might be dealing with nested
       --  loops. Only the outermost loop has an identifier.
@@ -1777,7 +1842,6 @@ package body Exp_Prag is
       Variant := First (Pragma_Argument_Associations (N));
       while Present (Variant) loop
          Process_Variant (Variant, Is_Last => Variant = Last_Var);
-
          Next (Variant);
       end loop;
 
@@ -1817,6 +1881,10 @@ 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;
    end Expand_Pragma_Loop_Variant;
 
    --------------------------------