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, 95 insertions, 26 deletions

diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 6c5472a1..dd1aec5 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -528,26 +528,81 @@ package Sinfo is
    -- Ghost Mode --
    ----------------
 
-   --  When a declaration is subject to pragma Ghost, it establishes a Ghost
-   --  region depending on the Ghost assertion policy in effect at the point
-   --  of declaration. This region is temporal and starts right before the
-   --  analysis of the Ghost declaration and ends after its expansion. The
-   --  values of global variable Opt.Ghost_Mode are as follows:
+   --  The SPARK RM 6.9 defines two classes of constructs - Ghost entities and
+   --  Ghost statements. The intent of the feature is to treat Ghost constructs
+   --  as non-existent when Ghost assertion policy Ignore is in effect.
+
+   --  The corresponding nodes which map to Ghost constructs are:
+
+   --    Ghost entities
+   --      Declaration nodes
+   --      N_Package_Body
+   --      N_Subprogram_Body
+
+   --    Ghost statements
+   --      N_Assignment_Statement
+   --      N_Procedure_Call_Statement
+   --      N_Pragma
+
+   --  In addition, the compiler treats instantiations as Ghost entities
+
+   --  To achieve the removal of ignored Ghost constructs, the compiler relies
+   --  on global variable Ghost_Mode and a mechanism called "Ghost regions".
+   --  The values of the global variable are as follows:
 
    --    1. Check - All static semantics as defined in SPARK RM 6.9 are in
-   --       effect.
+   --       effect. The Ghost region has mode Check.
 
    --    2. Ignore - Same as Check, ignored Ghost code is not present in ALI
-   --       files, object files as well as the final executable.
+   --       files, object files, and the final executable. The Ghost region
+   --       has mode Ignore.
+
+   --    3. None - No Ghost region is in effect
+
+   --  A Ghost region is a compiler operating mode, similar to Check_Syntax,
+   --  however a region is much more finely grained and depends on the policy
+   --  in effect. The region starts prior to the analysis of a Ghost construct
+   --  and ends immediately after its expansion. The region is established as
+   --  follows:
+
+   --    1. Declarations - Prior to analysis, if the declaration is subject to
+   --       pragma Ghost.
+
+   --    2. Renaming declarations - Same as 1) or when the renamed entity is
+   --       Ghost.
 
-   --  To achieve the runtime semantics of "Ignore", the compiler marks each
-   --  node created during an ignored Ghost region and signals all enclosing
-   --  scopes that such a node resides within. The compilation unit where the
-   --  node resides is also added to an auxiliary table for post processing.
+   --    3. Completing declarations - Same as 1) or when the declaration is
+   --       partially analyzed and the declaration completes a Ghost entity.
+
+   --    4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is
+   --       partially analyzed and completes a Ghost entity.
+
+   --    5. N_Assignment_Statement - After the left hand side is analyzed and
+   --       references a Ghost entity.
+
+   --    6. N_Procedure_Call_Statement - After the name is analyzed and denotes
+   --       a Ghost procedure.
+
+   --    7. N_Pragma - During analysis, when the related entity is Ghost or the
+   --       pragma encloses a Ghost entity.
+
+   --    8. Instantiations - Save as 1) or when the instantiation is partially
+   --       analyzed and the generic template is Ghost.
+
+   --  Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine
+   --  Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled
+   --  similar to scopes for decoupled expansion such as the generation of
+   --  dispatch tables or the creation of a predicate function.
+
+   --  If the mode of a Ghost region is Ignore, any newly created nodes as well
+   --  as source entities are marked as ignored Ghost. In additon, the marking
+   --  process signals all enclosing scopes that an ignored Ghost node resides
+   --  within. The compilation unit where the node resides is also added to an
+   --  auxiliary table for post processing.
 
    --  After the analysis and expansion of all compilation units takes place
    --  as well as the instantiation of all inlined [generic] bodies, the GNAT
-   --  driver initiates a separate pass which removes all ignored Ghost code
+   --  driver initiates a separate pass which removes all ignored Ghost nodes
    --  from all units stored in the auxiliary table.
 
    --------------------
@@ -1581,6 +1636,11 @@ package Sinfo is
    --    be further modified (in some cases these flags are copied when a
    --    pragma is rewritten).
 
+   --  Is_Checked_Ghost_Pragma (Flag3-Sem)
+   --    This flag is present in N_Pragma nodes. It is set when the pragma is
+   --    related to a checked Ghost entity or encloses a checked Ghost entity.
+   --    This flag has no relation to Is_Checked.
+
    --  Is_Component_Left_Opnd  (Flag13-Sem)
    --  Is_Component_Right_Opnd (Flag14-Sem)
    --    Present in concatenation nodes, to indicate that the corresponding
@@ -1651,11 +1711,6 @@ package Sinfo is
    --      Refined_State
    --      Test_Case
 
-   --  Is_Ghost_Pragma (Flag3-Sem)
-   --    This flag is present in N_Pragma nodes. It is set when the pragma is
-   --    either declared within a Ghost construct or it applies to a Ghost
-   --    construct.
-
    --  Is_Ignored (Flag9-Sem)
    --    A flag set in an N_Aspect_Specification or N_Pragma node if there was
    --    a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
@@ -1670,6 +1725,11 @@ package Sinfo is
    --    aspect/pragma is fully analyzed and checked for other syntactic
    --    and semantic errors, but it does not have any semantic effect.
 
