aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2020-12-08 09:23:09 +0100
committerPierre-Marie de Rodat <derodat@adacore.com>2021-04-28 05:38:00 -0400
commit3545103fa4c2586796e1738b19ca8cb049998951 (patch)
tree738281ca30edab4433f8bd15436d0a9b7c051710
parent75716ebc25bfb4a647b05d0b2443b5495dab425e (diff)
downloadgcc-3545103fa4c2586796e1738b19ca8cb049998951.zip
gcc-3545103fa4c2586796e1738b19ca8cb049998951.tar.gz
gcc-3545103fa4c2586796e1738b19ca8cb049998951.tar.bz2
[Ada] Improve error message for ghost in predicate
gcc/ada/ * ghost.adb (Check_Ghost_Context): Add continuation message when in predicate.
-rw-r--r--gcc/ada/ghost.adb50
1 files changed, 50 insertions, 0 deletions
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 866f7f7..0311020 100644
--- 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;