From patchwork Tue Jun 2 08:45:02 2026 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 136240 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from vm01.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 631E54BA23D9 for ; Tue, 2 Jun 2026 08:51:46 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 631E54BA23D9 Authentication-Results: sourceware.org; dkim=pass (2048-bit key, secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=Gg1X+OgU X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32b.google.com (mail-wm1-x32b.google.com [IPv6:2a00:1450:4864:20::32b]) by sourceware.org (Postfix) with ESMTPS id E572B4BA2E37 for ; Tue, 2 Jun 2026 08:46:08 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org E572B4BA2E37 Authentication-Results: sourceware.org; dmarc=pass (p=quarantine dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org E572B4BA2E37 Authentication-Results: sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::32b ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1780389969; cv=none; b=U5C7nuAVlDTArZwuHX6NZWx05M69Dq5v1Sc1brYCZM8aZr/6k0hX9F5eEXLl6Jz7GlLrT3s7877LoBVpIoIsKyR0fAsmCKq3Jka5D7HPpIRU7D+Kgpx2Si7qsWbHLzUuiuFJqOshyF2t1Js93Gf/uIqJYKpgRCXewbbZ6Du04VA= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1780389969; c=relaxed/simple; bh=pSF2HxzvFDRfUVX8PsmzJp93iX1FCl2Hg0XcTrKSLBo=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=DD7QtIVbTCzsZub4+3/HZrqGWapmWmx8P0aUZfwlTEghz0LE2pdelFWsA1BVzrLmuSTlWy9skIdNBzKwnfi3l0hzZ4ynXtj0o3RlZ8Gwum0/e0ju2lCp0cC9hegIrjT114U/2+4cIUCohHQFGPjohTTgkeD8ZlO3HhwsEu6mdLw= ARC-Authentication-Results: i=1; sourceware.org; dkim=pass (2048-bit key, secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=Gg1X+OgU DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org E572B4BA2E37 Received: by mail-wm1-x32b.google.com with SMTP id 5b1f17b1804b1-4905529b933so85884145e9.0 for ; Tue, 02 Jun 2026 01:46:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1780389968; x=1780994768; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=OqZ6BJ1RjVGLHrLxGKRUCti7fWSiLAZFQxAdV/cv5og=; b=Gg1X+OgUXvXZ6xqsdzG+yIcWqxVtCoycAA+cFuqmLJW35IOpr751ar1ag+tLiDAAlv FH7Xjvj1kDxueR6hPVRdty6QuOtetDeBeyH1IX+Q9xi9UZENQJKFXg+GsHkTEQO1UoU6 7X+mKvg0IZuTJbWGUxBfk+Lhj0/iL+KLCTgyXKJUEoDx1Mk0yIZQIrUWp7uT7MbxnbpB EARvkyyWaKVSw0KBCKKpm0Lz6UxdZnNKCBv9kNxdres64FzxQZWGWCs9Mb69GRKATss1 /mYjHbqfye3PPX2/L+j6fF33dwgYX2qW7dZ2BwkcI2+dqOTR/dcX4FEF4NbCXNio7hst vAhg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1780389968; x=1780994768; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-gg:x-gm-message-state:from :to:cc:subject:date:message-id:reply-to; bh=OqZ6BJ1RjVGLHrLxGKRUCti7fWSiLAZFQxAdV/cv5og=; b=tDVWfQyxUxELeDnlFggLx+PQw/lC/sP20QNAIZH3U0TWTR5KCPIKaSp/7xjPctpBJs u7r2hAORA8B+cCXlF5Ajf2mA3SkMPxqAncahRNP3k6qWM7JeMLVK4qDp4etCjUSu+Wwj bx11ThQUtC00Z859x6I0PO2zscrKqwxxB5XlyyR9O4EB9Vi9feglK5ZTTzvXkdAUQ5GB ELfjVDi10jx93/J0nM10cknGxkcL0h/QCHqyTyIEhBQmeUjfZEkL9R6G+l0ptTIV+KA8 OjLf+C6Iz7X8mIjF1D6IRARPtKBUAvJBIkG2EOG9ljlMlrL2Uz+CxI+On07MU3bdzcGU CpXw== X-Gm-Message-State: AOJu0YwsWVoUKBPzlo8qxZndYtBQpLsFQLLR/QSMCOLSxZNXu7owvMIM kgUBxzLfeeHonLGRGvoxF+QTKDdCM7Dts8iLh/QTcKC+CeeEK1f1B8txwe13FTtmFHS52sLGRQG U34M= X-Gm-Gg: Acq92OFcegL8L8XtDS7HgcRVLdhyeTYETiggiQAJlxGt0ceVQ8+tFXMh0tMQ4k1f3ew LUsuKzfI6bNWQAcCAcunEb2bXlVdOA6H9QkNLWhZPoWiqjttwQEQZ3OZt6lQGQSrAOTeVEIJ/2p VXJh2a/CF7uROW0Yps74NnfRtAZEZyhaA1D5gsESv9bPCqRW1qhyau/Dhs/EyuLbJy+cbwJapN1 CnmEgicTNMvSDvU9sWg273JqOx2JdcAvCTBBvNEf41dvPui5QYvN7PICey4XnsncOmJNLIe9Nv4 wO8ZxZd3UU4rD8CQC6OmDiizwb53g2+alovzAcH98lU84za3aIewLGhqYJHrMQ8u9cv/DzWcAu7 uUme91EBMiy/LhlE9t+4lqIRxt01D+3AkDaDraXL5Q1iEzxHW3cp0tEe0gbUpD+oU5CSdi1i/SD s5RUWxuBhU0S8LZ9SAiUkZz+tf2HrH9JyR7bXJmAk1nlwxGdoY3NLqG624jhWme2613g7p4OoKu n9ozyvcQx5YmsAOFjL+xPBamQxbEVU= X-Received: by 2002:a05:600d:844f:20b0:490:9dc3:3473 with SMTP id 5b1f17b1804b1-490a2923a64mr204735575e9.2.1780389967878; Tue, 02 Jun 2026 01:46:07 -0700 (PDT) Received: from mecano.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-490ab55d39csm33907625e9.35.2026.06.02.01.46.07 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 02 Jun 2026 01:46:07 -0700 (PDT) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Viljar Indus Subject: [COMMITTED 14/51] ada: Fix SPARK RM 6.9(23) check for limited private types Date: Tue, 2 Jun 2026 10:45:02 +0200 Message-ID: <20260602084541.3829876-14-poulhies@adacore.com> X-Mailer: git-send-email 2.53.0 In-Reply-To: <20260602084541.3829876-1-poulhies@adacore.com> References: <20260602084541.3829876-1-poulhies@adacore.com> MIME-Version: 1.0 X-Spam-Status: No, score=-13.8 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_BLOCKED, RCVD_IN_PBL, SPF_HELO_NONE, SPF_PASS, TXREP shortcircuit=no autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces~patchwork=sourceware.org@gcc.gnu.org From: Viljar Indus The Check_Ghost_Equality_Op predicate was checking the type directly instead of its underlying type, so a limited private type whose full view is a non-limited record was incorrectly bypassing the check. Additionally, the check was never deferred to Process_Full_View, so equality operators declared in the visible part of a package were not re-checked once the full view became available. gcc/ada/ChangeLog: * ghost.adb (Check_Ghost_Equality_Op): Use Underlying_Type to look through the private view before checking Is_Record_Type and Is_Limited_Record. * sem_ch3.adb (Process_Full_View): After completing the full view, re-check any primitive equality operators on the private type against SPARK RM 6.9(23) via Check_Ghost_Equality_Op. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/ghost.adb | 10 +++++++++- gcc/ada/sem_ch3.adb | 21 +++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index a87d044524b..afa6b97947f 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1072,12 +1072,20 @@ package body Ghost is ----------------------------- procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id; Typ : Entity_Id) is + Underlying : constant Entity_Id := Underlying_Type (Typ); begin if not Is_Ghost_Entity (Eq_Op) then return; end if; - if not Is_Record_Type (Typ) or else Is_Limited_Record (Typ) then + -- Look through any private view to get the underlying record type, + -- since a limited private type whose full view is a non-limited record + -- does not have "only limited views" and must be checked. + + if No (Underlying) + or else not Is_Record_Type (Underlying) + or else Is_Limited_Record (Underlying) + then return; end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 99799431d87..bc02601fe0c 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -22515,6 +22515,27 @@ package body Sem_Ch3 is (Underlying_Full_View (Full_T), Priv_T); end if; + -- Now that the full view is known, check any primitive equality + -- operators declared in the visible part against SPARK RM 6.9(23). + -- This check is deferred from Check_For_Primitive_Subprogram because + -- the full view of a private type is not available when the operator + -- is declared in the visible part of the package. + + if Has_Primitive_Operations (Priv_T) then + declare + Prim : Elmt_Id := First_Elmt (Primitive_Operations (Priv_T)); + Op : Entity_Id; + begin + while Present (Prim) loop + Op := Node (Prim); + if Chars (Op) = Name_Op_Eq then + Check_Ghost_Equality_Op (Op, Priv_T); + end if; + Next_Elmt (Prim); + end loop; + end; + end if; + <> Restore_Ghost_Region (Saved_Ghost_Config); end Process_Full_View;