+   --  Is_Ignored_Ghost_Pragma (Flag8-Sem)
+   --    This flag is present in N_Pragma nodes. It is set when the pragma is
+   --    related to an ignored Ghost entity or encloses ignored Ghost entity.
+   --    This flag has no relation to Is_Ignored.
+
    --  Is_In_Discriminant_Check (Flag11-Sem)
    --    This flag is present in a selected component, and is used to indicate
    --    that the reference occurs within a discriminant check. The
@@ -2519,11 +2579,12 @@ package Sinfo is
       --  Import_Interface_Present (Flag16-Sem)
       --  Is_Analyzed_Pragma (Flag5-Sem)
       --  Is_Checked (Flag11-Sem)
+      --  Is_Checked_Ghost_Pragma (Flag3-Sem)
       --  Is_Delayed_Aspect (Flag14-Sem)
       --  Is_Disabled (Flag15-Sem)
       --  Is_Generic_Contract_Pragma (Flag2-Sem)
-      --  Is_Ghost_Pragma (Flag3-Sem)
       --  Is_Ignored (Flag9-Sem)
+      --  Is_Ignored_Ghost_Pragma (Flag8-Sem)
       --  Is_Inherited_Pragma (Flag4-Sem)
       --  Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
       --  Uneval_Old_Accept (Flag7-Sem)
@@ -9364,6 +9425,9 @@ package Sinfo is
    function Is_Checked
      (N : Node_Id) return Boolean;    -- Flag11
 
+   function Is_Checked_Ghost_Pragma
+     (N : Node_Id) return Boolean;    -- Flag3
+
    function Is_Component_Left_Opnd
      (N : Node_Id) return Boolean;    -- Flag13
 
@@ -9403,12 +9467,12 @@ package Sinfo is
    function Is_Generic_Contract_Pragma
      (N : Node_Id) return Boolean;    -- Flag2
 
-   function Is_Ghost_Pragma
-     (N : Node_Id) return Boolean;    -- Flag3
-
    function Is_Ignored
      (N : Node_Id) return Boolean;    -- Flag9
 
+   function Is_Ignored_Ghost_Pragma
+     (N : Node_Id) return Boolean;    -- Flag8
+
    function Is_In_Discriminant_Check
      (N : Node_Id) return Boolean;    -- Flag11
 
@@ -10414,6 +10478,9 @@ package Sinfo is
    procedure Set_Is_Checked
      (N : Node_Id; Val : Boolean := True);    -- Flag11
 
+   procedure Set_Is_Checked_Ghost_Pragma
+     (N : Node_Id; Val : Boolean := True);    -- Flag3
+
    procedure Set_Is_Component_Left_Opnd
      (N : Node_Id; Val : Boolean := True);    -- Flag13
 
@@ -10453,12 +10520,12 @@ package Sinfo is
    procedure Set_Is_Generic_Contract_Pragma
      (N : Node_Id; Val : Boolean := True);    -- Flag2
 
-   procedure Set_Is_Ghost_Pragma
-     (N : Node_Id; Val : Boolean := True);    -- Flag3
-
    procedure Set_Is_Ignored
      (N : Node_Id; Val : Boolean := True);    -- Flag9
 
+   procedure Set_Is_Ignored_Ghost_Pragma
+     (N : Node_Id; Val : Boolean := True);    -- Flag8
+
    procedure Set_Is_In_Discriminant_Check
      (N : Node_Id; Val : Boolean := True);    -- Flag11
 
@@ -12865,6 +12932,7 @@ package Sinfo is
    pragma Inline (Is_Asynchronous_Call_Block);
    pragma Inline (Is_Boolean_Aspect);
    pragma Inline (Is_Checked);
+   pragma Inline (Is_Checked_Ghost_Pragma);
    pragma Inline (Is_Component_Left_Opnd);
    pragma Inline (Is_Component_Right_Opnd);
    pragma Inline (Is_Controlling_Actual);
@@ -12878,8 +12946,8 @@ package Sinfo is
    pragma Inline (Is_Finalization_Wrapper);
    pragma Inline (Is_Folded_In_Parser);
    pragma Inline (Is_Generic_Contract_Pragma);
-   pragma Inline (Is_Ghost_Pragma);
    pragma Inline (Is_Ignored);
+   pragma Inline (Is_Ignored_Ghost_Pragma);
    pragma Inline (Is_In_Discriminant_Check);
    pragma Inline (Is_Inherited_Pragma);
    pragma Inline (Is_Machine_Number);
@@ -13210,6 +13278,7 @@ package Sinfo is
    pragma Inline (Set_Is_Asynchronous_Call_Block);
    pragma Inline (Set_Is_Boolean_Aspect);
    pragma Inline (Set_Is_Checked);
+   pragma Inline (Set_Is_Checked_Ghost_Pragma);
    pragma Inline (Set_Is_Component_Left_Opnd);
    pragma Inline (Set_Is_Component_Right_Opnd);
    pragma Inline (Set_Is_Controlling_Actual);
@@ -13223,8 +13292,8 @@ package Sinfo is
    pragma Inline (Set_Is_Finalization_Wrapper);
    pragma Inline (Set_Is_Folded_In_Parser);
    pragma Inline (Set_Is_Generic_Contract_Pragma);
-   pragma Inline (Set_Is_Ghost_Pragma);
    pragma Inline (Set_Is_Ignored);
+   pragma Inline (Set_Is_Ignored_Ghost_Pragma);
    pragma Inline (Set_Is_In_Discriminant_Check);
    pragma Inline (Set_Is_Inherited_Pragma);
    pragma Inline (Set_Is_Machine_Number);