[Ada] Support ghost generic formal parameters

This adds support in GNAT for ghost generic formal parameters, as
included in SPARK RM 6.9.

gcc/ada/

	* ghost.adb (Check_Ghost_Context): Delay checking for generic
	associations.
	(Check_Ghost_Context_In_Generic_Association): Perform ghost
	checking in analyzed generic associations.
	(Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM
	6.9(13-14) for formal procedures and packages.
	(Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for
	variables.
	* ghost.ads: Declarations for the above.
	* sem_ch12.adb (Analyze_Associations): Apply delayed checking
	for generic associations.
	(Analyze_Formal_Object_Declaration): Same.
	(Analyze_Formal_Subprogram_Declaration): Same.
	(Instantiate_Formal_Package): Same.
	(Instantiate_Formal_Subprogram): Same.
	(Instantiate_Object): Same.  Copy ghost aspect to newly declared
	object for actual for IN formal object. Use new function
	Get_Enclosing_Deep_Object to retrieve root object.
	(Instantiate_Type): Copy ghost aspect to declared subtype for
	actual for formal type.
	* sem_prag.adb (Analyze_Pragma): Recognize new allowed
	declarations.
	* sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect
	between nodes.
	(Get_Enclosing_Deep_Object): New function to return enclosing
	deep object (or root for reachable part).
	* sem_util.ads (Copy_Ghost_Aspect): Same.
	(Get_Enclosing_Deep_Object): Same.
	* libgnat/s-imageu.ads: Declare formal subprograms as ghost.
	* libgnat/s-valuei.ads: Same.
	* libgnat/s-valuti.ads: Same.

9 files changed, 347 insertions, 63 deletions

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 8f23cbd..1ce1d6a 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -472,6 +472,13 @@ package body Ghost is
                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
@@ -521,19 +528,6 @@ package body Ghost is
                then
                   return True;
 
-               --  In the context of an instantiation, accept currently Ghost
-               --  arguments for formal subprograms, as SPARK does not provide
-               --  a way to distinguish Ghost formal parameters from non-Ghost
-               --  ones. Illegal use of such arguments in a non-Ghost context
-               --  will lead to errors inside the instantiation.
-
-               elsif Nkind (Parent (Par)) = N_Generic_Association
-                 and then (Nkind (Par) in N_Has_Entity
-                            and then Present (Entity (Par))
-                            and then Is_Subprogram (Entity (Par)))
-               then
-                  return True;
-
                elsif Is_OK_Declaration (Par) then
                   return True;
 
@@ -680,6 +674,128 @@ package body Ghost is
       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 --
    ----------------------------
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 21126a7..ca311bf 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -44,6 +44,33 @@ package Ghost is
    --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
    --  where Ghost entity Ghost_Id can safely reside.
 
+   procedure Check_Ghost_Context_In_Generic_Association
+     (Actual : Node_Id;
+      Formal : Entity_Id);
+   --  Check that if Actual contains references to ghost entities, generic
+   --  formal parameter Formal is ghost (SPARK RM 6.9(10)).
+
+   procedure Check_Ghost_Formal_Procedure_Or_Package
+     (N          : Node_Id;
+      Actual     : Entity_Id;
+      Formal     : Entity_Id;
+      Is_Default : Boolean := False);
+   --  Verify that if generic formal procedure (resp. package) Formal is ghost,
+   --  then Actual is not Empty and also a ghost procedure (resp. package)
+   --  (SPARK RM 6.9(13-14)). The error if any is located on N. If
+   --  Is_Default is False, N and Actual represent the actual parameter in an
+   --  instantiation. Otherwise, they represent the default subprogram of a
+   --  formal subprogram declaration.
+
+   procedure Check_Ghost_Formal_Variable
+     (Actual     : Node_Id;
+      Formal     : Entity_Id;
+      Is_Default : Boolean := False);
+   --  Verify that if Formal (either an IN OUT generic formal parameter, or an
+   --  IN generic formal parameter of access-to-variable type) is ghost, then
+   --  Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
+   --  Actual is the default expression of the formal object declaration.
+
    procedure Check_Ghost_Overriding
      (Subp            : Entity_Id;
       Overridden_Subp : Entity_Id);
diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index d3f2981..789cf65 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -54,27 +54,34 @@ generic
 
    Unsigned_Width_Ghost : Natural;
 
-   with function Wrap_Option (Value : Uns) return Uns_Option;
+   with function Wrap_Option (Value : Uns) return Uns_Option
+      with Ghost;
    with function Only_Decimal_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
-   with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+      return Boolean
+      with Ghost;
+   with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+      with Ghost;
    with function Scan_Based_Number_Ghost
      (Str      : String;
       From, To : Integer;
       Base     : Uns := 10;
-      Acc      : Uns := 0) return Uns_Option;
-   with function Is_Unsigned_Ghost (Str : String) return Boolean;
+      Acc      : Uns := 0) return Uns_Option
+      with Ghost;
+   with function Is_Unsigned_Ghost (Str : String) return Boolean
+      with Ghost;
    with function Value_Unsigned (Str : String) return Uns;
    with procedure Prove_Iter_Scan_Based_Number_Ghost
      (Str1, Str2 : String;
       From, To : Integer;
       Base     : Uns := 10;
-      Acc      : Uns := 0);
+      Acc      : Uns := 0)
+      with Ghost;
    with procedure Prove_Scan_Only_Decimal_Ghost
      (Str : String;
-      Val : Uns);
+      Val : Uns)
+      with Ghost;
 
 package System.Image_U is
 
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index c5b4b8e..5e42773 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -55,30 +55,37 @@ generic
    --  Additional parameters for ghost subprograms used inside contracts
 
    type Uns_Option is private;
