exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and restore the Ghost mode.

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.

From-SVN: r223684

1 files changed, 446 insertions, 208 deletions

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index b608a45..75ceb4b 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -37,6 +37,7 @@ with Opt;      use Opt;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
@@ -62,10 +63,15 @@ package body Ghost is
    -- Local Subprograms --
    -----------------------
 
+   function Ghost_Entity (N : Node_Id) return Entity_Id;
+   --  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.
+
    procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
-   --  Subsidiary to Set_Ghost_Mode_xxx. Signal all enclosing scopes that they
-   --  now contain ignored Ghost code. Add the compilation unit containing N to
-   --  table Ignored_Ghost_Units for post processing.
+   --  Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
+   --  Signal all enclosing scopes that they now contain ignored Ghost code.
+   --  Add the compilation unit containing N to table Ignored_Ghost_Units for
+   --  post processing.
 
    ----------------------------
    -- Add_Ignored_Ghost_Unit --
@@ -113,18 +119,20 @@ package body Ghost is
       then
          Error_Msg_Sloc := Sloc (Full_View);
 
-         Error_Msg_N ("incompatible ghost policies in effect",   Partial_View);
-         Error_Msg_N ("\& declared with ghost policy Check",     Partial_View);
-         Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
+         Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+         Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
+         Error_Msg_N
+           ("\& completed # with ghost policy `Ignore`", Partial_View);
 
       elsif Is_Ignored_Ghost_Entity (Partial_View)
         and then Policy = Name_Check
       then
          Error_Msg_Sloc := Sloc (Full_View);
 
-         Error_Msg_N ("incompatible ghost policies in effect",  Partial_View);
-         Error_Msg_N ("\& declared with ghost policy Ignore",   Partial_View);
-         Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
+         Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+         Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
+         Error_Msg_N
+           ("\& completed # with ghost policy `Check`", Partial_View);
       end if;
    end Check_Ghost_Completion;
 
@@ -147,213 +155,282 @@ package body Ghost is
       -------------------------
 
       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
-         function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
-         --  Determine whether node Decl is a Ghost declaration or appears
-         --  within a Ghost declaration.
-
-         function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
-         --  Determine whether statement or pragma N is Ghost or appears within
-         --  a Ghost statement or pragma. To qualify as such, N must either
-         --    1) Occur within a ghost subprogram or package
-         --    2) Denote a call to a ghost procedure
-         --    3) Denote an assignment statement whose target is a ghost
-         --       variable.
-         --    4) Denote a pragma that mentions a ghost entity
-
-         --------------------------
-         -- Is_Ghost_Declaration --
-         --------------------------
-
-         function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
-            Par       : Node_Id;
+         function Is_OK_Declaration (Decl : Node_Id) return Boolean;
+         --  Determine whether node Decl is a suitable context for a reference
+         --  to a Ghost entity. To qualify as such, Decl must either
+         --    1) Be subject to pragma Ghost
+         --    2) Rename a Ghost entity
+
+         function Is_OK_Pragma (Prag : Node_Id) return Boolean;
+         --  Determine whether node Prag is a suitable context for a reference
+         --  to a Ghost entity. To qualify as such, Prag must either
+         --    1) Be an assertion expression pragma
+         --    2) Denote pragma Global, Depends, Initializes, Refined_Global,
+         --       Refined_Depends or Refined_State
+         --    3) Specify an aspect of a Ghost entity
+         --    4) Contain a reference to a Ghost entity
+
+         function Is_OK_Statement (Stmt : Node_Id) return Boolean;
+         --  Determine whether node Stmt is a suitable context for a reference
+         --  to a Ghost entity. To qualify as such, Stmt must either
+         --    1) Denote a call to a Ghost procedure
+         --    2) Denote an assignment statement whose target is Ghost
+
+         -----------------------
+         -- Is_OK_Declaration --
+         -----------------------
+
+         function Is_OK_Declaration (Decl : Node_Id) return Boolean is
+            function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
+            --  Determine whether node Ren_Decl denotes a renaming declaration
+            --  with a Ghost name.
+
+            -----------------------
+            -- Is_Ghost_Renaming --
+            -----------------------
+
+            function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
+               Nam_Id : Entity_Id;
+
+            begin
+               if Is_Renaming_Declaration (Ren_Decl) then
+                  Nam_Id := Ghost_Entity (Name (Ren_Decl));
+
+                  return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
+               end if;
+
+               return False;
+            end Is_Ghost_Renaming;
+
+            --  Local variables
+
             Subp_Decl : Node_Id;
             Subp_Id   : Entity_Id;
 
