atree.adb (Allocate_Initialize_Node): A newly created node is no longer marked as Ghost at this level.

2017-01-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.adb (Allocate_Initialize_Node): A newly created node is
	no longer marked as Ghost at this level.
	(Mark_New_Ghost_Node): New routine.
	(New_Copy): Mark the copy as Ghost.
	(New_Entity): Mark the entity as Ghost.
	(New_Node): Mark the node as Ghost.
	* einfo.adb (Is_Checked_Ghost_Entity): This attribute can now
	apply to unanalyzed entities.
	(Is_Ignored_Ghost_Entity): This attribute can now apply to unanalyzed
	entities.
	(Set_Is_Checked_Ghost_Entity): This attribute now
	applies to all entities as well as unanalyzed entities.
	(Set_Is_Ignored_Ghost_Entity): This attribute now applies to
	all entities as well as unanalyzed entities.
	* expander.adb Add with and use clauses for Ghost.
	(Expand): Install and revert the Ghost region associated with the node
	being expanded.
	* exp_ch3.adb (Expand_Freeze_Array_Type): Remove all Ghost-related code.
	(Expand_Freeze_Class_Wide_Type): Remoe all Ghost-related code.
	(Expand_Freeze_Enumeration_Type): Remove all Ghost-related code.
	(Expand_Freeze_Record_Type): Remove all Ghost-related code.
	(Freeze_Type): Install and revert the Ghost region associated
	with the type being frozen.
	* exp_ch5.adb Remove with and use clauses for Ghost.
	(Expand_N_Assignment_Statement): Remove all Ghost-related code.
	* exp_ch6.adb Remove with and use clauses for Ghost.
	(Expand_N_Procedure_Call_Statement): Remove all Ghost-relatd code.
	(Expand_N_Subprogram_Body): Remove all Ghost-related code.
	* exp_ch7.adb (Build_Invariant_Procedure_Body): Install and revert the
	Ghost region of the working type.
	(Build_Invariant_Procedure_Declaration): Install and revert
	the Ghost region of the working type.
	(Expand_N_Package_Body): Remove all Ghost-related code.
	* exp_ch8.adb Remove with and use clauses for Ghost.
	(Expand_N_Exception_Renaming_Declaration): Remove all Ghost-related
	code.
	(Expand_N_Object_Renaming_Declaration): Remove all Ghost-related code.
	(Expand_N_Package_Renaming_Declaration): Remove all Ghost-related code.
	(Expand_N_Subprogram_Renaming_Declaration): Remove all Ghost-related
	code.
	* exp_ch13.adb Remove with and use clauses for Ghost.
	(Expand_N_Freeze_Entity): Remove all Ghost-related code.
	* exp_disp.adb (Make_DT): Install and revert the Ghost region of
	the tagged type. Move the generation of various entities within
	the Ghost region of the type.
	* exp_prag.adb Remove with and use clauses for Ghost.
	(Expand_Pragma_Check): Remove all Ghost-related code.
	(Expand_Pragma_Contract_Cases): Remove all Ghost-related code.
	(Expand_Pragma_Initial_Condition): Remove all Ghost-related code.
	(Expand_Pragma_Loop_Variant): Remove all Ghost-related code.
	* exp_util.adb (Build_DIC_Procedure_Body): Install
	and revert the Ghost region of the working types.
	(Build_DIC_Procedure_Declaration): Install and revert the
	Ghost region of the working type.
	(Make_Invariant_Call): Install and revert the Ghost region of the
	associated type.
	(Make_Predicate_Call): Reimplemented. Install and revert the
	Ghost region of the associated type.
	* freeze.adb (Freeze_Entity): Install and revert the Ghost region
	of the entity being frozen.
	(New_Freeze_Node): Removed.
	* ghost.adb Remove with and use clauses for Opt.
	(Check_Ghost_Completion): Update the parameter profile
	and all references to formal parameters.
	(Ghost_Entity): Update the comment on usage.
	(Install_Ghost_Mode): New routines.
	(Is_Ghost_Assignment): New routine.
	(Is_Ghost_Declaration): New routine.
	(Is_Ghost_Pragma): New routine.
	(Is_Ghost_Procedure_Call): New routine.
	(Is_Ghost_Renaming): Removed.
	(Is_OK_Declaration): Reimplemented.
	(Is_OK_Pragma): Reimplemented.
	(Is_OK_Statement): Reimplemented.
	(Is_Subject_To_Ghost): Update the comment on usage.
	(Mark_And_Set_Ghost_Assignment): New routine.
	(Mark_And_Set_Ghost_Body): New routine.
	(Mark_And_Set_Ghost_Completion): New routine.
	(Mark_And_Set_Ghost_Declaration): New routine.
	(Mark_And_Set_Ghost_Instantiation): New routine.
	(Mark_And_Set_Ghost_Procedure_Call): New routine.
	(Mark_Full_View_As_Ghost): Removed.
	(Mark_Ghost_Declaration_Or_Body): New routine.
	(Mark_Ghost_Pragma): New routine.
	(Mark_Ghost_Renaming): New routine.
	(Mark_Pragma_As_Ghost): Removed.
	(Mark_Renaming_As_Ghost): Removed.
	(Propagate_Ignored_Ghost_Code): Update the comment on usage.
	(Prune_Node): Freeze nodes no longer need special pruning, they
	are processed by the general ignored Ghost code mechanism.
	(Restore_Ghost_Mode): New routine.
	(Set_Ghost_Mode): Reimplemented.
	(Set_Ghost_Mode_From_Entity): Removed.
	* ghost.ads Add with and use clauses for Ghost.
	(Check_Ghost_Completion): Update the parameter profile
	along with the comment on usage.
	(Install_Ghost_Mode): New routine.
	(Is_Ghost_Assignment): New routine.
	(Is_Ghost_Declaration): New routine.
	(Is_Ghost_Pragma): New routine.
	(Is_Ghost_Procedure_Call): New routine.
	(Mark_And_Set_Ghost_Assignment): New routine.
	(Mark_And_Set_Ghost_Body): New routine.
	(Mark_And_Set_Ghost_Completion): New routine.
	(Mark_And_Set_Ghost_Declaration): New routine.
	(Mark_And_Set_Ghost_Instantiation): New routine.
	(Mark_And_Set_Ghost_Procedure_Call): New routine.
	(Mark_Full_View_As_Ghost): Removed.
	(Mark_Ghost_Pragma): New routine.
	(Mark_Ghost_Renaming): New routine.
	(Mark_Pragma_As_Ghost): Removed.
	(Mark_Renaming_As_Ghost): Removed.
	(Restore_Ghost_Mode): New routine.
	(Set_Ghost_Mode): Redefined.
	(Set_Ghost_Mode_From_Entity): Removed.
	* sem.adb (Analyze): Install and revert the Ghost region of the
	node being analyzed.
	(Do_Analyze): Change the way a clean Ghost
	region is installed and reverted.
	* sem_ch3.adb (Analyze_Full_Type_Declaration): Remove
	all Ghost-related code.
	(Analyze_Incomplete_Type_Decl): Remove all Ghost-related code.
	(Analyze_Number_Declaration): Remove all Ghost-related code.
	(Analyze_Object_Declaration): Install and revert the Ghost region of
	a deferred object declaration's completion.
	(Array_Type_Declaration): Remove all Ghost-related code.
	(Build_Derived_Type): Update the comment on
	the propagation of Ghost attributes from a parent to a derived type.
	(Derive_Subprogram): Remove all Ghost-related code.
	(Make_Class_Wide_Type): Remove all Ghost-related code.
	(Make_Implicit_Base): Remove all Ghost-related code.
	(Process_Full_View): Install and revert the Ghost region of
	the partial view.  There is no longer need to check the Ghost
	completion here.
	* sem_ch5.adb (Analyze_Assignment): Install and revert the Ghost
	region of the left hand side.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Remove
	all Ghost-related code.
	(Analyze_Expression_Function): Remove all Ghost-related code.
	(Analyze_Generic_Subprogram_Body): Remove all Ghost-related code.
	(Analyze_Procedure_Call): Install and revert the Ghost region of
	the procedure being called.
	(Analyze_Subprogram_Body_Helper): Install and revert the Ghost
	region of the spec or body.
	(Analyze_Subprogram_Declaration): Remove all Ghost-related code.
	(Build_Subprogram_Declaration): Remove all Ghost-related code.
	(Find_Corresponding_Spec): Remove all Ghost-related code.
	(Process_Formals): Remove all Ghost-related code.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Install and revert
	the Ghost region of the spec.
	(Analyze_Package_Declaration): Remove all Ghost-related code.
	* sem_ch8.adb (Analyze_Exception_Renaming): Mark a renaming as
	Ghost when it aliases a Ghost entity.
	(Analyze_Generic_Renaming): Mark a renaming as Ghost when it aliases
	a Ghost entity.
	(Analyze_Object_Renaming): Mark a renaming as Ghost when
	it aliases a Ghost entity.
	(Analyze_Package_Renaming): Mark a renaming as Ghost when it aliases
	a Ghost entity.
	(Analyze_Subprogram_Renaming): Mark a renaming as Ghost when it
	aliases a Ghost entity.
	* sem_ch11.adb Remove with and use clauses for Ghost.
	(Analyze_Exception_Declaration): Remove all Ghost-related code.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Remove all
	Ghost-related code.
	(Analyze_Generic_Subprogram_Declaration): Remove all Ghost-related
	code.
	(Analyze_Package_Instantiation): Install and revert the Ghost region
	of the package instantiation.
	(Analyze_Subprogram_Instantiation): Install
	and revert the Ghost region of the subprogram instantiation.
	(Instantiate_Package_Body): Code clean up. Install and revert the
	Ghost region of the package body.
	(Instantiate_Subprogram_Body): Code clean up. Install and revert the
	Ghost region of the subprogram body.
	* sem_ch13.adb (Build_Predicate_Functions): Install
	and revert the Ghost region of the related type.
	(Build_Predicate_Function_Declaration): Code clean up. Install
	and rever the Ghost region of the related type.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Install and revert the Ghost region of the pragma.
	(Analyze_Initial_Condition_In_Decl_Part): Install and revert the
	Ghost region of the pragma.
	(Analyze_Pragma): Install and revert the Ghost region of various
	pragmas.  Mark a pragma as Ghost when it is related to a Ghost entity
	or encloses a Ghost entity.
	(Analyze_Pre_Post_Condition): Install and revert the Ghost
	region of the pragma.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Install and revert the
	Ghost region of the pragma.
	* sem_res.adb (Resolve): Remove all Ghost-related code.
	* sem_util.adb (Is_Declaration): Reimplemented.
	(Is_Declaration_Other_Than_Renaming): New routine.
	* sem_util.ads (Is_Declaration_Other_Than_Renaming): New routine.
	* sinfo.adb (Is_Checked_Ghost_Pragma): New routine.
	(Is_Ghost_Pragma): Removed.
	(Is_Ignored_Ghost_Pragma): New routine.
	(Set_Is_Checked_Ghost_Pragma): New routine.
	(Set_Is_Ghost_Pragma): Removed.
	(Set_Is_Ignored_Ghost_Pragma): New routine.
	* sinfo.ads: Update the documentation on Ghost mode and
	Ghost regions.	New attributes Is_Checked_Ghost_Pragma
	and Is_Ignored_Ghost_Pragma along with usages in nodes.
	Remove attribute Is_Ghost_Pragma along with usages in nodes.
	(Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
	(Is_Ghost_Pragma): Removed along with pragma Inline.
	(Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Ghost_Pragma): Removed along with pragma Inline.
	(Set_Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.

From-SVN: r244395

1 files changed, 139 insertions, 57 deletions

diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 7a0aec3..d5f11df 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2014-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2014-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -26,6 +26,7 @@
 --  This package contains routines that deal with the static and runtime
 --  semantics of Ghost entities.
 
+with Opt;   use Opt;
 with Types; use Types;
 
 package Ghost is
@@ -35,13 +36,15 @@ package Ghost is
    --  post processing.
 
    procedure Check_Ghost_Completion
-     (Partial_View : Entity_Id;
-      Full_View    : Entity_Id);
-   --  Verify that the Ghost policy of a full view or a completion is the same
-   --  as the Ghost policy of the partial view. Emit an error if this is not
-   --  the case.
-
-   procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
+     (Prev_Id  : Entity_Id;
+      Compl_Id : Entity_Id);
+   --  Verify that the Ghost policy of initial entity Prev_Id is compatible
+   --  with the Ghost policy of completing entity Compl_Id. Emit an error if
+   --  this is not the case.
+
+   procedure Check_Ghost_Context
+     (Ghost_Id  : Entity_Id;
+      Ghost_Ref : Node_Id);
    --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
    --  where Ghost entity Ghost_Id can safely reside.
 
@@ -71,70 +74,149 @@ package Ghost is
    procedure Initialize;
    --  Initialize internal tables
 
-   procedure Lock;
-   --  Lock internal tables before calling backend
+   procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
+   --  Set the value of global variable Ghost_Mode depending on the Ghost
+   --  policy denoted by Mode.
 
-   procedure Mark_Full_View_As_Ghost
-     (Priv_Typ : Entity_Id;
-      Full_Typ : Entity_Id);
-   --  Set all Ghost-related attributes of type Full_Typ depending on the Ghost
-   --  mode of incomplete or private type Priv_Typ.
+   function Is_Ghost_Assignment (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary node N denotes an assignment statement whose
+   --  target is a Ghost entity.
 
-   procedure Mark_Pragma_As_Ghost
-     (Prag       : Node_Id;
-      Context_Id : Entity_Id);
-   --  Set all Ghost-related attributes of pragma Prag if its context denoted
-   --  by Id is a Ghost entity.
+   function Is_Ghost_Declaration (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary node N denotes a declaration which defines
+   --  a Ghost entity.
 
-   procedure Mark_Renaming_As_Ghost
-     (Ren_Decl : Node_Id;
-      Nam_Id   : Entity_Id);
-   --  Set all Ghost-related attributes of renaming declaration Ren_Decl if its
-   --  renamed name denoted by Nam_Id is a Ghost entity.
+   function Is_Ghost_Pragma (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary node N denotes a pragma which encloses a
+   --  Ghost entity or is associated with a Ghost entity.
 
-   procedure Remove_Ignored_Ghost_Code;
-   --  Remove all code marked as ignored Ghost from the trees of all qualifying
-   --  units (SPARK RM 6.9(4)).
-   --
-   --  WARNING: this is a separate front end pass, care should be taken to keep
-   --  it optimized.
+   function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary node N denotes a procedure call invoking a
+   --  Ghost procedure.
 
-   procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
-   --  Set the value of global variable Ghost_Mode depending on the following
-   --  scenarios:
+   procedure Lock;
+   --  Lock internal tables before calling backend
+
+   procedure Mark_And_Set_Ghost_Assignment
+     (N    : Node_Id;
+      Mode : out Ghost_Mode_Type);
+   --  Mark assignment statement N as Ghost when:
+   --
+   --    * The left hand side denotes a Ghost entity
+   --
+   --  Install the Ghost mode of the assignment statement. Mode is the Ghost
+   --  mode in effect prior to processing the assignment. This routine starts
+   --  a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_And_Set_Ghost_Body
+     (N       : Node_Id;
+      Spec_Id : Entity_Id;
+      Mode    : out Ghost_Mode_Type);
+   --  Mark package or subprogram body N as Ghost when:
+   --
+   --    * The body is subject to pragma Ghost
+   --
+   --    * The body completes a previous declaration whose spec denoted by
+   --      Spec_Id is a Ghost entity.
+   --
+   --    * The body appears within a Ghost region
    --
-   --    If N is a declaration, determine whether N is subject to pragma Ghost.
-   --    If this is the case, the Ghost_Mode is set based on the current Ghost
-   --    policy in effect. Special cases:
+   --  Install the Ghost mode of the body. Mode is the Ghost mode prior to
+   --  processing the body. This routine starts a Ghost region and must be
+   --  used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_And_Set_Ghost_Completion
+     (N       : Node_Id;
+      Prev_Id : Entity_Id;
+      Mode    : out Ghost_Mode_Type);
+   --  Mark completion N of a deferred constant or private type [extension]
+   --  Ghost when:
    --
-   --      N is the completion of a deferred constant, the Ghost_Mode is set
-   --      based on the mode of partial declaration entity denoted by Id.
+   --    * The entity of the previous declaration denoted by Prev_Id is Ghost
    --
-   --      N is the full view of a private type, the Ghost_Mode is set based
-   --      on the mode of the partial declaration entity denoted by Id.
+   --    * The completion appears within a Ghost region
    --
-   --    If N is an assignment statement or a procedure call, the Ghost_Mode is
-   --    set based on the mode of the name.
+   --  Install the Ghost mode of the completion. Mode is the Ghost mode prior
+   --  to processing the completion. This routine starts a Ghost region and
+   --  must be used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_And_Set_Ghost_Declaration
+     (N    : Node_Id;
+      Mode : out Ghost_Mode_Type);
+   --  Mark declaration N as Ghost when:
    --
-   --    If N denotes a package or a subprogram body, the Ghost_Mode is set to
-   --    the current Ghost policy in effect if the body is subject to Ghost or
-   --    the corresponding spec denoted by Id is a Ghost entity.
+   --    * The declaration is subject to pragma Ghost
    --
-   --    If N is a pragma, the Ghost_Mode is set based on the mode of the
-   --    pragma.
+   --    * The declaration denotes a child package or subprogram and the parent
+   --      is a Ghost unit.
    --
-   --    If N is a freeze node, the Global_Mode is set based on the mode of
-   --    entity Id.
+   --    * The declaration appears within a Ghost region
    --
-   --  WARNING: the caller must save and restore the value of Ghost_Mode in a
-   --  a stack-like fasion as this routine may override the existing value.
+   --  Install the Ghost mode of the declaration. Mode is the Ghost mode prior
+   --  to processing the declaration. This routine starts a Ghost region and
+   --  must be used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_And_Set_Ghost_Instantiation
+     (N      : Node_Id;
+      Gen_Id : Entity_Id;
+      Mode   : out Ghost_Mode_Type);
+   --  Mark instantiation N as Ghost when:
+   --
+   --    * The instantiation is subject to pragma Ghost
+   --
+   --    * The generic template denoted by Gen_Id is Ghost
+   --
+   --    * The instantiation appears within a Ghost region
+   --
+   --  Install the Ghost mode of the instantiation. Mode is the Ghost mode
+   --  prior to processing the instantiation. This routine starts a Ghost
+   --  region and must be used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_And_Set_Ghost_Procedure_Call
+     (N    : Node_Id;
+      Mode : out Ghost_Mode_Type);
+   --  Mark procedure call N as Ghost when:
+   --
+   --    * The procedure being invoked is a Ghost entity
+   --
+   --  Install the Ghost mode of the procedure call. Mode is the Ghost mode
+   --  prior to processing the procedure call. This routine starts a Ghost
+   --  region and must be used in conjunction with Restore_Ghost_Mode.
+
+   procedure Mark_Ghost_Pragma
+     (N  : Node_Id;
+      Id : Entity_Id);
+   --  Mark pragma N as Ghost when:
+   --
+   --    * The pragma encloses Ghost entity Id
+   --
+   --    * The pragma is associated with Ghost entity Id
 
-   procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-   --  Set the valye of global variable Ghost_Mode depending on the mode of
-   --  entity Id.
+   procedure Mark_Ghost_Renaming
+     (N  : Node_Id;
+      Id : Entity_Id);
+   --  Mark renaming declaration N as Ghost when:
    --
-   --  WARNING: the caller must save and restore the value of Ghost_Mode in a
-   --  a stack-like fasion as this routine may override the existing value.
+   --    * Renamed entity Id denotes a Ghost entity
+
+   procedure Remove_Ignored_Ghost_Code;
+   --  Remove all code marked as ignored Ghost from the trees of all qualifying
+   --  units (SPARK RM 6.9(4)).
+   --
+   --  WARNING: this is a separate front end pass, care should be taken to keep
+   --  it optimized.
+
+   procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
+   --  Terminate a Ghost region by restoring the Ghost mode prior to the
+   --  region denoted by Mode. This routine must be used in conjunction
+   --  with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
+
+   procedure Set_Ghost_Mode
+     (N    : Node_Or_Entity_Id;
+      Mode : out Ghost_Mode_Type);
+   --  Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior
+   --  to processing the node. This routine starts a Ghost region and must be
+   --  used in conjunction with Restore_Ghost_Mode.
 
    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
    --  Set the relevant Ghost attributes of entity Id depending on the current