From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x132.google.com (mail-lf1-x132.google.com [IPv6:2a00:1450:4864:20::132]) by sourceware.org (Postfix) with ESMTPS id 3C7FF3857706 for ; Tue, 13 Jun 2023 07:37:59 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 3C7FF3857706 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-lf1-x132.google.com with SMTP id 2adb3069b0e04-4f61735676fso6382600e87.2 for ; Tue, 13 Jun 2023 00:37:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1686641878; x=1689233878; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=e92V3Q7Ld4ph2AO6d8RkDiGQhGCDJf50BS9OggnA6wk=; b=D4FSZS+l51UfEd98WboRNMCrXTXvTe/s7tbx+5ghkVgB6/GG4rRCicK4d/bUu5mEwv NSFOUmnSpEXB+fBhYROQ7Cys6RO9kMXV4GooyiJ42r2EHlwXR3Wos1MrPN0c0sDq1Q7I J25K3n/s1EieBOMRgTSZ/ioGDZeSOMkVNn++DEpY90R5P0BRFIVDXDjFiknFlLumBOh6 gdoR8W/hOttPf9BGnZhI/lYUPMQlfeuhaYuv7Z37fziMwO4NntLj5H+7A4EOhedXa2KN yKyI1/zv1K6fJGGGPO8XHz/TAuiQJ1T4EfUfkHyXXmyxhftc0+2yqNTVc2rvpWI7y3bD WBhw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1686641878; x=1689233878; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=e92V3Q7Ld4ph2AO6d8RkDiGQhGCDJf50BS9OggnA6wk=; b=B3xGvlw7J+XjPVGFooUYVjeuYziAtkPG0n4+NVQrnD2KOy00LI3BHRg1NF71D9Dp49 x1AZQlKaLbwIWKogqjWMMQGLbGH/c2JSRO63XW3t7BSZACGpIIv++fiDCtID5VuGhY/N GHrMPhpDaj+Xd9Z0027vNdWE7B3MF6+n+QFks4gu7GTdU1bSSH8MY67U5JQvyTvDp3cQ /sB4EVB6fgjQtuoWcn+wDiUdfDUhqfsmoAamdWrWQHg9d0Ov8YulCXqYE8TExuNBGwYo pU8H/GsXyObHcXJiD9yBdt3RBlGszyEX5mkq7ZyWJ+Q8ook3LY4uo92QtIFyipYDZlir SqSA== X-Gm-Message-State: AC+VfDwgF5JcR86GPOReasPldOAM9w+HS0G5BtCwdALAVCbt2kINmj/O 9gSKc8XCYswo8t5A05gGBfOjK6srMvMVtPXBpyAuMg== X-Google-Smtp-Source: ACHHUZ7AW0WUU0b8mrHPKTBWOZS70A6epqoR29QiaTpqhr2OeSExizhfepNoG4QtZzUIPZJXWGaOuQ== X-Received: by 2002:a19:671a:0:b0:4f1:458c:c4c with SMTP id b26-20020a19671a000000b004f1458c0c4cmr5053173lfc.43.1686641877799; Tue, 13 Jun 2023 00:37:57 -0700 (PDT) Received: from localhost.localdomain ([2001:861:3382:1a90:bfa8:5d29:40e5:cc66]) by smtp.gmail.com with ESMTPSA id v26-20020a1cf71a000000b003f80e81705asm10254416wmh.45.2023.06.13.00.37.56 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 13 Jun 2023 00:37:57 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Use ghost predicate in standard library Date: Tue, 13 Jun 2023 09:37:56 +0200 Message-Id: <20230613073756.239408-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.7 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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: From: Yannick Moy In preparation for attribute Initialized to become ghost, use aspect Ghost_Predicate instead of Predicate in unit Ada.Strings.Superbounded of the standard library. gcc/ada/ * libgnat/a-strsup.ads: Change predicate aspect. * sem_ch13.adb (Add_Predicate): Fix for first predicate. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strsup.ads | 2 +- gcc/ada/sem_ch13.adb | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 7a8a2bac996..2e0cd98f8d4 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -69,7 +69,7 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- Leaving it out is more efficient. end record with - Predicate => + Ghost_Predicate => Current_Length <= Max_Length and then Data (1 .. Current_Length)'Initialized, Put_Image => Put_Image; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 32771f06d76..2b8b64aa392 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -10101,9 +10101,13 @@ package body Sem_Ch13 is -- Start of processing for Add_Predicate begin - -- A ghost predicate is checked only when Ghost mode is enabled + -- A ghost predicate is checked only when Ghost mode is enabled. + -- Add a condition for the presence of a predicate to be recorded, + -- which is needed to generate the corresponding predicate + -- function. if Is_Ignored_Ghost_Pragma (Prag) then + Add_Condition (New_Occurrence_Of (Standard_True, Sloc (Prag))); return; end if; -- 2.40.0