+         --  Start of processing for Is_OK_Declaration
+
          begin
-            --  Climb the parent chain looking for an object declaration
+            if Is_Declaration (Decl) then
 
-            Par := Decl;
-            while Present (Par) loop
-               if Is_Declaration (Par) then
+               --  A renaming declaration is Ghost when it renames a Ghost
+               --  entity.
 
-                  --  A declaration is Ghost when it appears within a Ghost
-                  --  package or subprogram.
+               if Is_Ghost_Renaming (Decl) then
+                  return True;
 
-                  if Ghost_Mode > None then
-                     return True;
+               --  The declaration may not have been analyzed yet, determine
+               --  whether it is subject to pragma Ghost.
 
-                  --  Otherwise the declaration may not have been analyzed yet,
-                  --  determine whether it is subject to aspect/pragma Ghost.
+               elsif Is_Subject_To_Ghost (Decl) then
+                  return True;
 
-                  else
-                     return Is_Subject_To_Ghost (Par);
-                  end if;
+               --  The declaration appears within an assertion expression
 
-               --  Special cases
+               elsif In_Assertion_Expr > 0 then
+                  return True;
+               end if;
 
-               --  A reference to a Ghost entity may appear as the default
-               --  expression of a formal parameter of a subprogram body. This
-               --  context must be treated as suitable because the relation
-               --  between the spec and the body has not been established and
-               --  the body is not marked as Ghost yet. The real check was
-               --  performed on the spec.
+            --  Special cases
 
-               elsif Nkind (Par) = N_Parameter_Specification
-                 and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
-               then
-                  return True;
+            --  A reference to a Ghost entity may appear as the default
+            --  expression of a formal parameter of a subprogram body. This
+            --  context must be treated as suitable because the relation
+            --  between the spec and the body has not been established and
+            --  the body is not marked as Ghost yet. The real check was
+            --  performed on the spec.
 
-               --  References to Ghost entities may be relocated in internally
-               --  generated bodies.
+            elsif Nkind (Decl) = N_Parameter_Specification
+              and then Nkind (Parent (Parent (Decl))) = N_Subprogram_Body
+            then
+               return True;
 
-               elsif Nkind (Par) = N_Subprogram_Body
-                 and then not Comes_From_Source (Par)
-               then
-                  Subp_Id := Corresponding_Spec (Par);
+            --  References to Ghost entities may be relocated in internally
+            --  generated bodies.
 
-                  --  The original context is an expression function that has
-                  --  been split into a spec and a body. The context is OK as
-                  --  long as the the initial declaration is Ghost.
+            elsif Nkind (Decl) = N_Subprogram_Body
+              and then not Comes_From_Source (Decl)
+            then
+               Subp_Id := Corresponding_Spec (Decl);
 
-                  if Present (Subp_Id) then
-                     Subp_Decl :=
-                       Original_Node (Unit_Declaration_Node (Subp_Id));
+               --  The original context is an expression function that has
+               --  been split into a spec and a body. The context is OK as
+               --  long as the initial declaration is Ghost.
 
-                     if Nkind (Subp_Decl) = N_Expression_Function then
-                        return Is_Subject_To_Ghost (Subp_Decl);
-                     end if;
+               if Present (Subp_Id) then
+                  Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id));
+
+                  if Nkind (Subp_Decl) = N_Expression_Function then
+                     return Is_Subject_To_Ghost (Subp_Decl);
                   end if;
 
-                  --  Otherwise this is either an internal body or an internal
-                  --  completion. Both are OK because the real check was done
-                  --  before expansion activities.
+               --  Otherwise this is either an internal body or an internal
+               --  completion. Both are OK because the real check was done
+               --  before expansion activities.
 
