public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
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).