From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Yannick Moy <moy@adacore.com>
Subject: [Ada] Improve error message for ghost in predicate
Date: Wed, 28 Apr 2021 05:41:39 -0400 [thread overview]
Message-ID: <20210428094139.GA139645@adacore.com> (raw)
[-- 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;
reply other threads:[~2021-04-28 9:41 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20210428094139.GA139645@adacore.com \
--to=derodat@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=moy@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).