From patchwork Mon Oct 25 15:08:53 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 46623 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 48D5C3858423 for ; Mon, 25 Oct 2021 15:11:01 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 48D5C3858423 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1635174661; bh=tmXSku2zSAX3aOIavy/IK6Cwgd5XnjLuHvCsFTf1y3g=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=aFWmTNhkv65Q74i5TmyejROo3rLQty1q51v5wX3hShF08mKLV56JnfP+TmT59P44G S36GMoFUrV280nCIBfpAt7ZusteOTIz4VNPb8qmUreSnmrFdxZme86gUI0DpW4IgzN PwoSWPK76sC/ZJ80kd8zh2eT9kjMteHr5T0nz1X4= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lj1-x22e.google.com (mail-lj1-x22e.google.com [IPv6:2a00:1450:4864:20::22e]) by sourceware.org (Postfix) with ESMTPS id 7C45D3858001 for ; Mon, 25 Oct 2021 15:08:56 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 7C45D3858001 Received: by mail-lj1-x22e.google.com with SMTP id h11so1541588ljk.1 for ; Mon, 25 Oct 2021 08:08:56 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=tmXSku2zSAX3aOIavy/IK6Cwgd5XnjLuHvCsFTf1y3g=; b=tOVpjuefcjtjL9JK14twiHPdnYC+3jJYXoA/s5fNn5WrYPG4HyeQ7DxFXkSGXwHJUR 9wndB2tljkUJQEG3yIoputO8+ns0PELrLFR3+6xGkvhjokmmtTZJ9KnRjhrmlxuH1BUx lQ6SRK76+b2lHAuDr+QXzELxh9bnBExLWO9ZLqkFGSQuFt1RKIKJJJc4jIffVCm5FpSp 0zRnAdU+lGu8ekPnsIEEk35I2iOuSs9aK/6FEGsdkfyaS0vT3A6Yov+Rx1h4hd4oBIqy DaNWsLhIXQ5eeUs7potB1Wh9d5Ak5HgbFTvUtimFk75+bLVcWQtcK1Ayg2ljRsDQ9AIr ayKg== X-Gm-Message-State: AOAM530IAJF0fR9ySKn6+LQUJAw1/FWvQQiz+1pCUQiNb2P5g6fZ0n7n WKcOltXivtbw6GHZo8YvdjfOvK2JfVogSA== X-Google-Smtp-Source: ABdhPJxP2QWt9WtvofZdAruLAZmSW0F8LfVQdx9e6Fbj4QEdFC7jrFSyp65gtSBWgMqQW5m6S3TaDQ== X-Received: by 2002:a05:651c:2128:: with SMTP id a40mr19555387ljq.148.1635174535118; Mon, 25 Oct 2021 08:08:55 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id u4sm134193lff.198.2021.10.25.08.08.53 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 25 Oct 2021 08:08:54 -0700 (PDT) Date: Mon, 25 Oct 2021 15:08:53 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Issue error on invalid use of Ghost inside pragma Predicate Message-ID: <20211025150853.GA346257@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.1 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" 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. 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;