path: root/gcc/ada/ghost.adb

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                                G H O S T                                 --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--            Copyright (C) 2014-2015, 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;    use Alloc;
with Aspects;  use Aspects;
with Atree;    use Atree;
with Einfo;    use Einfo;
with Elists;   use Elists;
with Errout;   use Errout;
with Lib;      use Lib;
with Namet;    use Namet;
with Nlists;   use Nlists;
with Nmake;    use Nmake;
with Opt;      use Opt;
with Sem;      use Sem;
with Sem_Aux;  use Sem_Aux;
with Sem_Eval; use Sem_Eval;
with Sem_Res;  use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo;    use Sinfo;
with Snames;   use Snames;
with Table;

package body Ghost is

   --  The following table contains the N_Compilation_Unit node for a unit that
   --  is either subject to pragma Ghost with policy Ignore or contains ignored
   --  Ghost code. The table is used in the removal of ignored Ghost code from
   --  units.

   package Ignored_Ghost_Units is new Table.Table (
     Table_Component_Type => Node_Id,
     Table_Index_Type     => Int,
     Table_Low_Bound      => 0,
     Table_Initial        => Alloc.Ignored_Ghost_Units_Initial,
     Table_Increment      => Alloc.Ignored_Ghost_Units_Increment,
     Table_Name           => "Ignored_Ghost_Units");

   -----------------------
   -- Local Subprograms --
   -----------------------

   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.

   ----------------------------
   -- Add_Ignored_Ghost_Unit --
   ----------------------------

   procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
   begin
      pragma Assert (Nkind (Unit) = N_Compilation_Unit);

      --  Avoid duplicates in the table as pruning the same unit more than once
      --  is wasteful. Since ignored Ghost code tends to be grouped up, check
      --  the contents of the table in reverse.

      for Index in reverse Ignored_Ghost_Units.First ..
                           Ignored_Ghost_Units.Last
      loop
         --  If the unit is already present in the table, do not add it again

         if Unit = Ignored_Ghost_Units.Table (Index) then
            return;
         end if;
      end loop;

      --  If we get here, then this is the first time the unit is being added

      Ignored_Ghost_Units.Append (Unit);
   end Add_Ignored_Ghost_Unit;

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

   procedure Check_Ghost_Completion
     (Partial_View : Entity_Id;
      Full_View    : Entity_Id)
   is
      Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);

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

      if Is_Checked_Ghost_Entity (Partial_View)
        and then Policy = Name_Ignore
      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);

      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);
      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; Err_N : Node_Id);
      --  Verify that the Ghost policy at the point of declaration of entity Id
      --  matches the policy at the point of reference. If this is not the case
      --  emit an error at Err_N.

      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.

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

      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;
            Subp_Decl : Node_Id;
            Subp_Id   : Entity_Id;

         begin
            --  Climb the parent chain looking for an object declaration

            Par := Decl;
            while Present (Par) loop
               if Is_Declaration (Par) then

                  --  A declaration is Ghost when it appears within a Ghost
                  --  package or subprogram.

                  if Ghost_Mode > None then
                     return True;

                  --  Otherwise the declaration may not have been analyzed yet,
                  --  determine whether it is subject to aspect/pragma Ghost.

                  else
                     return Is_Subject_To_Ghost (Par);
                  end if;

               --  Special cases

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

               elsif Nkind (Par) = N_Parameter_Specification
                 and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
               then
                  return True;

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

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

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

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

                  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;

            return False;
         end Is_Ghost_Declaration;

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

            -------------------------------
            -- Is_Ghost_Entity_Reference --
            -------------------------------

            function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean 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;

               return
                 Is_Entity_Name (Ref)
                   and then Present (Entity (Ref))
                   and then Is_Ghost_Entity (Entity (Ref));
            end Is_Ghost_Entity_Reference;

            --  Local variables

            Arg  : Node_Id;
            Stmt : Node_Id;

         --  Start of processing for Is_Ghost_Statement_Or_Pragma

         begin
            if Nkind (N) = N_Pragma then

               --  A pragma is Ghost when it appears within a Ghost package or
               --  subprogram.

               if Ghost_Mode > None then
                  return True;
               end if;

               --  A pragma is Ghost when it mentions a Ghost entity

               Arg := First (Pragma_Argument_Associations (N));
               while Present (Arg) loop
                  if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
                     return True;
                  end if;

                  Next (Arg);
               end loop;
            end if;

            Stmt := N;
            while Present (Stmt) loop
               if Is_Statement (Stmt) then

                  --  A statement is Ghost when it appears within a Ghost
                  --  package or subprogram.

                  if Ghost_Mode > None then
                     return True;

                  --  An assignment statement or a procedure call is Ghost when
                  --  the name denotes a Ghost entity.

                  elsif Nkind_In (Stmt, N_Assignment_Statement,
                                        N_Procedure_Call_Statement)
                  then
                     return Is_Ghost_Entity_Reference (Name (Stmt));
                  end if;

               --  Prevent the search from going too far

               elsif Is_Body_Or_Package_Declaration (Stmt) then
                  return False;
               end if;

               Stmt := Parent (Stmt);
            end loop;

            return False;
         end Is_Ghost_Statement_Or_Pragma;

      --  Start of processing for Is_OK_Ghost_Context

      begin
         --  The Ghost entity appears within an assertion expression

         if In_Assertion_Expr > 0 then
            return True;

         --  The Ghost entity is part of a declaration or its completion

         elsif Is_Ghost_Declaration (Context) then
            return True;

         --  The Ghost entity is referenced within a Ghost statement

         elsif Is_Ghost_Statement_Or_Pragma (Context) 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;

         else
            return False;
         end if;
      end Is_OK_Ghost_Context;

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

      procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : 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(14)).

         if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
            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);

         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);
         end if;
      end Check_Ghost_Policy;

   --  Start of processing for Check_Ghost_Context

   begin
      --  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
         Check_Ghost_Policy (Ghost_Id, Ghost_Ref);

      --  Otherwise the Ghost entity appears in a non-Ghost context and affects
      --  its behavior or value.

      else
         Error_Msg_N
           ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
            Ghost_Ref);
      end if;
   end Check_Ghost_Context;

   ----------------------------
   -- Check_Ghost_Derivation --
   ----------------------------

   procedure Check_Ghost_Derivation (Typ : Entity_Id) is
      Parent_Typ : constant Entity_Id := Etype (Typ);
      Iface      : Entity_Id;
      Iface_Elmt : Elmt_Id;

   begin
      --  Allow untagged derivations from predefined types such as Integer as
      --  those are not Ghost by definition.

      if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
         null;

      --  The parent type of a Ghost type extension must be Ghost

      elsif not Is_Ghost_Entity (Parent_Typ) then
         Error_Msg_N  ("type extension & cannot be ghost", Typ);
         Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
         return;
      end if;

      --  All progenitors (if any) must be Ghost as well

      if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
         Iface_Elmt := First_Elmt (Interfaces (Typ));
         while Present (Iface_Elmt) loop
            Iface := Node (Iface_Elmt);

            if not Is_Ghost_Entity (Iface) then
               Error_Msg_N  ("type extension & cannot be ghost", Typ);
               Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
               return;
            end if;

            Next_Elmt (Iface_Elmt);
         end loop;
      end if;
   end Check_Ghost_Derivation;

   --------------------------------
   -- 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_Units.Init;
   end Initialize;

   ---------------------
   -- Is_Ghost_Entity --
   ---------------------

   function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
   begin
      return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
   end Is_Ghost_Entity;

   -------------------------
   -- 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 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_In (N, 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_In (N, 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.

         elsif Comes_From_Source (Decl) then
            exit;
         end if;

         Next (Decl);
      end loop;

      return False;
   end Is_Subject_To_Ghost;

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

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

   ----------------------------------
   -- Propagate_Ignored_Ghost_Code --
   ----------------------------------

   procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
      Nod  : Node_Id;
      Scop : Entity_Id;

   begin
      --  Traverse the parent chain looking for blocks, packages and
      --  subprograms or their respective bodies.

      Nod := Parent (N);
      while Present (Nod) loop
         Scop := Empty;

         if Nkind (Nod) = N_Block_Statement then
            Scop := Entity (Identifier (Nod));

         elsif Nkind_In (Nod, N_Package_Body,
                              N_Package_Declaration,
                              N_Subprogram_Body,
                              N_Subprogram_Declaration)
         then
            Scop := Defining_Entity (Nod);
         end if;

         --  The current node denotes a scoping construct

         if Present (Scop) then

            --  Stop the traversal when the scope already contains ignored
            --  Ghost code as all enclosing scopes have already been marked.

            if Contains_Ignored_Ghost_Code (Scop) then
               exit;

            --  Otherwise mark this scope and keep climbing

            else
               Set_Contains_Ignored_Ghost_Code (Scop);
            end if;
         end if;

         Nod := Parent (Nod);
      end loop;

      --  The unit containing the ignored Ghost code must be post processed
      --  before invoking the back end.

      Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
   end Propagate_Ignored_Ghost_Code;

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

   procedure Remove_Ignored_Ghost_Code is
      procedure Prune_Tree (Root : Node_Id);
      --  Remove all code marked as ignored Ghost from the tree of denoted by
      --  Root.

      ----------------
      -- Prune_Tree --
      ----------------

      procedure Prune_Tree (Root : Node_Id) is
         procedure Prune (N : Node_Id);
         --  Remove a given node from the tree by rewriting it into null

         function Prune_Node (N : Node_Id) return Traverse_Result;
         --  Determine whether node N denotes an ignored Ghost construct. If
         --  this is the case, rewrite N as a null statement. See the body for
         --  special cases.

         -----------
         -- Prune --
         -----------

         procedure Prune (N : Node_Id) is
         begin
            --  Destroy any aspects that may be associated with the node

            if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
               Remove_Aspects (N);
            end if;

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

         ----------------
         -- Prune_Node --
         ----------------

         function Prune_Node (N : Node_Id) return Traverse_Result is
            Id : Entity_Id;

         begin
            --  The node is either declared as ignored Ghost or is a byproduct
            --  of expansion. Destroy it and stop the traversal on this branch.

            if Is_Ignored_Ghost_Node (N) then
               Prune (N);
               return Skip;

            --  Scoping constructs such as blocks, packages, subprograms and
            --  bodies offer some flexibility with respect to pruning.

            elsif Nkind_In (N, N_Block_Statement,
                               N_Package_Body,
                               N_Package_Declaration,
                               N_Subprogram_Body,
                               N_Subprogram_Declaration)
            then
               if Nkind (N) = N_Block_Statement then
                  Id := Entity (Identifier (N));
               else
                  Id := Defining_Entity (N);
               end if;

               --  The scoping construct contains both living and ignored Ghost
               --  code, let the traversal prune all relevant nodes.

               if Contains_Ignored_Ghost_Code (Id) then
                  return OK;

               --  Otherwise the construct contains only living code and should
               --  not be pruned.

               else
                  return Skip;
               end if;

            --  Otherwise keep searching for ignored Ghost nodes

            else
               return OK;
            end if;
         end Prune_Node;

         procedure Prune_Nodes is new Traverse_Proc (Prune_Node);

      --  Start of processing for Prune_Tree

      begin
         Prune_Nodes (Root);
      end Prune_Tree;

   --  Start of processing for Remove_Ignored_Ghost_Code

   begin
      for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
         Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
      end loop;
   end Remove_Ignored_Ghost_Code;

   --------------------
   -- 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);
      --  Set the value of global variable Ghost_Mode depending on the mode of
      --  entity Id.

      procedure Set_Ghost_Mode_From_Policy;
      --  Set the value of global variable Ghost_Mode depending on the current
      --  Ghost policy in effect.

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

      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;

            Set_Is_Ignored_Ghost_Node (N);
            Propagate_Ignored_Ghost_Code (N);
         end if;
      end Set_Ghost_Mode_From_Entity;

      --------------------------------
      -- Set_Ghost_Mode_From_Policy --
      --------------------------------

      procedure Set_Ghost_Mode_From_Policy is
         Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);

      begin
         if Policy = Name_Check then
            Ghost_Mode := Check;

         elsif Policy = Name_Ignore then
            Ghost_Mode := Ignore;

            Set_Is_Ignored_Ghost_Node (N);
            Propagate_Ignored_Ghost_Code (N);
         end if;
      end Set_Ghost_Mode_From_Policy;

      --  Local variables

      Nam : Node_Id;

   --  Start of processing for Set_Ghost_Mode

   begin
      --  The input node denotes one of the many declaration kinds that may be
      --  subject to pragma Ghost.

      if Is_Declaration (N) then
         if Is_Subject_To_Ghost (N) then
            Set_Ghost_Mode_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)
         then
            Set_Ghost_Mode_From_Entity (Prev_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)
         then
            Set_Ghost_Mode_From_Entity (Prev_Id);
         end if;

      --  The input denotes an assignment or a procedure call. In this case
      --  the Ghost mode is dictated by the name of the construct.

      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;

         if Is_Entity_Name (Nam)
           and then Present (Entity (Nam))
         then
            Set_Ghost_Mode_From_Entity (Entity (Nam));
         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))
           or else Is_Subject_To_Ghost (N)
         then
            Set_Ghost_Mode_From_Policy;
         end if;
      end if;
   end Set_Ghost_Mode;

   -------------------------------
   -- Set_Ghost_Mode_For_Freeze --
   -------------------------------

   procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_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;

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

end Ghost;