+               else
                   return True;
                end if;
-
-               --  Prevent the search from going too far
-
-               if Is_Body_Or_Package_Declaration (Par) then
-                  return False;
-               end if;
-
-               Par := Parent (Par);
-            end loop;
+            end if;
 
             return False;
-         end Is_Ghost_Declaration;
+         end Is_OK_Declaration;
 
-         ----------------------------------
-         -- Is_Ghost_Statement_Or_Pragma --
-         ----------------------------------
+         ------------------
+         -- Is_OK_Pragma --
+         ------------------
 
-         function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
-            function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
-            --  Determine whether an arbitrary node denotes a reference to a
-            --  Ghost entity.
+         function Is_OK_Pragma (Prag : Node_Id) return Boolean is
+            procedure Check_Policies (Prag_Nam : Name_Id);
+            --  Verify that the Ghost policy in effect is the same as the
+            --  assertion policy for pragma name Prag_Nam. Emit an error if
+            --  this is not the case.
 
-            -------------------------------
-            -- Is_Ghost_Entity_Reference --
-            -------------------------------
+            --------------------
+            -- Check_Policies --
+            --------------------
 
-            function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
-               Ref : Node_Id;
+            procedure Check_Policies (Prag_Nam : Name_Id) is
+               AP : constant Name_Id := Check_Kind (Prag_Nam);
+               GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
 
             begin
-               --  When the reference extracts a subcomponent, recover the
-               --  related object (SPARK RM 6.9(1)).
-
-               Ref := N;
-               while Nkind_In (Ref, N_Explicit_Dereference,
-                                    N_Indexed_Component,
-                                    N_Selected_Component,
-                                    N_Slice)
-               loop
-                  Ref := Prefix (Ref);
-               end loop;
-
-               return
-                 Is_Entity_Name (Ref)
-                   and then Present (Entity (Ref))
-                   and then Is_Ghost_Entity (Entity (Ref));
-            end Is_Ghost_Entity_Reference;
+               --  If the Ghost policy in effect at the point of a Ghost entity
+               --  reference is Ignore, then the assertion policy of the pragma
+               --  must be Ignore (SPARK RM 6.9(18)).
+
+               if GP = Name_Ignore and then AP /= Name_Ignore then
+                  Error_Msg_N
+                    ("incompatible ghost policies in effect", Ghost_Ref);
+                  Error_Msg_NE
+                    ("\ghost entity & has policy `Ignore`",
+                     Ghost_Ref, Ghost_Id);
+
+                  Error_Msg_Name_1 := AP;
+                  Error_Msg_N
+                    ("\assertion expression has policy %", Ghost_Ref);
+               end if;
+            end Check_Policies;
 
             --  Local variables
 
-            Arg  : Node_Id;
-            Stmt : Node_Id;
+            Arg      : Node_Id;
+            Arg_Id   : Entity_Id;
+            Prag_Id  : Pragma_Id;
+            Prag_Nam : Name_Id;
 
-         --  Start of processing for Is_Ghost_Statement_Or_Pragma
+         --  Start of processing for Is_OK_Pragma
 
          begin
-            if Nkind (N) = N_Pragma then
+            if Nkind (Prag) = N_Pragma then
+               Prag_Id  := Get_Pragma_Id (Prag);
+               Prag_Nam := Original_Aspect_Pragma_Name (Prag);
 
-               --  A pragma is Ghost when it appears within a Ghost package or
-               --  subprogram.
+               --  A pragma that applies to a Ghost construct or specifies an
+               --  aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
 
-               if Ghost_Mode > None then
+               if Is_Ghost_Pragma (Prag) then
                   return True;
-               end if;
 
-               --  A pragma is Ghost when it mentions a Ghost entity
+               --  An assertion expression is a Ghost pragma when it contains a
+               --  reference to a Ghost entity (SPARK RM 6.9(11)).
 
-               Arg := First (Pragma_Argument_Associations (N));
-               while Present (Arg) loop
-                  if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
-                     return True;
-                  end if;
+               elsif Assertion_Expression_Pragma (Prag_Id) then
 
