2015-01-07 Hristian Kirtchev <kirtchev@adacore.com>

	* alloc.ads Alphabetize several declarations. Add constants
	Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment.
	* atree.adb Add with and use clauses for Opt.
	(Allocate_Initialize_Node): Mark a node as ignored Ghost
	if it is created in an ignored Ghost region.
	(Ekind_In): New variant.
	(Is_Ignored_Ghost_Node): New routine.
	(Set_Is_Ignored_Ghost_Node): New routine.
	* atree.adb Aplhabetize several subprograms declarations. Flag
	Spare0 is now known as Is_Ignored_Ghost_Node.
	(Ekind_In): New variant.
	(Is_Ignored_Ghost_Node): New routine.
	(Set_Is_Ignored_Ghost_Node): New routine.
	* einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code.
	(Contains_Ignored_Ghost_Code): New routine.
	(Set_Contains_Ignored_Ghost_Code): New routine.
	(Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity):
	It is now possible to set this property on an unanalyzed entity.
	(Write_Entity_Flags): Output the status of flag
	Contains_Ignored_Ghost_Code.
	* einfo.ads New attribute Contains_Ignored_Ghost_Code along with
	usage in nodes.
	(Contains_Ignored_Ghost_Code): New routine
	along with pragma Inline.
	(Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline.
	* exp_ch3.adb Add with and use clauses for Ghost.
	(Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit.
	Set the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* exp_ch7.adb (Process_Declarations): Do not process a context
	that invoves an ignored Ghost entity.
	* exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost
	construct that has been rewritten as a null statement.
	* exp_disp.adb Add with and use clauses for Ghost.
	(Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set
	the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity
	does not require any clean up. Add two missing cases that deal
	with block statements.
	* freeze.adb Add with and use clauses for Ghost.
	(Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit.
	Set the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* frontend.adb Add with and use clauses for Ghost. Remove any
	ignored Ghost code from all units that qualify.
	* ghost.adb New unit.
	* ghost.ads New unit.
	* gnat1drv.adb Add with clause for Ghost. Initialize and lock
	the table in package Ghost.
	* lib.ads: Alphabetize several subprogram declarations.
	* lib-xref.adb (Output_References): Do not generate reference
	information for ignored Ghost entities.
	* opt.ads Add new type Ghost_Mode_Type and new global variable
	Ghost_Mode.
	* rtsfind.adb (Load_RTU): Provide a clean environment when
	loading a runtime unit.
	* sem.adb (Analyze): Capture/restore the value of Ghost_Mode on
	entry/exit as the node may set a different mode.
	(Do_Analyze):
	Capture/restore the value of Ghost_Mode on entry/exit as the
	unit may be withed from a unit with a different Ghost mode.
	* sem_ch3.adb Add with and use clauses for Ghost.
	(Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl,
	Analyze_Number_Declaration, Analyze_Private_Extension_Declaration,
	Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark
	the entity as Ghost when there is a Ghost_Mode in effect.
	(Array_Type_Declaration): The implicit base type inherits the
	"ghostness" from the array type.
	(Derive_Subprogram): The
	alias inherits the "ghostness" from the parent subprogram.
	(Make_Implicit_Base): The implicit base type inherits the
	"ghostness" from the parent type.
	* sem_ch5.adb Add with and use clauses for Ghost.
	(Analyze_Assignment): Set the Ghost_Mode in effect.
	* sem_ch6.adb Add with and use clauses for Ghost.
	(Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call,
	Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration):
	Set the Ghost_Mode in effect. Mark the entity as Ghost when
	there is a Ghost_Mode in effect.
	* sem_ch7.adb Add with and use clauses for Ghost.
	(Analyze_Package_Body_Helper, Analyze_Package_Declaration,
	Analyze_Private_Type_Declaration): Set the Ghost_Mode in
	effect. Mark the entity as Ghost when there is a Ghost_Mode
	in effect.
	* sem_ch8.adb Add with and use clauses for Ghost.
	(Analyze_Exception_Renaming, Analyze_Generic_Renaming,
	Analyze_Object_Renaming, Analyze_Package_Renaming,
	Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark
	the entity as Ghost when there is a Ghost_Mode in effect.
	(Find_Type): Check the Ghost context of a type.
	* sem_ch11.adb Add with and use clauses for Ghost.
	(Analyze_Exception_Declaration): Set the Ghost_Mode in
	effect. Mark the entity as Ghost when there is a Ghost_Mode
	in effect.
	* sem_ch12.adb Add with and use clauses for Ghost.
	(Analyze_Generic_Package_Declaration,
	Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect.
	Mark the entity as Ghost when there is a Ghost_Mode in effect.
	* sem_prag.adb Add with and use clauses for Ghost.
	(Analyze_Pragma): Ghost-related checks are triggered when there
	is a Ghost mode in effect.
	(Create_Abstract_State): Mark the
	entity as Ghost when there is a Ghost_Mode in effect.
	* sem_res.adb Add with and use clauses for Ghost.
	(Check_Ghost_Context): Removed.
	* sem_util.adb (Check_Ghost_Completion): Removed.
	(Check_Ghost_Derivation): Removed.
	(Incomplete_Or_Partial_View):
	Add a guard in case the entity has not been analyzed yet
	and does carry a scope.
	(Is_Declaration): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Statement_Or_Pragma):
	Removed.
	(Is_Subject_To_Ghost): Removed.
	(Set_Is_Ghost_Entity):
	Removed.
	(Within_Ghost_Scope): Removed.
	* sem_util.adb (Check_Ghost_Completion): Removed.
	(Check_Ghost_Derivation): Removed.
	(Is_Declaration): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_Subject_To_Ghost): Removed.
	(Set_Is_Ghost_Entity): Removed.
	(Within_Ghost_Scope): Removed.
	* sinfo.ads Add a section on Ghost mode.
	* treepr.adb (Print_Header_Flag): New routine.
	(Print_Node_Header): Factor out code. Output flag
	Is_Ignored_Ghost_Node.
	* gcc-interface/Make-lang.in: Add dependency for unit Ghost.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@219280 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 949 insertions, 0 deletions

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
new file mode 100644
index 00000000000..b69c74ee68f
--- /dev/null
+++ b/gcc/ada/ghost.adb
@@ -0,0 +1,949 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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
+         --  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
+               Ref := N;
+
+               --  When the reference extracts a subcomponent, recover the
+               --  related object (SPARK RM 6.9(1)).
+
+               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
+         Nam := Name (N);
+
+         --  When the reference extracts a subcomponent, recover the related
+         --  object (SPARK RM 6.9(1)).
+
+         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;