From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Yannick Moy <moy@adacore.com>
Subject: [Ada] Issue error on invalid use of Ghost inside pragma Predicate
Date: Mon, 25 Oct 2021 15:08:53 +0000 [thread overview]
Message-ID: <20211025150853.GA346257@adacore.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 450 bytes --]
Checking for ghost placement was only occurring inside the various
versions of predicate aspects, not inside the pragma Predicate. Now
fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_ch13.adb (Freeze_Entity_Checks): Perform same check on
predicate expression inside pragma as inside aspect.
* sem_util.adb (Is_Current_Instance): Recognize possible
occurrence of subtype as current instance inside the pragma
Predicate.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2344 bytes --]
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -13144,6 +13144,28 @@ package body Sem_Ch13 is
else
Check_Aspect_At_Freeze_Point (Ritem);
end if;
+
+ -- A pragma Predicate should be checked like one of the
+ -- corresponding aspects, wrt possible misuse of ghost
+ -- entities.
+
+ elsif Nkind (Ritem) = N_Pragma
+ and then No (Corresponding_Aspect (Ritem))
+ and then
+ Get_Pragma_Id (Pragma_Name (Ritem)) = Pragma_Predicate
+ then
+ -- Retrieve the visibility to components and discriminants
+ -- in order to properly analyze the pragma.
+
+ declare
+ Arg : constant Node_Id :=
+ Next (First (Pragma_Argument_Associations (Ritem)));
+ begin
+ Push_Type (E);
+ Preanalyze_Spec_Expression
+ (Expression (Arg), Standard_Boolean);
+ Pop_Type (E);
+ end;
end if;
Next_Rep_Item (Ritem);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -16644,7 +16644,8 @@ package body Sem_Util is
-- Predicate_Failure aspect, for which we do not construct a
-- wrapper procedure. The subtype will be replaced by the
-- expression being tested when the corresponding predicate
- -- check is expanded.
+ -- check is expanded. It may also appear in the pragma Predicate
+ -- expression during legality checking.
elsif Nkind (P) = N_Aspect_Specification
and then Nkind (Parent (P)) = N_Subtype_Declaration
@@ -16652,7 +16653,8 @@ package body Sem_Util is
return True;
elsif Nkind (P) = N_Pragma
- and then Get_Pragma_Id (P) = Pragma_Predicate_Failure
+ and then Get_Pragma_Id (P) in Pragma_Predicate
+ | Pragma_Predicate_Failure
then
return True;
end if;
reply other threads:[~2021-10-25 15:08 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=20211025150853.GA346257@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).