From patchwork Mon May 15 09:44:29 2023 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: 94068 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:b0ea:0:b0:3b6:4342:cba0 with SMTP id b10csp6796483vqo; Mon, 15 May 2023 02:59:51 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ4arKk7N8N3wWGLIUF/G/lnDhhLT5R13YDVm1covOH8ojqV5PjvrMDqkaft7xfifTVHmsT4 X-Received: by 2002:aa7:d455:0:b0:50d:a27b:10c2 with SMTP id q21-20020aa7d455000000b0050da27b10c2mr18480845edr.6.1684144790939; Mon, 15 May 2023 02:59:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684144790; cv=none; d=google.com; s=arc-20160816; b=GBSA+piCDMTdQYVYoedvLNj0JFsjYwcDPXoc4eSsyUxLK5ZD1nG/k+SIfV0QfbV6p0 MxCTzcwe2CZ3HHtZ1viwxndReRbEF2HvQgQAK4WMMTnrM6AlgvwnPWpNiEb6zcbRJdLX sp66ATmOj1p/ymivWVxuVBLXkqOhrYdQfzUyvg3oixFpeJCZXgYHV4Dc0rWy+Z2zoGbG UaX5KEd9HpexW0zjyCAQT1FqyjuHWBze94Hreat0zsR9S1tWiBZz2QEKLj3uklScL3Kn 4Z6TyUAo4y/WvfG/xydoSvjTNofpNPHnMmTeSu+kMYQZ/0uO5Z7vVIk6uZyWvf2HCNpu Bx+A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=UwEhIHvboDuh6TAHuPNRs0zSiNT+/77t8abMwqEGL+0=; b=QwCdjeSfSxwyWdyo233iH2oBAZlbuB30HBN5fLCSkgJaSQ2Sr9v+q4pvae0jmwZg6m sKkZvZ8e8orqF3Qfjb7omtL8KVmZqLSr3xt0Ort2CEnA+mhqJRN361L8QCE60WlH736l yvEQo3A5y045D52N/H0Vxd/bmXBPILSkzpcqlgeRnkZVsVzQQQ+W+0JPGtqfBOdcfxC2 kwot0eudtvFpLYTVE18MV9DMbnpJoVWE+wpggv2cE0OnUkJR81JDdkUZ86RErNiB2sn6 W5Nu7KZlyvWY0i3tCu9Q9solljSIw3TY7uyVTiQ82AamSJh//wnJLs9WHuVrE55N9Iat mR0g== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=gpilh1St; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (ip-8-43-85-97.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id bo12-20020a0564020b2c00b005068f0309cbsi10549720edb.268.2023.05.15.02.59.50 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:59:50 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=gpilh1St; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 7201138A9095 for ; Mon, 15 May 2023 09:54:02 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 7201138A9095 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684144442; bh=UwEhIHvboDuh6TAHuPNRs0zSiNT+/77t8abMwqEGL+0=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=gpilh1St8Y+mALVt1NorL93ggR4CDt08iaivrLACbnaxRjX8rYz+UDFSSdxkDQDXM +h90By/L0/kaE0EiqIMY1dRilPUfGpf4YaxdGhdpZbwfvKgaw22RsCnwmNnLc98JCM 4puQzMiHUNFBGxMJj31k4Yc2xhOFDUv0BZz8SFrQ= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x42a.google.com (mail-wr1-x42a.google.com [IPv6:2a00:1450:4864:20::42a]) by sourceware.org (Postfix) with ESMTPS id AC9793836F2A for ; Mon, 15 May 2023 09:44:32 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org AC9793836F2A Received: by mail-wr1-x42a.google.com with SMTP id ffacd0b85a97d-307a8386946so4762665f8f.2 for ; Mon, 15 May 2023 02:44:32 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684143871; x=1686735871; 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=UwEhIHvboDuh6TAHuPNRs0zSiNT+/77t8abMwqEGL+0=; b=Kwtm55obLjtJesj6pkaYf/mIWXN0fW6+FVoeb9bIQ+r4GwvazhvIwmvDxqBNd+T2JQ iCRJHRwPJ5jh6Q2ZCME1/YsLvbOTBacMfuIpDffaEvt4KmXygGFvJUJiFMKD9wTffghb S68I5uN/joHdBC1HJmQfDH06/MmDMJkmwdFbxJyOX1jqdfX1ugIstXFJQe8Co5l8p1Vz 0uRsD/zzAHFzbdxcYAq02TVul8z/dled9EeSvI/EF1OFr5kdtrC1mYTTNaaIf1FGAylu VJ87ORKqUpSlTtw/lB5tw5PYKW7TD2pk2o0swFIRTNZJk6mJbNwJDokNbXIQWB7Jg0Oq M5nQ== X-Gm-Message-State: AC+VfDxKCKiIKamFwNEUeHD6wZhbHVm5Yyu21IWxYeqFUa5enAgGJKLt V+RA7i/weIQ2CfPuBpSIucLTYsAg5gzd9SnsJz0O5Q== X-Received: by 2002:a5d:4d92:0:b0:306:26d6:dd7a with SMTP id b18-20020a5d4d92000000b0030626d6dd7amr23416084wru.32.1684143871508; Mon, 15 May 2023 02:44:31 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id x20-20020a1c7c14000000b003f17af4c4e0sm36152724wmc.9.2023.05.15.02.44.30 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:44:30 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Recover proof of runtime units Date: Mon, 15 May 2023 11:44:29 +0200 Message-Id: <20230515094429.1409007-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.4 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 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: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1765953808334399423?= X-GMAIL-MSGID: =?utf-8?q?1765953808334399423?= From: Yannick Moy Changes needed to make proof go through, after some change in GNAT and SPARK. gcc/ada/ * libgnat/a-strsup.adb (Super_Slice): Reorder component assignment to avoid failing predicate check related to initialization. * libgnat/s-expmod.adb (Exp_Modular): Add intermediate assertion. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strsup.adb | 11 ++++++----- gcc/ada/libgnat/s-expmod.adb | 1 + 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb index a9323cf0d3e..dd7b0322b76 100644 --- a/gcc/ada/libgnat/a-strsup.adb +++ b/gcc/ada/libgnat/a-strsup.adb @@ -1654,6 +1654,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is Low : Positive; High : Natural) return Super_String is + Len : constant Natural := (if Low > High then 0 else High - Low + 1); begin return Result : Super_String (Source.Max_Length) do if Low - 1 > Source.Current_Length @@ -1662,9 +1663,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is raise Index_Error; end if; - Result.Current_Length := (if Low > High then 0 else High - Low + 1); - Result.Data (1 .. Result.Current_Length) := - Source.Data (Low .. High); + Result.Data (1 .. Len) := Source.Data (Low .. High); + Result.Current_Length := Len; end return; end Super_Slice; @@ -1674,6 +1674,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is Low : Positive; High : Natural) is + Len : constant Natural := (if Low > High then 0 else High - Low + 1); begin if Low - 1 > Source.Current_Length or else High > Source.Current_Length @@ -1681,8 +1682,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is raise Index_Error; end if; - Target.Current_Length := (if Low > High then 0 else High - Low + 1); - Target.Data (1 .. Target.Current_Length) := Source.Data (Low .. High); + Target.Data (1 .. Len) := Source.Data (Low .. High); + Target.Current_Length := Len; end Super_Slice; ---------------- diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb index 6cf68a5b586..0682589d352 100644 --- a/gcc/ada/libgnat/s-expmod.adb +++ b/gcc/ada/libgnat/s-expmod.adb @@ -309,6 +309,7 @@ is Lemma_Mod_Mod (Rest * Rest, Big (Modulus)); Lemma_Mod_Ident (Big (Result), Big (Modulus)); Lemma_Mult_Mod (Big (Result), Rest * Rest, Big (Modulus)); + pragma Assert (Big (Factor) >= 0); Lemma_Mult_Mod (Big (Result), Big (Factor) ** Exp, Big (Modulus)); pragma Assert (Equal_Modulo