[Ada] Issue errors on wrong context for ghost entities

References to ghost entities should only occur in ghost context.  This
was not checked systematically on all references.

gcc/ada/

	* sem_ch2.adb (Analyze_Identifier): Add checking for ghost
	context.
	* sem_ch5.adb (Analyze_Implicit_Label_Declaration): Treat
	implicit labels like other entities by setting their ghost
	status according to context.
	* ghost.adb (Check_Ghost_Context): Adapt checking.

3 files changed, 79 insertions, 8 deletions

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 962941d..25b9a28 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -365,6 +365,17 @@ package body Ghost is
                if Is_Ghost_Pragma (Prag) then
                   return True;
 
+               --  A pragma may not be analyzed, so that its Ghost status is
+               --  not determined yet, but it is guaranteed to be Ghost when
+               --  referencing a Ghost entity.
+
+               elsif Prag_Nam in Name_Annotate
+                               | Name_Compile_Time_Error
+                               | Name_Compile_Time_Warning
+                               | Name_Unreferenced
+               then
+                  return True;
+
                --  An assertion expression pragma is Ghost when it contains a
                --  reference to a Ghost entity (SPARK RM 6.9(10)), except for
                --  predicate pragmas (SPARK RM 6.9(11)).
@@ -444,14 +455,6 @@ package body Ghost is
          if Ghost_Mode > None then
             return True;
 
-         --  A Ghost type may be referenced in a use_type clause
-         --  (SPARK RM 6.9.10).
-
-         elsif Present (Parent (Context))
-           and then Nkind (Parent (Context)) = N_Use_Type_Clause
-         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
@@ -482,6 +485,46 @@ package body Ghost is
                then
                   return True;
 
+               --  A Ghost type may be referenced in a use or use_type clause
+               --  (SPARK RM 6.9(10)).
+
+               elsif Present (Parent (Par))
+                 and then Nkind (Parent (Par)) in N_Use_Package_Clause
+                                                | N_Use_Type_Clause
+               then
+                  return True;
+
+               --  The context is an attribute definition clause for a Ghost
+               --  entity.
+
+               elsif Nkind (Parent (Par)) = N_Attribute_Definition_Clause
+                 and then Par = Name (Parent (Par))
+               then
+                  return True;
+
+               --  The context is the instantiation or renaming of a Ghost
+               --  entity.
+
+               elsif Nkind (Parent (Par)) in N_Generic_Instantiation
+                                           | N_Renaming_Declaration
+                                           | N_Generic_Renaming_Declaration
+                   and then Par = Name (Parent (Par))
+               then
+                  return True;
+
+               --  In the 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;
 
@@ -593,6 +636,13 @@ package body Ghost is
          return;
       end if;
 
+      --  When assertions are enabled, compiler generates code for ghost
+      --  entities, that is not subject to Ghost policy.
+
+      if not Comes_From_Source (Ghost_Ref) then
+         return;
+      end if;
+
       --  Once it has been established that the reference to the Ghost entity
       --  is within a suitable context, ensure that the policy at the point of
       --  declaration and at the point of use match.
diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb
index 4a45b597..6b84af4 100644
--- a/gcc/ada/sem_ch2.adb
+++ b/gcc/ada/sem_ch2.adb
@@ -26,6 +26,7 @@
 with Atree;          use Atree;
 with Einfo;          use Einfo;
 with Einfo.Utils;    use Einfo.Utils;
+with Ghost;          use Ghost;
 with Namet;          use Namet;
 with Opt;            use Opt;
 with Restrict;       use Restrict;
@@ -34,6 +35,7 @@ with Sem_Ch8;        use Sem_Ch8;
 with Sem_Dim;        use Sem_Dim;
 with Sinfo;          use Sinfo;
 with Sinfo.Nodes;    use Sinfo.Nodes;
+with Sinfo.Utils;    use Sinfo.Utils;
 with Stand;          use Stand;
 with Uintp;          use Uintp;
 
@@ -77,6 +79,18 @@ package body Sem_Ch2 is
          Find_Direct_Name (N);
       end if;
 
+      --  A Ghost entity must appear in a specific context. Only do this
+      --  checking on non-overloaded expressions, as otherwise we need to
+      --  wait for resolution, and the checking is done in Resolve_Entity_Name.
+
+      if Nkind (N) in N_Expanded_Name | N_Identifier
+        and then Present (Entity (N))
+        and then Is_Ghost_Entity (Entity (N))
+        and then not Is_Overloaded (N)
+      then
+         Check_Ghost_Context (Entity (N), N);
+      end if;
+
       Analyze_Dimension (N);
    end Analyze_Identifier;
 
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index ab9f471..6c11f64 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2119,6 +2119,13 @@ package body Sem_Ch5 is
       Mutate_Ekind        (Id, E_Label);
       Set_Etype           (Id, Standard_Void_Type);
       Set_Enclosing_Scope (Id, Current_Scope);
+
+      --  A label declared within a Ghost region becomes Ghost (SPARK RM
+      --  6.9(2)).
+
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (Id);
+      end if;
    end Analyze_Implicit_Label_Declaration;
 
    ------------------------------