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