[Ada] Improve error message for ghost in predicate

[Ada] Improve error message for ghost in predicate

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 334 bytes --]

It may be surprising to users that a ghost entity is not allowed to
appear in a predicate, which is a kind of assertion. Explain this in a
continuation message, as well as the possible fixes.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* ghost.adb (Check_Ghost_Context): Add continuation message when
	in predicate.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2492 bytes --]

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -159,6 +159,9 @@ package body Ghost is
       --  Determine whether node Context denotes a Ghost-friendly context where
       --  a Ghost entity can safely reside (SPARK RM 6.9(10)).
 
+      function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean;
+      --  Return True iff N is enclosed in an aspect or pragma Predicate
+
       -------------------------
       -- Is_OK_Ghost_Context --
       -------------------------
@@ -540,6 +543,40 @@ package body Ghost is
          end if;
       end Check_Ghost_Policy;
 
+      -----------------------------------
+      -- In_Aspect_Or_Pragma_Predicate --
+      -----------------------------------
+
+      function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean is
+         Par : Node_Id := N;
+      begin
+         while Present (Par) loop
+            if Nkind (Par) = N_Pragma
+              and then Get_Pragma_Id (Par) = Pragma_Predicate
+            then
+               return True;
+
+            elsif Nkind (Par) = N_Aspect_Specification
+              and then Same_Aspect (Get_Aspect_Id (Par), Aspect_Predicate)
+            then
+               return True;
+
+            --  Stop the search when it's clear it cannot be inside an aspect
+            --  or pragma.
+
+            elsif Is_Declaration (Par)
+              or else Is_Statement (Par)
+              or else Is_Body (Par)
+            then
+               return False;
+            end if;
+
+            Par := Parent (Par);
+         end loop;
+
+         return False;
+      end In_Aspect_Or_Pragma_Predicate;
+
    --  Start of processing for Check_Ghost_Context
 
    begin
@@ -555,6 +592,19 @@ package body Ghost is
 
       else
          Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
+
+         --  When the Ghost entity appears in a pragma Predicate, explain the
+         --  reason for this being illegal, and suggest a fix instead.
+
+         if In_Aspect_Or_Pragma_Predicate (Ghost_Ref) then
+            Error_Msg_N
+              ("\as predicates are checked in membership tests, "
+               & "the type and its predicate must be both ghost",
+               Ghost_Ref);
+            Error_Msg_N
+              ("\either make the type ghost "
+               & "or use a type invariant on a private type", Ghost_Ref);
+         end if;
       end if;
    end Check_Ghost_Context;