-                  Next (Arg);
-               end loop;
-            end if;
+                  --  Predicates are excluded from this category when they do
+                  --  not apply to a Ghost subtype (SPARK RM 6.9(12)).
 
-            Stmt := N;
-            while Present (Stmt) loop
-               if Is_Statement (Stmt) then
+                  if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
+                                       Name_Predicate,
+                                       Name_Static_Predicate)
+                  then
+                     return False;
 
-                  --  A statement is Ghost when it appears within a Ghost
-                  --  package or subprogram.
+                  --  Otherwise ensure that the assertion policy and the Ghost
+                  --  policy are compatible (SPARK RM 6.9(18)).
 
-                  if Ghost_Mode > None then
+                  else
+                     Check_Policies (Prag_Nam);
                      return True;
+                  end if;
 
-                  --  An assignment statement or a procedure call is Ghost when
-                  --  the name denotes a Ghost entity.
+               --  Several pragmas that may apply to a non-Ghost entity are
+               --  treated as Ghost when they contain a reference to a Ghost
+               --  entity (SPARK RM 6.9(12)).
 
-                  elsif Nkind_In (Stmt, N_Assignment_Statement,
-                                        N_Procedure_Call_Statement)
-                  then
-                     return Is_Ghost_Entity_Reference (Name (Stmt));
-                  end if;
+               elsif Nam_In (Prag_Nam, Name_Global,
+                                       Name_Depends,
+                                       Name_Initializes,
+                                       Name_Refined_Global,
+                                       Name_Refined_Depends,
+                                       Name_Refined_State)
+               then
+                  return True;
 
-               --  Prevent the search from going too far
+               --  Otherwise a normal pragma is Ghost when it encloses a Ghost
+               --  name (SPARK RM 6.9(3)).
 
-               elsif Is_Body_Or_Package_Declaration (Stmt) then
-                  return False;
-               end if;
+               else
+                  Arg := First (Pragma_Argument_Associations (Prag));
+                  while Present (Arg) loop
+                     Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
 
-               Stmt := Parent (Stmt);
-            end loop;
+                     if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
+                        return True;
+                     end if;
+
+                     Next (Arg);
+                  end loop;
+               end if;
+            end if;
 
             return False;
-         end Is_Ghost_Statement_Or_Pragma;
+         end Is_OK_Pragma;
 
-      --  Start of processing for Is_OK_Ghost_Context
+         ---------------------
+         -- Is_OK_Statement --
+         ---------------------
 
-      begin
-         --  The Ghost entity appears within an assertion expression
+         function Is_OK_Statement (Stmt : Node_Id) return Boolean is
+            Nam_Id : Entity_Id;
 
-         if In_Assertion_Expr > 0 then
-            return True;
+         begin
+            --  An assignment statement or a procedure call is Ghost when the
+            --  name denotes a Ghost entity.
 
-         --  The Ghost entity is part of a declaration or its completion
+            if Nkind_In (Stmt, N_Assignment_Statement,
+                               N_Procedure_Call_Statement)
+            then
+               Nam_Id := Ghost_Entity (Name (Stmt));
 
-         elsif Is_Ghost_Declaration (Context) then
-            return True;
+               return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
+
+            --  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
+              and then Nkind (Original_Node (Stmt)) = N_Pragma
+              and then Assertion_Expression_Pragma
+                         (Get_Pragma_Id (Original_Node (Stmt)))
+            then
+               return True;
+            end if;
+
+            return False;
+         end Is_OK_Statement;
+
+         --  Local variables
 
-         --  The Ghost entity is referenced within a Ghost statement
+         Par : Node_Id;
 
-         elsif Is_Ghost_Statement_Or_Pragma (Context) then
+      --  Start of processing for Is_OK_Ghost_Context
+
+      begin
+         --  The context is Ghost when it appears within a Ghost package or
+         --  subprogram.
+
+         if Ghost_Mode > None then
             return True;
 
          --  Routine Expand_Record_Extension creates a parent subtype without
@@ -364,7 +441,39 @@ package body Ghost is
          elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
             return True;
 
