ada: Mark attribute Initialized as ghost code

[thirdparty/gcc.git] / gcc / ada / ghost.adb

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                                G H O S T                                 --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--          Copyright (C) 2014-2023, 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- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

with Alloc;
with Aspects;        use Aspects;
with Atree;          use Atree;
with Einfo;          use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils;    use Einfo.Utils;
with Elists;         use Elists;
with Errout;         use Errout;
with Nlists;         use Nlists;
with Nmake;          use Nmake;
with Sem;            use Sem;
with Sem_Aux;        use Sem_Aux;
with Sem_Disp;       use Sem_Disp;
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;
with Sinfo.Nodes;    use Sinfo.Nodes;
with Sinfo.Utils;    use Sinfo.Utils;
with Snames;         use Snames;
with Table;

package body Ghost is

   ---------------------
   -- Data strictures --
   ---------------------

   --  The following table contains all ignored Ghost nodes that must be
   --  eliminated from the tree by routine Remove_Ignored_Ghost_Code.

   package Ignored_Ghost_Nodes is new Table.Table (
     Table_Component_Type => Node_Id,
     Table_Index_Type     => Int,
     Table_Low_Bound      => 0,
     Table_Initial        => Alloc.Ignored_Ghost_Nodes_Initial,
     Table_Increment      => Alloc.Ignored_Ghost_Nodes_Increment,
     Table_Name           => "Ignored_Ghost_Nodes");

   -----------------------
   -- Local subprograms --
   -----------------------

   function Whole_Object_Ref (Ref : Node_Id) return Node_Id;
   --  For a name that denotes an object, returns a name that denotes the whole
   --  object, declared by an object declaration, formal parameter declaration,
   --  etc. For example, for P.X.Comp (J), if P is a package X is a record
   --  object, this returns P.X.

   function Ghost_Entity (Ref : Node_Id) return Entity_Id;
   pragma Inline (Ghost_Entity);
   --  Obtain the entity of a Ghost entity from reference Ref. Return Empty if
   --  no such entity exists.

   procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
   pragma Inline (Install_Ghost_Mode);
   --  Install Ghost mode Mode as the Ghost mode in effect

   procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id);
   pragma Inline (Install_Ghost_Region);
   --  Install a Ghost region comprised of mode Mode and ignored region start
   --  node N.

   function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
   --  Determine whether declaration or body N is subject to aspect or pragma
   --  Ghost. This routine must be used in cases where pragma Ghost has not
   --  been analyzed yet, but the context needs to establish the "ghostness"
   --  of N.

   procedure Mark_Ghost_Declaration_Or_Body
     (N    : Node_Id;
      Mode : Name_Id);
   --  Mark the defining entity of declaration or body N as Ghost depending on
   --  mode Mode. Mark all formals parameters when N denotes a subprogram or a
   --  body.

   procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id);
   --  Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
   --  later elimination.

   ----------------------------
   -- Check_Ghost_Completion --
   ----------------------------

   procedure Check_Ghost_Completion
     (Prev_Id  : Entity_Id;
      Compl_Id : Entity_Id)
   is
      Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);

   begin
      --  Nothing to do if one of the views is missing

      if No (Prev_Id) or else No (Compl_Id) then
         null;

      --  The Ghost policy in effect at the point of declaration and at the
      --  point of completion must match (SPARK RM 6.9(14)).

      elsif Is_Checked_Ghost_Entity (Prev_Id)
        and then Policy = Name_Ignore
      then
         Error_Msg_Sloc := Sloc (Compl_Id);

         Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
         Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id);
         Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);

      elsif Is_Ignored_Ghost_Entity (Prev_Id)
        and then Policy = Name_Check
      then
         Error_Msg_Sloc := Sloc (Compl_Id);

         Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
         Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id);
         Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
      end if;
   end Check_Ghost_Completion;

   -------------------------
   -- Check_Ghost_Context --
   -------------------------

   procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
      procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id);
      --  Verify that the Ghost policy at the point of declaration of entity Id
      --  matches the policy at the point of reference Ref. If this is not the
      --  case emit an error at Ref.

      function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
      --  Determine whether node Context denotes a Ghost-friendly context where
      --  a Ghost entity can safely reside (SPARK RM 6.9(10)).

      function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean;
      --  Return True iff N is enclosed in an aspect or pragma Predicate

      -------------------------
      -- Is_OK_Ghost_Context --
      -------------------------

      function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
         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
         --
         --    * Define a Ghost entity
         --
         --    * Be subject to pragma Ghost

         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
         --
         --    * Be an assertion expression pragma
         --
         --    * Denote pragma Global, Depends, Initializes, Refined_Global,
         --      Refined_Depends or Refined_State.
         --
         --    * Specify an aspect of a Ghost entity
         --
         --    * 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
         --
         --    * Denote a procedure call to a Ghost procedure
         --
         --    * Denote an assignment statement whose target is Ghost

         -----------------------
         -- Is_OK_Declaration --
         -----------------------

         function Is_OK_Declaration (Decl : Node_Id) return Boolean is
            function In_Subprogram_Body_Profile (N : Node_Id) return Boolean;
            --  Determine whether node N appears in the profile of a subprogram
            --  body.

            --------------------------------
            -- In_Subprogram_Body_Profile --
            --------------------------------

            function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is
               Spec : constant Node_Id := Parent (N);

            begin
               --  The node appears in a parameter specification in which case
               --  it is either the parameter type or the default expression or
               --  the node appears as the result definition of a function.

               return
                 (Nkind (N) = N_Parameter_Specification
                   or else
                     (Nkind (Spec) = N_Function_Specification
                       and then N = Result_Definition (Spec)))
                   and then Nkind (Parent (Spec)) = N_Subprogram_Body;
            end In_Subprogram_Body_Profile;

            --  Local variables

            Subp_Decl : Node_Id;
            Subp_Id   : Entity_Id;

         --  Start of processing for Is_OK_Declaration

         begin
            if Is_Ghost_Declaration (Decl) then
               return True;

            --  Special cases

            --  A reference to a Ghost entity may appear within the profile of
            --  a subprogram body. This context is treated as suitable because
            --  it duplicates the context of the corresponding spec. The real
            --  check was already performed during the analysis of the spec.

            elsif In_Subprogram_Body_Profile (Decl) then
               return True;

            --  A reference to a Ghost entity may appear within an expression
            --  function which is still being analyzed. This context is treated
            --  as suitable because it is not yet known whether the expression
            --  function is an initial declaration or a completion. The real
            --  check is performed when the expression function is expanded.

            elsif Nkind (Decl) = N_Expression_Function
              and then not Analyzed (Decl)
            then
               return True;

            --  A reference to a Ghost entity may appear within the class-wide
            --  precondition of a helper subprogram. This context is treated
            --  as suitable because it was already verified when we were
            --  analyzing the original class-wide precondition.

            elsif Is_Subprogram (Current_Scope)
              and then Present (Class_Preconditions_Subprogram (Current_Scope))
            then
               return True;

            --  References to Ghost entities may be relocated in internally
            --  generated bodies.

            elsif Nkind (Decl) = N_Subprogram_Body
              and then not Comes_From_Source (Decl)
            then
               Subp_Id := Corresponding_Spec (Decl);

               if Present (Subp_Id) then

                  --  The context is the internally built _Wrapped_Statements
                  --  procedure, which is OK because the real check was done
                  --  before contract expansion activities.

                  if Chars (Subp_Id) = Name_uWrapped_Statements then
                     return True;

                  --  The context is the internally built predicate function,
                  --  which is OK because the real check was done before the
                  --  predicate function was generated.

                  elsif Is_Predicate_Function (Subp_Id) then
                     return True;

                  else
                     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_Ghost_Declaration (Subp_Decl);
                     end if;
                  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.

               else
                  return True;
               end if;
            end if;

            return False;
         end Is_OK_Declaration;

         ------------------
         -- Is_OK_Pragma --
         ------------------

         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.

            --------------------
            -- Check_Policies --
            --------------------

            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
               --  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

            Prag_Id  : Pragma_Id;
            Prag_Nam : Name_Id;

         --  Start of processing for Is_OK_Pragma

         begin
            if Nkind (Prag) = N_Pragma then
               Prag_Id  := Get_Pragma_Id (Prag);
               Prag_Nam := Original_Aspect_Pragma_Name (Prag);

               --  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 Is_Ghost_Pragma (Prag) then
                  return True;

               --  A pragma may not be analyzed, so that its Ghost status is
               --  not determined yet, but it is guaranteed to be Ghost when
               --  referencing a Ghost entity.

               elsif Prag_Nam in Name_Annotate
                               | Name_Compile_Time_Error
                               | Name_Compile_Time_Warning
                               | Name_Unreferenced
               then
                  return True;

               --  An assertion expression pragma is Ghost when it contains a
               --  reference to a Ghost entity (SPARK RM 6.9(10)), except for
               --  predicate pragmas (SPARK RM 6.9(11)).

               elsif Assertion_Expression_Pragma (Prag_Id)
                 and then Prag_Id /= Pragma_Predicate
               then
                  --  Ensure that the assertion policy and the Ghost policy are
                  --  compatible (SPARK RM 6.9(18)).

                  Check_Policies (Prag_Nam);
                  return True;

               --  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(11)).

               elsif Prag_Nam in Name_Global
                               | Name_Depends
                               | Name_Initializes
                               | Name_Refined_Global
                               | Name_Refined_Depends
                               | Name_Refined_State
               then
                  return True;
               end if;
            end if;

            return False;
         end Is_OK_Pragma;

         ---------------------
         -- Is_OK_Statement --
         ---------------------

         function Is_OK_Statement (Stmt : Node_Id) return Boolean is
         begin
            --  An assignment statement is Ghost when the target is a Ghost
            --  entity.

            if Nkind (Stmt) = N_Assignment_Statement then
               return Is_Ghost_Assignment (Stmt);

            --  A procedure call is Ghost when it calls a Ghost procedure

            elsif Nkind (Stmt) = N_Procedure_Call_Statement then
               return Is_Ghost_Procedure_Call (Stmt);

            --  Special cases

            --  An if statement is a suitable context for a Ghost entity if it
            --  is the byproduct of assertion expression expansion. Note that
            --  the assertion expression may not be related to a Ghost entity,
            --  but it may still contain references to Ghost entities.

            elsif Nkind (Stmt) = N_If_Statement
              and then Comes_From_Check_Or_Contract (Stmt)
            then
               return True;
            end if;

            return False;
         end Is_OK_Statement;

         --  Local variables

         Par : Node_Id;

      --  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
         --  inserting it into the tree. There is no good way of recognizing
         --  this special case as there is no parent. Try to approximate the
         --  context.

         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;

               --  It is not possible to check correct use of Ghost entities
               --  in generic instantiations until after the generic has been
               --  resolved. Postpone that verification to after resolution.

               elsif Nkind (Par) = N_Generic_Association then
                  return True;

               --  A reference to a Ghost entity can appear within an aspect
               --  specification (SPARK RM 6.9(10)). The precise checking will
               --  occur when analyzing the corresponding pragma. We make an
               --  exception for predicate aspects other than Ghost_Predicate
               --  that only allow referencing a Ghost entity when the
               --  corresponding type declaration is Ghost (SPARK RM 6.9(11)).

               elsif Nkind (Par) = N_Aspect_Specification
                 and then
                   (Get_Aspect_Id (Par) = Aspect_Ghost_Predicate
                     or else not Same_Aspect
                                   (Get_Aspect_Id (Par), Aspect_Predicate))
               then
                  return True;

               --  A Ghost type may be referenced in a use or use_type clause
               --  (SPARK RM 6.9(10)).

               elsif Present (Parent (Par))
                 and then Nkind (Parent (Par)) in N_Use_Package_Clause
                                                | N_Use_Type_Clause
               then
                  return True;

               --  The context is an attribute definition clause for a Ghost
               --  entity.

               elsif Nkind (Parent (Par)) = N_Attribute_Definition_Clause
                 and then Par = Name (Parent (Par))
               then
                  return True;

               --  The context is the instantiation or renaming of a Ghost
               --  entity.

               elsif Nkind (Parent (Par)) in N_Generic_Instantiation
                                           | N_Renaming_Declaration
                                           | N_Generic_Renaming_Declaration
                 and then Par = Name (Parent (Par))
               then
                  return True;

               --  In the case of the renaming of a ghost object, the type
               --  itself may be ghost.

               elsif Nkind (Parent (Par)) = N_Object_Renaming_Declaration
                 and then (Par = Subtype_Mark (Parent (Par))
                             or else Par = Access_Definition (Parent (Par)))
               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
                  exit;
               end if;

               Par := Parent (Par);
            end loop;

            --  The expansion of assertion expression pragmas and attribute Old
            --  may cause a legal Ghost entity reference to become illegal due
            --  to node relocation. Check the In_Assertion_Expr counter as last
            --  resort to try and infer the original legal context.

            if In_Assertion_Expr > 0 then
               return True;

            --  Otherwise the context is not suitable for a reference to a
            --  Ghost entity.

            else
               return False;
            end if;
         end if;
      end Is_OK_Ghost_Context;

      ------------------------
      -- Check_Ghost_Policy --
      ------------------------

      procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
         Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);

      begin
         --  The Ghost policy in effect a the point of declaration and at the
         --  point of use must match (SPARK RM 6.9(13)).

         if Is_Checked_Ghost_Entity (Id)
           and then Policy = Name_Ignore
           and then Known_To_Be_Assigned (Ref)
         then
            Error_Msg_Sloc := Sloc (Ref);

            Error_Msg_N  ("incompatible ghost policies in effect", Ref);
            Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id);
            Error_Msg_NE ("\& used # with ghost policy `Ignore`",  Ref, Id);

         elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
            Error_Msg_Sloc := Sloc (Ref);

            Error_Msg_N  ("incompatible ghost policies in effect",  Ref);
            Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id);
            Error_Msg_NE ("\& used # with ghost policy `Check`",    Ref, Id);
         end if;
      end Check_Ghost_Policy;

      -----------------------------------
      -- In_Aspect_Or_Pragma_Predicate --
      -----------------------------------

      function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean is
         Par : Node_Id := N;
      begin
         while Present (Par) loop
            if Nkind (Par) = N_Pragma
              and then Get_Pragma_Id (Par) = Pragma_Predicate
            then
               return True;

            elsif Nkind (Par) = N_Aspect_Specification
              and then Same_Aspect (Get_Aspect_Id (Par), Aspect_Predicate)
            then
               return True;

            --  Stop the search when it's clear it cannot be inside an aspect
            --  or pragma.

            elsif Is_Declaration (Par)
              or else Is_Statement (Par)
              or else Is_Body (Par)
            then
               return False;
            end if;

            Par := Parent (Par);
         end loop;

         return False;
      end In_Aspect_Or_Pragma_Predicate;

   --  Start of processing for Check_Ghost_Context

   begin
      --  Class-wide pre/postconditions of ignored pragmas are preanalyzed
      --  to report errors on wrong conditions; however, ignored pragmas may
      --  also have references to ghost entities and we must disable checking
      --  their context to avoid reporting spurious errors.

      if Inside_Class_Condition_Preanalysis then
         return;
      end if;

      --  When assertions are enabled, compiler generates code for ghost
      --  entities, that is not subject to Ghost policy.

      if not Comes_From_Source (Ghost_Ref) then
         return;
      end if;

      --  Once it has been established that the reference to the Ghost entity
      --  is within a suitable context, ensure that the policy at the point of
      --  declaration and at the point of use match.

      if Is_OK_Ghost_Context (Ghost_Ref) then
         if Present (Ghost_Id) then
            Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
         end if;

      --  Otherwise the Ghost entity appears in a non-Ghost context and affects
      --  its behavior or value (SPARK RM 6.9(10,11)).

      else
         Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);

         --  When the Ghost entity appears in a pragma Predicate, explain the
         --  reason for this being illegal, and suggest a fix instead.

         if In_Aspect_Or_Pragma_Predicate (Ghost_Ref) then
            Error_Msg_N
              ("\as predicates are checked in membership tests, "
               & "the type and its predicate must be both ghost",
               Ghost_Ref);
            Error_Msg_N
              ("\either make the type ghost "
               & "or use a Ghost_Predicate "
               & "or use a type invariant on a private type", Ghost_Ref);
         end if;
      end if;
   end Check_Ghost_Context;

   ------------------------------------------------
   -- Check_Ghost_Context_In_Generic_Association --
   ------------------------------------------------

   procedure Check_Ghost_Context_In_Generic_Association
     (Actual : Node_Id;
      Formal : Entity_Id)
   is
      function Emit_Error_On_Ghost_Reference
        (N : Node_Id)
         return Traverse_Result;
      --  Determine wether N denotes a reference to a ghost entity, and if so
      --  issue an error.

      -----------------------------------
      -- Emit_Error_On_Ghost_Reference --
      -----------------------------------

      function Emit_Error_On_Ghost_Reference
        (N : Node_Id)
         return Traverse_Result
      is
      begin
         if Is_Entity_Name (N)
           and then Present (Entity (N))
           and then Is_Ghost_Entity (Entity (N))
         then
            Error_Msg_N ("ghost entity cannot appear in this context", N);
            Error_Msg_Sloc := Sloc (Formal);
            Error_Msg_NE ("\formal & was not declared as ghost #", N, Formal);
            return Abandon;
         end if;

         return OK;
      end Emit_Error_On_Ghost_Reference;

      procedure Check_Ghost_References is
        new Traverse_Proc (Emit_Error_On_Ghost_Reference);

   --  Start of processing for Check_Ghost_Context_In_Generic_Association

   begin
      --  The context is ghost when it appears within a Ghost package or
      --  subprogram.

      if Ghost_Mode > None then
         return;

      --  The context is ghost if Formal is explicitly marked as ghost

      elsif Is_Ghost_Entity (Formal) then
         return;

      else
         Check_Ghost_References (Actual);
      end if;
   end Check_Ghost_Context_In_Generic_Association;

   ---------------------------------------------
   -- Check_Ghost_Formal_Procedure_Or_Package --
   ---------------------------------------------

   procedure Check_Ghost_Formal_Procedure_Or_Package
     (N          : Node_Id;
      Actual     : Entity_Id;
      Formal     : Entity_Id;
      Is_Default : Boolean := False)
   is
   begin
      if not Is_Ghost_Entity (Formal) then
         return;
      end if;

      if Present (Actual) and then Is_Ghost_Entity (Actual) then
         return;
      end if;

      if Is_Default then
         Error_Msg_N ("ghost procedure expected as default", N);
         Error_Msg_NE ("\formal & is declared as ghost", N, Formal);

      else
         if Ekind (Formal) = E_Procedure then
            Error_Msg_N ("ghost procedure expected for actual", N);
         else
            Error_Msg_N ("ghost package expected for actual", N);
         end if;

         Error_Msg_Sloc := Sloc (Formal);
         Error_Msg_NE ("\formal & was declared as ghost #", N, Formal);
      end if;
   end Check_Ghost_Formal_Procedure_Or_Package;

   ---------------------------------
   -- Check_Ghost_Formal_Variable --
   ---------------------------------

   procedure Check_Ghost_Formal_Variable
     (Actual     : Node_Id;
      Formal     : Entity_Id;
      Is_Default : Boolean := False)
   is
      Actual_Obj : constant Entity_Id := Get_Enclosing_Deep_Object (Actual);
   begin
      if not Is_Ghost_Entity (Formal) then
         return;
      end if;

      if No (Actual_Obj)
        or else not Is_Ghost_Entity (Actual_Obj)
      then
         if Is_Default then
            Error_Msg_N ("ghost object expected as default", Actual);
            Error_Msg_NE ("\formal & is declared as ghost", Actual, Formal);
         else
            Error_Msg_N ("ghost object expected for mutable actual", Actual);
            Error_Msg_Sloc := Sloc (Formal);
            Error_Msg_NE ("\formal & was declared as ghost #", Actual, Formal);
         end if;
      end if;
   end Check_Ghost_Formal_Variable;

   ----------------------------
   -- Check_Ghost_Overriding --
   ----------------------------

   procedure Check_Ghost_Overriding
     (Subp            : Entity_Id;
      Overridden_Subp : Entity_Id)
   is
      Deriv_Typ : Entity_Id;
      Over_Subp : Entity_Id;

   begin
      if Present (Subp) and then Present (Overridden_Subp) then
         Over_Subp := Ultimate_Alias (Overridden_Subp);
         Deriv_Typ := Find_Dispatching_Type (Subp);

         --  A Ghost primitive of a non-Ghost type extension cannot override an
         --  inherited non-Ghost primitive (SPARK RM 6.9(8)).

         if Is_Ghost_Entity (Subp)
           and then Present (Deriv_Typ)
           and then not Is_Ghost_Entity (Deriv_Typ)
           and then not Is_Ghost_Entity (Over_Subp)
           and then not Is_Abstract_Subprogram (Over_Subp)
         then
            Error_Msg_N ("incompatible overriding in effect", Subp);

            Error_Msg_Sloc := Sloc (Over_Subp);
            Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);

            Error_Msg_Sloc := Sloc (Subp);
            Error_Msg_N ("\overridden # with ghost subprogram", Subp);
         end if;

         --  A non-Ghost primitive of a type extension cannot override an
         --  inherited Ghost primitive (SPARK RM 6.9(8)).

         if Is_Ghost_Entity (Over_Subp)
           and then not Is_Ghost_Entity (Subp)
           and then not Is_Abstract_Subprogram (Subp)
         then
            Error_Msg_N ("incompatible overriding in effect", Subp);

            Error_Msg_Sloc := Sloc (Over_Subp);
            Error_Msg_N ("\& declared # as ghost subprogram", Subp);

            Error_Msg_Sloc := Sloc (Subp);
            Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
         end if;

         if Present (Deriv_Typ)
           and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
         then
            --  When a tagged type is either non-Ghost or checked Ghost and
            --  one of its primitives overrides an inherited operation, the
            --  overridden operation of the ancestor type must be ignored Ghost
            --  if the primitive is ignored Ghost (SPARK RM 6.9(17)).

            if Is_Ignored_Ghost_Entity (Subp) then

               --  Both the parent subprogram and overriding subprogram are
               --  ignored Ghost.

               if Is_Ignored_Ghost_Entity (Over_Subp) then
                  null;

               --  The parent subprogram carries policy Check

               elsif Is_Checked_Ghost_Entity (Over_Subp) then
                  Error_Msg_N
                    ("incompatible ghost policies in effect", Subp);

                  Error_Msg_Sloc := Sloc (Over_Subp);
                  Error_Msg_N
                    ("\& declared # with ghost policy `Check`", Subp);

                  Error_Msg_Sloc := Sloc (Subp);
                  Error_Msg_N
                    ("\overridden # with ghost policy `Ignore`", Subp);

               --  The parent subprogram is non-Ghost

               else
                  Error_Msg_N
                    ("incompatible ghost policies in effect", Subp);

                  Error_Msg_Sloc := Sloc (Over_Subp);
                  Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);

                  Error_Msg_Sloc := Sloc (Subp);
                  Error_Msg_N
                    ("\overridden # with ghost policy `Ignore`", Subp);
               end if;

            --  When a tagged type is either non-Ghost or checked Ghost and
            --  one of its primitives overrides an inherited operation, the
            --  the primitive of the tagged type must be ignored Ghost if the
            --  overridden operation is ignored Ghost (SPARK RM 6.9(17)).

            elsif Is_Ignored_Ghost_Entity (Over_Subp) then

               --  Both the parent subprogram and the overriding subprogram are
               --  ignored Ghost.

               if Is_Ignored_Ghost_Entity (Subp) then
                  null;

               --  The overriding subprogram carries policy Check

               elsif Is_Checked_Ghost_Entity (Subp) then
                  Error_Msg_N
                    ("incompatible ghost policies in effect", Subp);

                  Error_Msg_Sloc := Sloc (Over_Subp);
                  Error_Msg_N
                    ("\& declared # with ghost policy `Ignore`", Subp);

                  Error_Msg_Sloc := Sloc (Subp);
                  Error_Msg_N
                    ("\overridden # with Ghost policy `Check`", Subp);

               --  The overriding subprogram is non-Ghost

               else
                  Error_Msg_N
                    ("incompatible ghost policies in effect", Subp);

                  Error_Msg_Sloc := Sloc (Over_Subp);
                  Error_Msg_N
                    ("\& declared # with ghost policy `Ignore`", Subp);

                  Error_Msg_Sloc := Sloc (Subp);
                  Error_Msg_N
                    ("\overridden # with non-ghost subprogram", Subp);
               end if;
            end if;
         end if;
      end if;
   end Check_Ghost_Overriding;

   ---------------------------
   -- Check_Ghost_Primitive --
   ---------------------------

   procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
   begin
      --  The Ghost policy in effect at the point of declaration of a primitive
      --  operation and a tagged type must match (SPARK RM 6.9(16)).

      if Is_Tagged_Type (Typ) then
         if Is_Checked_Ghost_Entity (Prim)
           and then Is_Ignored_Ghost_Entity (Typ)
         then
            Error_Msg_N ("incompatible ghost policies in effect", Prim);

            Error_Msg_Sloc := Sloc (Typ);
            Error_Msg_NE
              ("\tagged type & declared # with ghost policy `Ignore`",
               Prim, Typ);

            Error_Msg_Sloc := Sloc (Prim);
            Error_Msg_N
              ("\primitive subprogram & declared # with ghost policy `Check`",
               Prim);

         elsif Is_Ignored_Ghost_Entity (Prim)
           and then Is_Checked_Ghost_Entity (Typ)
         then
            Error_Msg_N ("incompatible ghost policies in effect", Prim);

            Error_Msg_Sloc := Sloc (Typ);
            Error_Msg_NE
              ("\tagged type & declared # with ghost policy `Check`",
               Prim, Typ);

            Error_Msg_Sloc := Sloc (Prim);
            Error_Msg_N
              ("\primitive subprogram & declared # with ghost policy `Ignore`",
               Prim);
         end if;
      end if;
   end Check_Ghost_Primitive;

   ----------------------------
   -- Check_Ghost_Refinement --
   ----------------------------

   procedure Check_Ghost_Refinement
     (State      : Node_Id;
      State_Id   : Entity_Id;
      Constit    : Node_Id;
      Constit_Id : Entity_Id)
   is
   begin
      if Is_Ghost_Entity (State_Id) then
         if Is_Ghost_Entity (Constit_Id) then

            --  The Ghost policy in effect at the point of abstract state
            --  declaration and constituent must match (SPARK RM 6.9(15)).

            if Is_Checked_Ghost_Entity (State_Id)
              and then Is_Ignored_Ghost_Entity (Constit_Id)
            then
               Error_Msg_Sloc := Sloc (Constit);
               SPARK_Msg_N ("incompatible ghost policies in effect", State);

               SPARK_Msg_NE
                 ("\abstract state & declared with ghost policy `Check`",
                  State, State_Id);
               SPARK_Msg_NE
                 ("\constituent & declared # with ghost policy `Ignore`",
                  State, Constit_Id);

            elsif Is_Ignored_Ghost_Entity (State_Id)
              and then Is_Checked_Ghost_Entity (Constit_Id)
            then
               Error_Msg_Sloc := Sloc (Constit);
               SPARK_Msg_N ("incompatible ghost policies in effect", State);

               SPARK_Msg_NE
                 ("\abstract state & declared with ghost policy `Ignore`",
                  State, State_Id);
               SPARK_Msg_NE
                 ("\constituent & declared # with ghost policy `Check`",
                  State, Constit_Id);
            end if;

            --  A constituent of a Ghost abstract state must be a Ghost entity
            --  (SPARK RM 7.2.2(12)).

         else
            SPARK_Msg_NE
              ("constituent of ghost state & must be ghost",
               Constit, State_Id);
         end if;
      end if;
   end Check_Ghost_Refinement;

   ----------------------
   -- Check_Ghost_Type --
   ----------------------

   procedure Check_Ghost_Type (Typ : Entity_Id) is
      Conc_Typ : Entity_Id;
      Full_Typ : Entity_Id;

   begin
      if Is_Ghost_Entity (Typ) then
         Conc_Typ := Empty;
         Full_Typ := Typ;

         if Is_Single_Concurrent_Type (Typ) then
            Conc_Typ := Anonymous_Object (Typ);
            Full_Typ := Conc_Typ;

         elsif Is_Concurrent_Type (Typ) then
            Conc_Typ := Typ;
         end if;

         --  A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
         --  legality rule first to give a finer-grained diagnostic.

         if Present (Conc_Typ) then
            Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
         end if;

         --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))

         if Is_Effectively_Volatile (Full_Typ) then
            Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
         end if;
      end if;
   end Check_Ghost_Type;

   ------------------
   -- Ghost_Entity --
   ------------------

   function Ghost_Entity (Ref : Node_Id) return Entity_Id is
      Obj_Ref : constant Node_Id := Ultimate_Prefix (Ref);

   begin
      --  When the reference denotes a subcomponent, recover the related whole
      --  object (SPARK RM 6.9(1)).

      if Is_Entity_Name (Obj_Ref) then
         return Entity (Obj_Ref);

      --  Otherwise the reference cannot possibly denote a Ghost entity

      else
         return Empty;
      end if;
   end Ghost_Entity;

   --------------------------------
   -- Implements_Ghost_Interface --
   --------------------------------

   function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
      Iface_Elmt : Elmt_Id;

   begin
      --  Traverse the list of interfaces looking for a Ghost interface

      if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
         Iface_Elmt := First_Elmt (Interfaces (Typ));
         while Present (Iface_Elmt) loop
            if Is_Ghost_Entity (Node (Iface_Elmt)) then
               return True;
            end if;

            Next_Elmt (Iface_Elmt);
         end loop;
      end if;

      return False;
   end Implements_Ghost_Interface;

   ----------------
   -- Initialize --
   ----------------

   procedure Initialize is
   begin
      Ignored_Ghost_Nodes.Init;

      --  Set the soft link which enables Atree.Mark_New_Ghost_Node to record
      --  an ignored Ghost node or entity.

      Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access);
   end Initialize;

   ------------------------
   -- Install_Ghost_Mode --
   ------------------------

   procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
   begin
      Install_Ghost_Region (Mode, Empty);
   end Install_Ghost_Mode;

   --------------------------
   -- Install_Ghost_Region --
   --------------------------

   procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
   begin
      --  The context is already within an ignored Ghost region. Maintain the
      --  start of the outermost ignored Ghost region.

      if Present (Ignored_Ghost_Region) then
         null;

      --  The current region is the outermost ignored Ghost region. Save its
      --  starting node.

      elsif Present (N) and then Mode = Ignore then
         Ignored_Ghost_Region := N;

      --  Otherwise the current region is not ignored, nothing to save

      else
         Ignored_Ghost_Region := Empty;
      end if;

      Ghost_Mode := Mode;
   end Install_Ghost_Region;

   procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is
   begin
      Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N);
   end Install_Ghost_Region;

   -------------------------
   -- Is_Ghost_Assignment --
   -------------------------

   function Is_Ghost_Assignment (N : Node_Id) return Boolean is
      Id : Entity_Id;

   begin
      --  An assignment statement is Ghost when its target denotes a Ghost
      --  entity.

      if Nkind (N) = N_Assignment_Statement then
         Id := Ghost_Entity (Name (N));

         return Present (Id) and then Is_Ghost_Entity (Id);
      end if;

      return False;
   end Is_Ghost_Assignment;

   ----------------------------------
   -- Is_Ghost_Attribute_Reference --
   ----------------------------------

   function Is_Ghost_Attribute_Reference (N : Node_Id) return Boolean is
   begin
      return Nkind (N) = N_Attribute_Reference
        and then Attribute_Name (N) = Name_Initialized;
   end Is_Ghost_Attribute_Reference;

   --------------------------
   -- Is_Ghost_Declaration --
   --------------------------

   function Is_Ghost_Declaration (N : Node_Id) return Boolean is
      Id : Entity_Id;

   begin
      --  A declaration is Ghost when it elaborates a Ghost entity or is
      --  subject to pragma Ghost.

      if Is_Declaration (N) then
         Id := Defining_Entity (N);

         return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N);
      end if;

      return False;
   end Is_Ghost_Declaration;

   ---------------------
   -- Is_Ghost_Pragma --
   ---------------------

   function Is_Ghost_Pragma (N : Node_Id) return Boolean is
   begin
      return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N);
   end Is_Ghost_Pragma;

   -----------------------------
   -- Is_Ghost_Procedure_Call --
   -----------------------------

   function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is
      Id : Entity_Id;

   begin
      --  A procedure call is Ghost when it invokes a Ghost procedure

      if Nkind (N) = N_Procedure_Call_Statement then
         Id := Ghost_Entity (Name (N));

         return Present (Id) and then Is_Ghost_Entity (Id);
      end if;

      return False;
   end Is_Ghost_Procedure_Call;

   ---------------------------
   -- Is_Ignored_Ghost_Unit --
   ---------------------------

   function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is
      function Ultimate_Original_Node (Nod : Node_Id) return Node_Id;
      --  Obtain the original node of arbitrary node Nod following a potential
      --  chain of rewritings.

      ----------------------------
      -- Ultimate_Original_Node --
      ----------------------------

      function Ultimate_Original_Node (Nod : Node_Id) return Node_Id is
         Res : Node_Id := Nod;
      begin
         while Is_Rewrite_Substitution (Res) loop
            Res := Original_Node (Res);
         end loop;

         return Res;
      end Ultimate_Original_Node;

   --  Start of processing for Is_Ignored_Ghost_Unit

   begin
      --  Inspect the original node of the unit in case removal of ignored
      --  Ghost code has already taken place.

      return
        Nkind (N) = N_Compilation_Unit
          and then Is_Ignored_Ghost_Entity
                     (Defining_Entity (Ultimate_Original_Node (Unit (N))));
   end Is_Ignored_Ghost_Unit;

   -------------------------
   -- Is_Subject_To_Ghost --
   -------------------------

   function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
      function Enables_Ghostness (Arg : Node_Id) return Boolean;
      --  Determine whether aspect or pragma argument Arg enables "ghostness"

      -----------------------
      -- Enables_Ghostness --
      -----------------------

      function Enables_Ghostness (Arg : Node_Id) return Boolean is
         Expr : Node_Id;

      begin
         Expr := Arg;

         if Nkind (Expr) = N_Pragma_Argument_Association then
            Expr := Get_Pragma_Arg (Expr);
         end if;

         --  Determine whether the expression of the aspect or pragma is static
         --  and denotes True.

         if Present (Expr) then
            Preanalyze_And_Resolve (Expr);

            return
              Is_OK_Static_Expression (Expr)
                and then Is_True (Expr_Value (Expr));

         --  Otherwise Ghost defaults to True

         else
            return True;
         end if;
      end Enables_Ghostness;

      --  Local variables

      Id      : constant Entity_Id := Defining_Entity (N);
      Asp     : Node_Id;
      Decl    : Node_Id;
      Prev_Id : Entity_Id;

   --  Start of processing for Is_Subject_To_Ghost

   begin
      --  The related entity of the declaration has not been analyzed yet, do
      --  not inspect its attributes.

      if Ekind (Id) = E_Void then
         null;

      elsif Is_Ghost_Entity (Id) then
         return True;

      --  The completion of a type or a constant is not fully analyzed when the
      --  reference to the Ghost entity is resolved. Because the completion is
      --  not marked as Ghost yet, inspect the partial view.

      elsif Is_Record_Type (Id)
        or else Ekind (Id) = E_Constant
        or else (Nkind (N) = N_Object_Declaration
                  and then Constant_Present (N))
      then
         Prev_Id := Incomplete_Or_Partial_View (Id);

         if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
            return True;
         end if;
      end if;

      --  Examine the aspect specifications (if any) looking for aspect Ghost

      if Permits_Aspect_Specifications (N) then
         Asp := First (Aspect_Specifications (N));
         while Present (Asp) loop
            if Chars (Identifier (Asp)) = Name_Ghost then
               return Enables_Ghostness (Expression (Asp));
            end if;

            Next (Asp);
         end loop;
      end if;

      Decl := Empty;

      --  When the context is a [generic] package declaration, pragma Ghost
      --  resides in the visible declarations.

      if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration
      then
         Decl := First (Visible_Declarations (Specification (N)));

      --  When the context is a package or a subprogram body, pragma Ghost
      --  resides in the declarative part.

      elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then
         Decl := First (Declarations (N));

      --  Otherwise pragma Ghost appears in the declarations following N

      elsif Is_List_Member (N) then
         Decl := Next (N);
      end if;

      while Present (Decl) loop
         if Nkind (Decl) = N_Pragma
           and then Pragma_Name (Decl) = Name_Ghost
         then
            return
              Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));

         --  A source construct ends the region where pragma Ghost may appear,
         --  stop the traversal. Check the original node as source constructs
         --  may be rewritten into something else by expansion.

         elsif Comes_From_Source (Original_Node (Decl)) then
            exit;
         end if;

         Next (Decl);
      end loop;

      return False;
   end Is_Subject_To_Ghost;

   ----------
   -- Lock --
   ----------

   procedure Lock is
   begin
      Ignored_Ghost_Nodes.Release;
      Ignored_Ghost_Nodes.Locked := True;
   end Lock;

   -----------------------------------
   -- Mark_And_Set_Ghost_Assignment --
   -----------------------------------

   procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is
      --  A ghost assignment is an assignment whose left-hand side denotes a
      --  ghost object. Subcomponents are not marked "ghost", so we need to
      --  find the containing "whole" object. So, for "P.X.Comp (J) := ...",
      --  where P is a package, X is a record, and Comp is an array, we need
      --  to check the ghost flags of X.

      Orig_Lhs : constant Node_Id := Name (N);
   begin
      --  Ghost assignments are irrelevant when the expander is inactive, and
      --  processing them in that mode can lead to spurious errors.

      if Expander_Active then
         --  Cases where full analysis is needed, involving array indexing
         --  which would otherwise be missing array-bounds checks:

         if not Analyzed (Orig_Lhs)
           and then
             ((Nkind (Orig_Lhs) = N_Indexed_Component
                and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component
                and then Nkind (Prefix (Prefix (Orig_Lhs))) =
                           N_Indexed_Component)
              or else
             (Nkind (Orig_Lhs) = N_Selected_Component
              and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component
              and then Nkind (Prefix (Prefix (Orig_Lhs))) =
                         N_Selected_Component
              and then Nkind (Parent (N)) /= N_Loop_Statement))
         then
            Analyze (Orig_Lhs);
         end if;

         --  Make sure Lhs is at least preanalyzed, so we can tell whether
         --  it denotes a ghost variable. In some cases we need to do a full
         --  analysis, or else the back end gets confused. Note that in the
         --  preanalysis case, we are preanalyzing a copy of the left-hand
         --  side name, temporarily attached to the tree.

         declare
            Lhs : constant Node_Id :=
              (if Analyzed (Orig_Lhs) then Orig_Lhs
               else New_Copy_Tree (Orig_Lhs));
         begin
            if not Analyzed (Lhs) then
               Set_Name   (N, Lhs);
               Set_Parent (Lhs, N);
               Preanalyze_Without_Errors (Lhs);
               Set_Name (N, Orig_Lhs);
            end if;

            declare
               Whole : constant Node_Id := Whole_Object_Ref (Lhs);
               Id    : Entity_Id;
            begin
               if Is_Entity_Name (Whole) then
                  Id := Entity (Whole);

                  if Present (Id) then
                     --  Left-hand side denotes a Checked ghost entity, so
                     --  install the region.

                     if Is_Checked_Ghost_Entity (Id) then
                        Install_Ghost_Region (Check, N);

                     --  Left-hand side denotes an Ignored ghost entity, so
                     --  install the region, and mark the assignment statement
                     --  as an ignored ghost assignment, so it will be removed
                     --  later.

                     elsif Is_Ignored_Ghost_Entity (Id) then
                        Install_Ghost_Region (Ignore, N);
                        Set_Is_Ignored_Ghost_Node (N);
                        Record_Ignored_Ghost_Node (N);
                     end if;
                  end if;
               end if;
            end;
         end;
      end if;
   end Mark_And_Set_Ghost_Assignment;

   -----------------------------
   -- Mark_And_Set_Ghost_Body --
   -----------------------------

   procedure Mark_And_Set_Ghost_Body
     (N       : Node_Id;
      Spec_Id : Entity_Id)
   is
      Body_Id : constant Entity_Id := Defining_Entity (N);
      Policy  : Name_Id := No_Name;

   begin
      --  A body becomes Ghost when it is subject to aspect or pragma Ghost

      if Is_Subject_To_Ghost (N) then
         Policy := Policy_In_Effect (Name_Ghost);

      --  A body declared within a Ghost region is automatically Ghost
      --  (SPARK RM 6.9(2)).

      elsif Ghost_Mode = Check then
         Policy := Name_Check;

      elsif Ghost_Mode = Ignore then
         Policy := Name_Ignore;

      --  Inherit the "ghostness" of the previous declaration when the body
      --  acts as a completion.

      elsif Present (Spec_Id) then
         if Is_Checked_Ghost_Entity (Spec_Id) then
            Policy := Name_Check;

         elsif Is_Ignored_Ghost_Entity (Spec_Id) then
            Policy := Name_Ignore;
         end if;
      end if;

      --  The Ghost policy in effect at the point of declaration and at the
      --  point of completion must match (SPARK RM 6.9(14)).

      Check_Ghost_Completion
        (Prev_Id  => Spec_Id,
         Compl_Id => Body_Id);

      --  Mark the body as its formals as Ghost

      Mark_Ghost_Declaration_Or_Body (N, Policy);

      --  Install the appropriate Ghost region

      Install_Ghost_Region (Policy, N);
   end Mark_And_Set_Ghost_Body;

   -----------------------------------
   -- Mark_And_Set_Ghost_Completion --
   -----------------------------------

   procedure Mark_And_Set_Ghost_Completion
     (N       : Node_Id;
      Prev_Id : Entity_Id)
   is
      Compl_Id : constant Entity_Id := Defining_Entity (N);
      Policy   : Name_Id := No_Name;

   begin
      --  A completion elaborated in a Ghost region is automatically Ghost
      --  (SPARK RM 6.9(2)).

      if Ghost_Mode = Check then
         Policy := Name_Check;

      elsif Ghost_Mode = Ignore then
         Policy := Name_Ignore;

      --  The completion becomes Ghost when its initial declaration is also
      --  Ghost.

      elsif Is_Checked_Ghost_Entity (Prev_Id) then
         Policy := Name_Check;

      elsif Is_Ignored_Ghost_Entity (Prev_Id) then
         Policy := Name_Ignore;
      end if;

      --  The Ghost policy in effect at the point of declaration and at the
      --  point of completion must match (SPARK RM 6.9(14)).

      Check_Ghost_Completion
        (Prev_Id  => Prev_Id,
         Compl_Id => Compl_Id);

      --  Mark the completion as Ghost

      Mark_Ghost_Declaration_Or_Body (N, Policy);

      --  Install the appropriate Ghost region

      Install_Ghost_Region (Policy, N);
   end Mark_And_Set_Ghost_Completion;

   ------------------------------------
   -- Mark_And_Set_Ghost_Declaration --
   ------------------------------------

   procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is
      Par_Id : Entity_Id;
      Policy : Name_Id := No_Name;

   begin
      --  A declaration becomes Ghost when it is subject to aspect or pragma
      --  Ghost.

      if Is_Subject_To_Ghost (N) then
         Policy := Policy_In_Effect (Name_Ghost);

      --  A declaration elaborated in a Ghost region is automatically Ghost
      --  (SPARK RM 6.9(2)).

      elsif Ghost_Mode = Check then
         Policy := Name_Check;

      elsif Ghost_Mode = Ignore then
         Policy := Name_Ignore;

      --  A child package or subprogram declaration becomes Ghost when its
      --  parent is Ghost (SPARK RM 6.9(2)).

      elsif Nkind (N) in N_Generic_Function_Renaming_Declaration
                       | N_Generic_Package_Declaration
                       | N_Generic_Package_Renaming_Declaration
                       | N_Generic_Procedure_Renaming_Declaration
                       | N_Generic_Subprogram_Declaration
                       | N_Package_Declaration
                       | N_Package_Renaming_Declaration
                       | N_Subprogram_Declaration
                       | N_Subprogram_Renaming_Declaration
        and then Present (Parent_Spec (N))
      then
         Par_Id := Defining_Entity (Unit (Parent_Spec (N)));

         if Is_Checked_Ghost_Entity (Par_Id) then
            Policy := Name_Check;

         elsif Is_Ignored_Ghost_Entity (Par_Id) then
            Policy := Name_Ignore;
         end if;
      end if;

      --  Mark the declaration and its formals as Ghost

      Mark_Ghost_Declaration_Or_Body (N, Policy);

      --  Install the appropriate Ghost region

      Install_Ghost_Region (Policy, N);
   end Mark_And_Set_Ghost_Declaration;

   --------------------------------------
   -- Mark_And_Set_Ghost_Instantiation --
   --------------------------------------

   procedure Mark_And_Set_Ghost_Instantiation
     (N      : Node_Id;
      Gen_Id : Entity_Id)
   is
      procedure Check_Ghost_Actuals;
      --  Check the context of ghost actuals

      -------------------------
      -- Check_Ghost_Actuals --
      -------------------------

      procedure Check_Ghost_Actuals is
         Assoc : Node_Id := First (Generic_Associations (N));
         Act   : Node_Id;

      begin
         while Present (Assoc) loop
            if Nkind (Assoc) /= N_Others_Choice then
               Act := Explicit_Generic_Actual_Parameter (Assoc);

               --  Within a nested instantiation, a defaulted actual is an
               --  empty association, so nothing to check.

               if No (Act) then
                  null;

               elsif Comes_From_Source (Act)
                  and then Nkind (Act) in N_Has_Etype
                  and then Present (Etype (Act))
                  and then Is_Ghost_Entity (Etype (Act))
               then
                  Check_Ghost_Context (Etype (Act), Act);
               end if;
            end if;

            Next (Assoc);
         end loop;
      end Check_Ghost_Actuals;

      --  Local variables

      Policy : Name_Id := No_Name;

   begin
      --  An instantiation becomes Ghost when it is subject to pragma Ghost

      if Is_Subject_To_Ghost (N) then
         Policy := Policy_In_Effect (Name_Ghost);

      --  An instantiation declaration within a Ghost region is automatically
      --  Ghost (SPARK RM 6.9(2)).

      elsif Ghost_Mode = Check then
         Policy := Name_Check;

      elsif Ghost_Mode = Ignore then
         Policy := Name_Ignore;

      --  Inherit the "ghostness" of the generic unit

      elsif Is_Checked_Ghost_Entity (Gen_Id) then
         Policy := Name_Check;

      elsif Is_Ignored_Ghost_Entity (Gen_Id) then
         Policy := Name_Ignore;
      end if;

      --  Mark the instantiation as Ghost

      Mark_Ghost_Declaration_Or_Body (N, Policy);

      --  Install the appropriate Ghost region

      Install_Ghost_Region (Policy, N);

      --  Check Ghost actuals. Given that this routine is unconditionally
      --  invoked with subprogram and package instantiations, this check
      --  verifies the context of all the ghost entities passed in generic
      --  instantiations.

      Check_Ghost_Actuals;
   end Mark_And_Set_Ghost_Instantiation;

   ---------------------------------------
   -- Mark_And_Set_Ghost_Procedure_Call --
   ---------------------------------------

   procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is
      Id : Entity_Id;

   begin
      --  A procedure call becomes Ghost when the procedure being invoked is
      --  Ghost. Install the Ghost mode of the procedure.

      Id := Ghost_Entity (Name (N));

      if Present (Id) then
         if Is_Checked_Ghost_Entity (Id) then
            Install_Ghost_Region (Check, N);

         elsif Is_Ignored_Ghost_Entity (Id) then
            Install_Ghost_Region (Ignore, N);

            Set_Is_Ignored_Ghost_Node (N);
            Record_Ignored_Ghost_Node (N);
         end if;
      end if;
   end Mark_And_Set_Ghost_Procedure_Call;

   -----------------------
   -- Mark_Ghost_Clause --
   -----------------------

   procedure Mark_Ghost_Clause (N : Node_Id) is
      Nam : Node_Id := Empty;

   begin
      if Nkind (N) = N_Use_Package_Clause then
         Nam := Name (N);

      elsif Nkind (N) = N_Use_Type_Clause then
         Nam := Subtype_Mark (N);

      elsif Nkind (N) = N_With_Clause then
         Nam := Name (N);
      end if;

      if Present (Nam)
        and then Is_Entity_Name (Nam)
        and then Present (Entity (Nam))
        and then Is_Ignored_Ghost_Entity (Entity (Nam))
      then
         Set_Is_Ignored_Ghost_Node (N);
         Record_Ignored_Ghost_Node (N);
      end if;
   end Mark_Ghost_Clause;

   ------------------------------------
   -- Mark_Ghost_Declaration_Or_Body --
   ------------------------------------

   procedure Mark_Ghost_Declaration_Or_Body
     (N    : Node_Id;
      Mode : Name_Id)
   is
      Id : constant Entity_Id := Defining_Entity (N);

      Mark_Formals : Boolean := False;
      Param        : Node_Id;
      Param_Id     : Entity_Id;

   begin
      --  Mark the related node and its entity

      if Mode = Name_Check then
         Mark_Formals := True;
         Set_Is_Checked_Ghost_Entity (Id);

      elsif Mode = Name_Ignore then
         Mark_Formals := True;
         Set_Is_Ignored_Ghost_Entity (Id);
         Set_Is_Ignored_Ghost_Node (N);
         Record_Ignored_Ghost_Node (N);
      end if;

      --  Mark all formal parameters when the related node denotes a subprogram
      --  or a body. The traversal is performed via the specification because
      --  the related subprogram or body may be unanalyzed.

      --  ??? could extra formal parameters cause a Ghost leak?

      if Mark_Formals
        and then Nkind (N) in N_Abstract_Subprogram_Declaration
                            | N_Formal_Abstract_Subprogram_Declaration
                            | N_Formal_Concrete_Subprogram_Declaration
                            | N_Generic_Subprogram_Declaration
                            | N_Subprogram_Body
                            | N_Subprogram_Body_Stub
                            | N_Subprogram_Declaration
                            | N_Subprogram_Renaming_Declaration
      then
         Param := First (Parameter_Specifications (Specification (N)));
         while Present (Param) loop
            Param_Id := Defining_Entity (Param);

            if Mode = Name_Check then
               Set_Is_Checked_Ghost_Entity (Param_Id);

            elsif Mode = Name_Ignore then
               Set_Is_Ignored_Ghost_Entity (Param_Id);
            end if;

            Next (Param);
         end loop;
      end if;
   end Mark_Ghost_Declaration_Or_Body;

   -----------------------
   -- Mark_Ghost_Pragma --
   -----------------------

   procedure Mark_Ghost_Pragma
     (N  : Node_Id;
      Id : Entity_Id)
   is
   begin
      --  A pragma becomes Ghost when it encloses a Ghost entity or relates to
      --  a Ghost entity.

      if Is_Checked_Ghost_Entity (Id) then
         Mark_Ghost_Pragma (N, Check);

      elsif Is_Ignored_Ghost_Entity (Id) then
         Mark_Ghost_Pragma (N, Ignore);
      end if;
   end Mark_Ghost_Pragma;

   procedure Mark_Ghost_Pragma
     (N    : Node_Id;
      Mode : Ghost_Mode_Type)
   is
   begin
      if Mode = Check then
         Set_Is_Checked_Ghost_Pragma (N);

      else
         Set_Is_Ignored_Ghost_Pragma (N);
         Set_Is_Ignored_Ghost_Node (N);
         Record_Ignored_Ghost_Node (N);
      end if;
   end Mark_Ghost_Pragma;

   -------------------------
   -- Mark_Ghost_Renaming --
   -------------------------

   procedure Mark_Ghost_Renaming
     (N  : Node_Id;
      Id : Entity_Id)
   is
      Policy : Name_Id := No_Name;

   begin
      --  A renaming becomes Ghost when it renames a Ghost entity

      if Is_Checked_Ghost_Entity (Id) then
         Policy := Name_Check;

      elsif Is_Ignored_Ghost_Entity (Id) then
         Policy := Name_Ignore;
      end if;

      Mark_Ghost_Declaration_Or_Body (N, Policy);
   end Mark_Ghost_Renaming;

   ------------------------
   -- Name_To_Ghost_Mode --
   ------------------------

   function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is
   begin
      if Mode = Name_Check then
         return Check;

      elsif Mode = Name_Ignore then
         return Ignore;

      --  Otherwise the mode must denote one of the following:
      --
      --    * Disable indicates that the Ghost policy in effect is Disable
      --
      --    * None or No_Name indicates that the associated construct is not
      --      subject to any Ghost annotation.

      else
         pragma Assert (Mode in Name_Disable | Name_None | No_Name);
         return None;
      end if;
   end Name_To_Ghost_Mode;

   -------------------------------
   -- Record_Ignored_Ghost_Node --
   -------------------------------

   procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id) is
   begin
      --  Save all "top level" ignored Ghost nodes which can be safely replaced
      --  with a null statement. Note that there is need to save other kinds of
      --  nodes because those will always be enclosed by some top level ignored
      --  Ghost node.

      if Is_Body (N)
        or else Is_Declaration (N)
        or else Nkind (N) in N_Generic_Instantiation
                           | N_Push_Pop_xxx_Label
                           | N_Raise_xxx_Error
                           | N_Representation_Clause
                           | N_Statement_Other_Than_Procedure_Call
                           | N_Call_Marker
                           | N_Freeze_Entity
                           | N_Freeze_Generic_Entity
                           | N_Itype_Reference
                           | N_Pragma
                           | N_Procedure_Call_Statement
                           | N_Use_Package_Clause
                           | N_Use_Type_Clause
                           | N_Variable_Reference_Marker
                           | N_With_Clause
      then
         --  Only ignored Ghost nodes must be recorded in the table

         pragma Assert (Is_Ignored_Ghost_Node (N));
         Ignored_Ghost_Nodes.Append (N);
      end if;
   end Record_Ignored_Ghost_Node;

   -------------------------------
   -- Remove_Ignored_Ghost_Code --
   -------------------------------

   procedure Remove_Ignored_Ghost_Code is
      procedure Remove_Ignored_Ghost_Node (N : Node_Id);
      --  Eliminate ignored Ghost node N from the tree

      -------------------------------
      -- Remove_Ignored_Ghost_Node --
      -------------------------------

      procedure Remove_Ignored_Ghost_Node (N : Node_Id) is
      begin
         --  The generation and processing of ignored Ghost nodes may cause the
         --  same node to be saved multiple times. Reducing the number of saves
         --  to one involves costly solutions such as a hash table or the use
         --  of a flag shared by all nodes. To solve this problem, the removal
         --  machinery allows for multiple saves, but does not eliminate a node
         --  which has already been eliminated.

         if Nkind (N) = N_Null_Statement then
            null;

         --  Otherwise the ignored Ghost node must be eliminated

         else
            --  Only ignored Ghost nodes must be eliminated from the tree

            pragma Assert (Is_Ignored_Ghost_Node (N));

            --  Eliminate the node by rewriting it into null. Another option
            --  is to remove it from the tree, however multiple corner cases
            --  emerge which have be dealt individually.

            Rewrite (N, Make_Null_Statement (Sloc (N)));

            --  Eliminate any aspects hanging off the ignored Ghost node

            Remove_Aspects (N);
         end if;
      end Remove_Ignored_Ghost_Node;

   --  Start of processing for Remove_Ignored_Ghost_Code

   begin
      for Index in Ignored_Ghost_Nodes.First .. Ignored_Ghost_Nodes.Last loop
         Remove_Ignored_Ghost_Node (Ignored_Ghost_Nodes.Table (Index));
      end loop;
   end Remove_Ignored_Ghost_Code;

   --------------------------
   -- Restore_Ghost_Region --
   --------------------------

   procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
   begin
      Ghost_Mode           := Mode;
      Ignored_Ghost_Region := N;
   end Restore_Ghost_Region;

   --------------------
   -- Set_Ghost_Mode --
   --------------------

   procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is
      procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
      --  Install the Ghost mode of entity Id

      --------------------------------
      -- Set_Ghost_Mode_From_Entity --
      --------------------------------

      procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
      begin
         if Is_Checked_Ghost_Entity (Id) then
            Install_Ghost_Mode (Check);
         elsif Is_Ignored_Ghost_Entity (Id) then
            Install_Ghost_Mode (Ignore);
         else
            Install_Ghost_Mode (None);
         end if;
      end Set_Ghost_Mode_From_Entity;

      --  Local variables

      Id : Entity_Id;

   --  Start of processing for Set_Ghost_Mode

   begin
      --  The Ghost mode of an assignment statement depends on the Ghost mode
      --  of the target.

      if Nkind (N) = N_Assignment_Statement then
         Id := Ghost_Entity (Name (N));

         if Present (Id) then
            Set_Ghost_Mode_From_Entity (Id);
         end if;

      --  The Ghost mode of a body or a declaration depends on the Ghost mode
      --  of its defining entity.

      elsif Is_Body (N) or else Is_Declaration (N) then
         Set_Ghost_Mode_From_Entity (Defining_Entity (N));

      --  The Ghost mode of an entity depends on the entity itself

      elsif Nkind (N) in N_Entity then
         Set_Ghost_Mode_From_Entity (N);

      --  The Ghost mode of a [generic] freeze node depends on the Ghost mode
      --  of the entity being frozen.

      elsif Nkind (N) in N_Freeze_Entity | N_Freeze_Generic_Entity then
         Set_Ghost_Mode_From_Entity (Entity (N));

      --  The Ghost mode of a pragma depends on the associated entity. The
      --  property is encoded in the pragma itself.

      elsif Nkind (N) = N_Pragma then
         if Is_Checked_Ghost_Pragma (N) then
            Install_Ghost_Mode (Check);
         elsif Is_Ignored_Ghost_Pragma (N) then
            Install_Ghost_Mode (Ignore);
         else
            Install_Ghost_Mode (None);
         end if;

      --  The Ghost mode of a procedure call depends on the Ghost mode of the
      --  procedure being invoked.

      elsif Nkind (N) = N_Procedure_Call_Statement then
         Id := Ghost_Entity (Name (N));

         if Present (Id) then
            Set_Ghost_Mode_From_Entity (Id);
         end if;
      end if;
   end Set_Ghost_Mode;

   -------------------------
   -- Set_Is_Ghost_Entity --
   -------------------------

   procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
      Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
   begin
      if Policy = Name_Check then
         Set_Is_Checked_Ghost_Entity (Id);
      elsif Policy = Name_Ignore then
         Set_Is_Ignored_Ghost_Entity (Id);
      end if;
   end Set_Is_Ghost_Entity;

   ----------------------
   -- Whole_Object_Ref --
   ----------------------

   function Whole_Object_Ref (Ref : Node_Id) return Node_Id is
   begin
      if Nkind (Ref) in N_Indexed_Component | N_Slice
        or else (Nkind (Ref) = N_Selected_Component
                   and then Is_Object_Reference (Prefix (Ref)))
      then
         if Is_Access_Type (Etype (Prefix (Ref))) then
            return Ref;
         else
            return Whole_Object_Ref (Prefix (Ref));
         end if;
      else
         return Ref;
      end if;
   end Whole_Object_Ref;

end Ghost;