-   with function Wrap_Option (Value : Uns) return Uns_Option;
-   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
+   with function Wrap_Option (Value : Uns) return Uns_Option
+      with Ghost;
+   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean
+      with Ghost;
    with function Raw_Unsigned_Overflows_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
+      return Boolean
+      with Ghost;
    with function Scan_Raw_Unsigned_Ghost
      (Str      : String;
       From, To : Integer)
-      return Uns;
+      return Uns
+      with Ghost;
    with function Raw_Unsigned_Last_Ghost
      (Str      : String;
       From, To : Integer)
-      return Positive;
+      return Positive
+      with Ghost;
    with function Only_Decimal_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
+      return Boolean
+      with Ghost;
    with function Scan_Based_Number_Ghost
      (Str      : String;
       From, To : Integer;
       Base     : Uns := 10;
       Acc      : Uns := 0)
-      return Uns_Option;
+      return Uns_Option
+      with Ghost;
 
 package System.Value_I is
    pragma Preelaborate;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 45a0b66..2b89b12 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -384,27 +384,36 @@ is
 
       Unsigned_Width_Ghost : Natural;
 
-      with function Wrap_Option (Value : Uns) return Uns_Option;
+      with function Wrap_Option (Value : Uns) return Uns_Option
+         with Ghost;
       with function Only_Decimal_Ghost
         (Str      : String;
          From, To : Integer)
-         return Boolean;
-      with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+         return Boolean
+         with Ghost;
+      with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+         with Ghost;
       with function Scan_Based_Number_Ghost
         (Str      : String;
          From, To : Integer;
          Base     : Uns := 10;
          Acc      : Uns := 0)
-         return Uns_Option;
-      with function Is_Integer_Ghost (Str : String) return Boolean;
+         return Uns_Option
+         with Ghost;
+      with function Is_Integer_Ghost (Str : String) return Boolean
+         with Ghost;
       with procedure Prove_Iter_Scan_Based_Number_Ghost
         (Str1, Str2 : String;
          From, To : Integer;
          Base     : Uns := 10;
-         Acc      : Uns := 0);
-      with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int);
-      with function Abs_Uns_Of_Int (Val : Int) return Uns;
-      with function Value_Integer (Str : String) return Int;
+         Acc      : Uns := 0)
+         with Ghost;
+      with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+         with Ghost;
+      with function Abs_Uns_Of_Int (Val : Int) return Uns
+         with Ghost;
+      with function Value_Integer (Str : String) return Int
+         with Ghost;
 
    package Int_Params is
    end Int_Params;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index dcc0dac..af8bbbe 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -2204,6 +2204,19 @@ package body Sem_Ch12 is
                   raise Program_Error;
             end case;
 
+            --  Check here the correct use of Ghost entities in generic
+            --  instantiations, as now the generic has been resolved and
+            --  we know which formal generic parameters are ghost (SPARK
+            --  RM 6.9(10)).
+
+            if Nkind (Formal) not in N_Use_Package_Clause
+                                   | N_Use_Type_Clause
+            then
+               Check_Ghost_Context_In_Generic_Association
+                 (Actual => Match,
+                  Formal => Defining_Entity (Analyzed_Formal));
+            end if;
+
             Formal := Saved_Formal;
             Next_Non_Pragma (Analyzed_Formal);
          end loop;
@@ -2715,6 +2728,17 @@ package body Sem_Ch12 is
          if Present (E) then
             Preanalyze_Spec_Expression (E, T);
 