+         --  Otherwise climb the parent chain looking for a suitable Ghost
+         --  context.
+
          else
+            Par := Context;
+            while Present (Par) loop
+               if Is_Ignored_Ghost_Node (Par) then
+                  return True;
+
+               --  A reference to a Ghost entity can appear within an aspect
+               --  specification (SPARK RM 6.9(11)).
+
+               elsif Nkind (Par) = N_Aspect_Specification then
+                  return True;
+
+               elsif Is_OK_Declaration (Par) then
+                  return True;
+
+               elsif Is_OK_Pragma (Par) then
+                  return True;
+
+               elsif Is_OK_Statement (Par) then
+                  return True;
+
+               --  Prevent the search from going too far
+
+               elsif Is_Body_Or_Package_Declaration (Par) then
+                  return False;
+               end if;
+
+               Par := Parent (Par);
+            end loop;
+
             return False;
          end if;
       end Is_OK_Ghost_Context;
@@ -384,15 +493,15 @@ package body Ghost is
             Error_Msg_Sloc := Sloc (Err_N);
 
             Error_Msg_N  ("incompatible ghost policies in effect", Err_N);
-            Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
-            Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+            Error_Msg_NE ("\& declared with ghost policy `Check`", Err_N, Id);
+            Error_Msg_NE ("\& used # with ghost policy `Ignore`", Err_N, Id);
 
          elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
             Error_Msg_Sloc := Sloc (Err_N);
 
             Error_Msg_N  ("incompatible ghost policies in effect", Err_N);
-            Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
-            Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+            Error_Msg_NE ("\& declared with ghost policy `Ignore`", Err_N, Id);
+            Error_Msg_NE ("\& used # with ghost policy `Check`", Err_N, Id);
          end if;
       end Check_Ghost_Policy;
 
@@ -458,6 +567,75 @@ package body Ghost is
       end if;
    end Check_Ghost_Derivation;
 
+   ----------------------------
+   -- Check_Ghost_Overriding --
+   ----------------------------
+
+   procedure Check_Ghost_Overriding
+     (Subp            : Entity_Id;
+      Overridden_Subp : Entity_Id)
+   is
+      Par_Subp : Entity_Id;
+
+   begin
+      if Present (Subp) and then Present (Overridden_Subp) then
+         Par_Subp := Ultimate_Alias (Overridden_Subp);
+
+         --  The Ghost policy in effect at the point of declaration of a parent
+         --  and an overriding subprogram must match (SPARK RM 6.9(17)).
+
+         if Is_Checked_Ghost_Entity (Par_Subp)
+           and then Is_Ignored_Ghost_Entity (Subp)
+         then
+            Error_Msg_N ("incompatible ghost policies in effect", Subp);
+
+            Error_Msg_Sloc := Sloc (Par_Subp);
+            Error_Msg_N ("\& declared # with ghost policy `Check`", Subp);
+
+            Error_Msg_Sloc := Sloc (Subp);
+            Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
+
+         elsif Is_Ignored_Ghost_Entity (Par_Subp)
+           and then Is_Checked_Ghost_Entity (Subp)
+         then
+            Error_Msg_N ("incompatible ghost policies in effect", Subp);
+
+            Error_Msg_Sloc := Sloc (Par_Subp);
+            Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
+
+            Error_Msg_Sloc := Sloc (Subp);
+            Error_Msg_N ("\overridden # with ghost policy `Check`", Subp);
+         end if;
+      end if;
+   end Check_Ghost_Overriding;
+
+   ------------------
+   -- Ghost_Entity --
+   ------------------
+
+   function Ghost_Entity (N : Node_Id) return Entity_Id is
+      Ref : Node_Id;
+
+   begin
+      --  When the reference extracts a subcomponent, recover the related
+      --  object (SPARK RM 6.9(1)).
+
+      Ref := N;
+      while Nkind_In (Ref, N_Explicit_Dereference,
+                           N_Indexed_Component,
+                           N_Selected_Component,
+                           N_Slice)
+      loop
+         Ref := Prefix (Ref);
+      end loop;
+
+      if Is_Entity_Name (Ref) then
+         return Entity (Ref);
+      else
+         return Empty;
+      end if;
+   end Ghost_Entity;
+
    --------------------------------
    -- Implements_Ghost_Interface --
    --------------------------------
@@ -639,6 +817,67 @@ package body Ghost is
       Ignored_Ghost_Units.Release;
    end Lock;
 
+   -----------------------------
+   -- Mark_Full_View_As_Ghost --
+   -----------------------------
+
+   procedure Mark_Full_View_As_Ghost
+     (Priv_Typ : Entity_Id;
+      Full_Typ : Entity_Id)
+   is
+      Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
+
+   begin
+      if Is_Checked_Ghost_Entity (Priv_Typ) then
+         Set_Is_Checked_Ghost_Entity (Full_Typ);
+
+      elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
+         Set_Is_Ignored_Ghost_Entity (Full_Typ);
+         Set_Is_Ignored_Ghost_Node (Full_Decl);
+         Propagate_Ignored_Ghost_Code (Full_Decl);
+      end if;
+   end Mark_Full_View_As_Ghost;
+
+   --------------------------
+   -- Mark_Pragma_As_Ghost --
+   --------------------------
+
+   procedure Mark_Pragma_As_Ghost
+     (Prag       : Node_Id;
+      Context_Id : Entity_Id)
+   is
+   begin
+      if Is_Checked_Ghost_Entity (Context_Id) then
+         Set_Is_Ghost_Pragma (Prag);
+
+      elsif Is_Ignored_Ghost_Entity (Context_Id) then
+         Set_Is_Ghost_Pragma (Prag);
+         Set_Is_Ignored_Ghost_Node (Prag);
+         Propagate_Ignored_Ghost_Code (Prag);
+      end if;
+   end Mark_Pragma_As_Ghost;
+
+   ----------------------------
+   -- Mark_Renaming_As_Ghost --
+   ----------------------------
+
+   procedure Mark_Renaming_As_Ghost
+     (Ren_Decl : Node_Id;
+      Nam_Id   : Entity_Id)
+   is
+      Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
+
+   begin
+      if Is_Checked_Ghost_Entity (Nam_Id) then
+         Set_Is_Checked_Ghost_Entity (Ren_Id);
+
+      elsif Is_Ignored_Ghost_Entity (Nam_Id) then
+         Set_Is_Ignored_Ghost_Entity (Ren_Id);
+         Set_Is_Ignored_Ghost_Node (Ren_Decl);
+         Propagate_Ignored_Ghost_Code (Ren_Decl);
+      end if;
+   end Mark_Renaming_As_Ghost;
+
    ----------------------------------
    -- Propagate_Ignored_Ghost_Code --
    ----------------------------------
@@ -799,37 +1038,34 @@ package body Ghost is
    -- Set_Ghost_Mode --
    --------------------
 
-   procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is
-      procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+   procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
+      procedure Set_From_Entity (Ent_Id : Entity_Id);
       --  Set the value of global variable Ghost_Mode depending on the mode of
-      --  entity Id.
+      --  entity Ent_Id.
 
-      procedure Set_Ghost_Mode_From_Policy;
+      procedure Set_From_Policy;
       --  Set the value of global variable Ghost_Mode depending on the current
       --  Ghost policy in effect.
 
-      --------------------------------
-      -- Set_Ghost_Mode_From_Entity --
-      --------------------------------
+      ---------------------
+      -- Set_From_Entity --
+      ---------------------
 
-      procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
+      procedure Set_From_Entity (Ent_Id : Entity_Id) is
       begin
-         if Is_Checked_Ghost_Entity (Id) then
-            Ghost_Mode := Check;
-
-         elsif Is_Ignored_Ghost_Entity (Id) then
-            Ghost_Mode := Ignore;
+         Set_Ghost_Mode_From_Entity (Ent_Id);
 
+         if Is_Ignored_Ghost_Entity (Ent_Id) then
             Set_Is_Ignored_Ghost_Node (N);
             Propagate_Ignored_Ghost_Code (N);
          end if;
-      end Set_Ghost_Mode_From_Entity;
+      end Set_From_Entity;
 