+            --  The default for a ghost generic formal IN parameter of
+            --  access-to-variable type should be a ghost object (SPARK
+            --  RM 6.9(13)).
+
+            if Is_Access_Variable (T) then
+               Check_Ghost_Formal_Variable
+                 (Actual     => E,
+                  Formal     => Id,
+                  Is_Default => True);
+            end if;
+
             if Is_Limited_Type (T) and then not OK_For_Limited_Init (T, E) then
                Error_Msg_N
                  ("initialization not allowed for limited types", E);
@@ -3398,6 +3422,25 @@ package body Sem_Ch12 is
             goto Leave;
          end if;
 
+         --  The default for a ghost generic formal procedure should be a ghost
+         --  procedure (SPARK RM 6.9(13)).
+
+         if Ekind (Nam) = E_Procedure then
+            declare
+               Def_E : Entity_Id := Empty;
+            begin
+               if Nkind (Def) in N_Has_Entity then
+                  Def_E := Entity (Def);
+               end if;
+
+               Check_Ghost_Formal_Procedure_Or_Package
+                 (N          => Def,
+                  Actual     => Def_E,
+                  Formal     => Nam,
+                  Is_Default => True);
+            end;
+         end if;
+
          --  Default name may be overloaded, in which case the interpretation
          --  with the correct profile must be selected, as for a renaming.
          --  If the definition is an indexed component, it must denote a
@@ -10594,6 +10637,14 @@ package body Sem_Ch12 is
          Gen_Parent := Generic_Parent (Specification (Analyzed_Formal));
          Formal_Pack := Defining_Unit_Name (Specification (Analyzed_Formal));
 
+         --  The actual for a ghost generic formal package should be a ghost
+         --  package (SPARK RM 6.9(14)).
+
+         Check_Ghost_Formal_Procedure_Or_Package
+           (N      => Actual,
+            Actual => Actual_Pack,
+            Formal => Formal_Pack);
+
          if Nkind (Parent (Actual_Pack)) = N_Defining_Program_Unit_Name then
             Parent_Spec := Package_Specification (Actual_Pack);
          else
@@ -10881,6 +10932,18 @@ package body Sem_Ch12 is
             Act_E := Empty;
          end if;
 
+         --  The actual for a ghost generic formal procedure should be a ghost
+         --  procedure (SPARK RM 6.9(14)).
+
+         if Present (Act_E)
+           and then Ekind (Act_E) = E_Procedure
+         then
+            Check_Ghost_Formal_Procedure_Or_Package
+              (N      => Act,
+               Actual => Act_E,
+               Formal => Analyzed_S);
+         end if;
+
          if (Present (Act_E) and then Is_Overloadable (Act_E))
            or else Nkind (Act) in N_Attribute_Reference
                                 | N_Indexed_Component
@@ -11400,40 +11463,22 @@ package body Sem_Ch12 is
          --  volatility refinement aspects.
 
          declare
-            Actual_Obj : Entity_Id;
-            N          : Node_Id := Actual;
+            Actual_Obj : constant Entity_Id :=
+              Get_Enclosing_Deep_Object (Actual);
          begin
-            --  Similar to Sem_Util.Get_Enclosing_Object, but treat
-            --  pointer dereference like component selection.
-            loop
-               if Is_Entity_Name (N) then
-                  Actual_Obj := Entity (N);
-                  exit;
-               end if;
-
-               case Nkind (N) is
-                  when N_Indexed_Component
-                     | N_Selected_Component
-                     | N_Slice
-                     | N_Explicit_Dereference
-                  =>
-                     N := Prefix (N);
-
-                  when N_Type_Conversion =>
-                     N := Expression (N);
-
-                  when others =>
-                     Actual_Obj := Etype (N);
-                     exit;
-               end case;
-            end loop;
-
             Check_Volatility_Compatibility
               (Actual_Obj, A_Gen_Obj, "actual object",
                "its corresponding formal object of mode in out",
                Srcpos_Bearer => Actual);
          end;
 
+         --  The actual for a ghost generic formal IN OUT parameter should be a
+         --  ghost object (SPARK RM 6.9(14)).
+
+         Check_Ghost_Formal_Variable
+           (Actual => Actual,
+            Formal => A_Gen_Obj);
+
       --  Formal in-parameter
 
       else
@@ -11459,6 +11504,7 @@ package body Sem_Ch12 is
                 Object_Definition      => Def,
                 Expression             => Actual);
 
+            Copy_Ghost_Aspect (Formal, To => Decl_Node);
             Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc);
 
             --  A generic formal object of a tagged type is defined to be
@@ -11470,6 +11516,16 @@ package body Sem_Ch12 is
 
             Append (Decl_Node, List);
 