-      --------------------------------
-      -- Set_Ghost_Mode_From_Policy --
-      --------------------------------
+      ---------------------
+      -- Set_From_Policy --
+      ---------------------
 
-      procedure Set_Ghost_Mode_From_Policy is
+      procedure Set_From_Policy is
          Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
 
       begin
@@ -842,11 +1078,11 @@ package body Ghost is
             Set_Is_Ignored_Ghost_Node (N);
             Propagate_Ignored_Ghost_Code (N);
          end if;
-      end Set_Ghost_Mode_From_Policy;
+      end Set_From_Policy;
 
       --  Local variables
 
-      Nam : Node_Id;
+      Nam_Id : Entity_Id;
 
    --  Start of processing for Set_Ghost_Mode
 
@@ -856,25 +1092,25 @@ package body Ghost is
 
       if Is_Declaration (N) then
          if Is_Subject_To_Ghost (N) then
-            Set_Ghost_Mode_From_Policy;
+            Set_From_Policy;
 
          --  The declaration denotes the completion of a deferred constant,
          --  pragma Ghost appears on the partial declaration.
 
          elsif Nkind (N) = N_Object_Declaration
            and then Constant_Present (N)
-           and then Present (Prev_Id)
+           and then Present (Id)
          then
-            Set_Ghost_Mode_From_Entity (Prev_Id);
+            Set_From_Entity (Id);
 
          --  The declaration denotes the full view of a private type, pragma
          --  Ghost appears on the partial declaration.
 
          elsif Nkind (N) = N_Full_Type_Declaration
            and then Is_Private_Type (Defining_Entity (N))
-           and then Present (Prev_Id)
+           and then Present (Id)
          then
-            Set_Ghost_Mode_From_Entity (Prev_Id);
+            Set_From_Entity (Id);
          end if;
 
       --  The input denotes an assignment or a procedure call. In this case
@@ -883,48 +1119,50 @@ package body Ghost is
       elsif Nkind_In (N, N_Assignment_Statement,
                          N_Procedure_Call_Statement)
       then
-         --  When the reference extracts a subcomponent, recover the related
-         --  object (SPARK RM 6.9(1)).
-
-         Nam := Name (N);
-         while Nkind_In (Nam, N_Explicit_Dereference,
-                              N_Indexed_Component,
-                              N_Selected_Component,
-                              N_Slice)
-         loop
-            Nam := Prefix (Nam);
-         end loop;
+         Nam_Id := Ghost_Entity (Name (N));
 
-         if Is_Entity_Name (Nam)
-           and then Present (Entity (Nam))
-         then
-            Set_Ghost_Mode_From_Entity (Entity (Nam));
+         if Present (Nam_Id) then
+            Set_From_Entity (Nam_Id);
          end if;
 
       --  The input denotes a package or subprogram body
 
       elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
-         if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id))
+         if (Present (Id) and then Is_Ghost_Entity (Id))
            or else Is_Subject_To_Ghost (N)
          then
-            Set_Ghost_Mode_From_Policy;
+            Set_From_Policy;
+         end if;
+
+      --  The input denotes a pragma
+
+      elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
+         if Is_Ignored_Ghost_Node (N) then
+            Ghost_Mode := Ignore;
+         else
+            Ghost_Mode := Check;
          end if;
+
+      --  The input denotes a freeze node
+
+      elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
+         Set_From_Entity (Id);
       end if;
    end Set_Ghost_Mode;
 
-   -------------------------------
-   -- Set_Ghost_Mode_For_Freeze --
-   -------------------------------
+   --------------------------------
+   -- Set_Ghost_Mode_From_Entity --
+   --------------------------------
 
-   procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
+   procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
    begin
       if Is_Checked_Ghost_Entity (Id) then
          Ghost_Mode := Check;
+
       elsif Is_Ignored_Ghost_Entity (Id) then
          Ghost_Mode := Ignore;
-         Propagate_Ignored_Ghost_Code (N);
       end if;
-   end Set_Ghost_Mode_For_Freeze;
+   end Set_Ghost_Mode_From_Entity;
 
    -------------------------
    -- Set_Is_Ghost_Entity --