+            --  The actual for a ghost generic formal IN parameter of
+            --  access-to-variable type should be a ghost object (SPARK
+            --  RM 6.9(14)).
+
+            if Is_Access_Variable (Etype (A_Gen_Obj)) then
+               Check_Ghost_Formal_Variable
+                 (Actual => Actual,
+                  Formal => A_Gen_Obj);
+            end if;
+
             --  No need to repeat (pre-)analysis of some expression nodes
             --  already handled in Preanalyze_Actuals.
 
@@ -11543,6 +11599,7 @@ package body Sem_Ch12 is
                 Expression             => New_Copy_Tree
                                             (Default_Expression (Formal)));
 
+            Copy_Ghost_Aspect (Formal, To => Decl_Node);
             Set_Corresponding_Generic_Association
               (Decl_Node, Expression (Decl_Node));
 
@@ -14199,6 +14256,8 @@ package body Sem_Ch12 is
           Defining_Identifier => Subt,
           Subtype_Indication  => New_Occurrence_Of (Act_T, Loc));
 
+      Copy_Ghost_Aspect (Formal, To => Decl_Node);
+
       --  Record whether the actual is private at this point, so that
       --  Check_Generic_Actuals can restore its proper view before the
       --  semantic analysis of the instance.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9ebac41..ad43808 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -17002,6 +17002,9 @@ package body Sem_Prag is
                --  The pragma applies to a legal construct, stop the traversal
 
                elsif Nkind (Stmt) in N_Abstract_Subprogram_Declaration
+                                   | N_Formal_Object_Declaration
+                                   | N_Formal_Subprogram_Declaration
+                                   | N_Formal_Type_Declaration
                                    | N_Full_Type_Declaration
                                    | N_Generic_Subprogram_Declaration
                                    | N_Object_Declaration
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index edb9482..942a77a 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7024,6 +7024,25 @@ package body Sem_Util is
       return Comps;
    end Copy_Component_List;
 
+   -----------------------
+   -- Copy_Ghost_Aspect --
+   -----------------------
+
+   procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id) is
+      pragma Assert (not Has_Aspects (To));
+      Asp : Node_Id;
+
+   begin
+      if Has_Aspects (From) then
+         Asp := Find_Aspect (Defining_Entity (From), Aspect_Ghost);
+
+         if Present (Asp) then
+            Set_Aspect_Specifications (To, New_List (New_Copy_Tree (Asp)));
+            Set_Has_Aspects (To, True);
+         end if;
+      end if;
+   end Copy_Ghost_Aspect;
+
    -------------------------
    -- Copy_Parameter_List --
    -------------------------
@@ -11004,6 +11023,32 @@ package body Sem_Util is
       end if;
    end Get_Enclosing_Object;
 
+   -------------------------------
+   -- Get_Enclosing_Deep_Object --
+   -------------------------------
+
+   function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id is
+   begin
+      if Is_Entity_Name (N) then
+         return Entity (N);
+      else
+         case Nkind (N) is
+            when N_Explicit_Dereference
+               | N_Indexed_Component
+               | N_Selected_Component
+               | N_Slice
+            =>
+               return Get_Enclosing_Deep_Object (Prefix (N));
+
+            when N_Type_Conversion =>
+               return Get_Enclosing_Deep_Object (Expression (N));
+
+            when others =>
+               return Empty;
+         end case;
+      end if;
+   end Get_Enclosing_Deep_Object;
+
    ---------------------------
    -- Get_Enum_Lit_From_Pos --
    ---------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index de7883c..a8afda0 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -625,6 +625,11 @@ package Sem_Util is
    --  create a new compatible record type. Loc is the source location assigned
    --  to the created nodes.
 
+   procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id);
+   --  Copy the Ghost aspect if present in the aspect specifications of node
+   --  From to node To. On entry it is assumed that To does not have aspect
+   --  specifications. If From has no aspects, the routine has no effect.
+
    function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
    --  Utility to create a parameter profile for a new subprogram spec, when
    --  the subprogram has a body that acts as spec. This is done for some cases
@@ -1183,6 +1188,12 @@ package Sem_Util is
    --  If expression N references a part of an object, return this object.
    --  Otherwise return Empty. Expression N should have been resolved already.
 
+   function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id;
+   --  If expression N references a reachable part of an object (as defined in
+   --  SPARK RM 6.9), return this object. Otherwise return Empty. It is similar
+   --  to Get_Enclosing_Object, but treats pointer dereference like component
+   --  selection. Expression N should have been resolved already.
+
    function Get_Generic_Entity (N : Node_Id) return Entity_Id;
    --  Returns the true generic entity in an instantiation. If the name in the
    --  instantiation is a renaming, the function returns the renamed generic.