From patchwork Tue Sep 6 07:15:50 2022 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: 1015 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:5044:0:0:0:0:0 with SMTP id h4csp504567wrt; Tue, 6 Sep 2022 00:20:15 -0700 (PDT) X-Google-Smtp-Source: AA6agR4eZF8I9c8xcp6wcgM1ek0kHUoAzYaM4q0+aqsVb9TKpTNUMyRQUjLQLaENEOXLjaV+v5n2 X-Received: by 2002:aa7:d0c7:0:b0:44d:f0ed:75b8 with SMTP id u7-20020aa7d0c7000000b0044df0ed75b8mr10031014edo.50.1662448815796; Tue, 06 Sep 2022 00:20:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1662448815; cv=none; d=google.com; s=arc-20160816; b=wYxPj0Wjt/6rO4QIu5a3M0sZkBNAN8SiTFTIbAwJXwdj4UxXSwXwZeGkKnnPIDwVRQ TpRTeOFjUq402NIxbKiKj40vXF0hx5/LUWEEdIwOTsQ+Xf0wEgOQGBGsb+Cs6XREZL6F Ko4XVHFiiWNXHNtw4YoiYll4lYlrYFDGiEOrJf9ib1lLxmClbobMQEOC1m9hEniRA+yO p7XsYjA7pL0EJAO1EEO4x23da+Xwmkx8VNqGlikaaiCLa0wZCKhdSK7LqxhsHVuozwUa Wz3mqZJuTx1Az4ZbE/oGzTLC7PxYg27t/WVUqK+mMGLNiw7qmxcUxFhLHrTMG2i019+d TBhg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:cc:reply-to:from:list-subscribe:list-help :list-post:list-archive:list-unsubscribe:list-id:precedence :content-disposition:mime-version:message-id:subject:to:date :dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=cVyanA9VlvZpOFuxA2EKlExDqm2WguJpn1ujBWDHkJo=; b=dZZVEmCtBt3V+xGCk0QEJeTyzlakpTwuo8tO2GI8WbNP2GebCrswnCQ96uPzkzt5vp gSKqv5lMMXOjnpN3V2Fj8/XEcqc4zImPVOIzzgWdRcvsWggKPL9gmEu+HZCsek5k3aEV w0LnWvvMKiWTOi+Q5mZNmKA5QKWuPsL4WJSzjPYnrEoPo30EAeBXLudqTOxZcVoCWMNB 6mXP+Jycfg/MkSK0HOVbioP8KhFBPmGLAvB1E74wXybXsDdoGBEP3Yhf67ur4hfbVp8w +uz7KlF3hULIQlgnmaGZ+T2l8F3eDwMNqCowyiTPVXGxhEaZ3oNBf/AywNIF0zONYvsF joaA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=KnzqO2L1; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c 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 (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id ht14-20020a170907608e00b0076f0ab6f6e0si567033ejc.527.2022.09.06.00.20.15 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Sep 2022 00:20:15 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=KnzqO2L1; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c 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 E428B3898C6A for ; Tue, 6 Sep 2022 07:17:42 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org E428B3898C6A DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1662448662; bh=cVyanA9VlvZpOFuxA2EKlExDqm2WguJpn1ujBWDHkJo=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=KnzqO2L1MWV091719sBO+sQ8vU0gxPQzykqeH4im2+SO4HerydvHwvHSjYFBj2BCc yR9zlU3MlXBBd8rEa0JnU5Qz+BQV5bDQsiYGstgVU8f/s2efkY4HZUAWrvAiQoD6mF ho4JMfVvlfqD9YpBPjHiwrJ/Wi5+FfBKNMFU6Vts= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32d.google.com (mail-wm1-x32d.google.com [IPv6:2a00:1450:4864:20::32d]) by sourceware.org (Postfix) with ESMTPS id AE20E3851164 for ; Tue, 6 Sep 2022 07:15:52 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org AE20E3851164 Received: by mail-wm1-x32d.google.com with SMTP id d5so6356321wms.5 for ; Tue, 06 Sep 2022 00:15:52 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :x-gm-message-state:from:to:cc:subject:date; bh=cVyanA9VlvZpOFuxA2EKlExDqm2WguJpn1ujBWDHkJo=; b=Hqo1erDuGuXSKjsYca7tFZmBDQCmtvd48+fDUDOHt/zgWvsyHUt2PUaKshxUB5qq14 AvEOewQBSVrTdkqVN8O23Rs7XNs5Bsbl21KSIz1szmqxAwgsg0vUoP0hy+A6XNf5OyXc xckbeOiYfkIuiEPumwqmCef9KJWKEExo62k3SB34visBsFpaoIxN0EVQA58v/fBmpqRQ Ih20zbiA1gCOrE/bXXu45Bnog0xniuXbJ7sitHeDDlzEz/F0ZC3bThj5KB0LLsUYQFKB 13E0MvzDFt5YXkaSsncYb3GIx+RzEFh4HMChreN+IPbBj9g6tSE43sJVDyrah75wbMYh Wi6Q== X-Gm-Message-State: ACgBeo0C+iezY5fuwoNa4UWrs+8aTpnB6lBxMKuN1hYoT3LJ2wKFa7rP Ni3fUC2s++AfEbbuSE84ItBQ/M3ACMtnHg== X-Received: by 2002:a05:600c:3502:b0:3a6:edc:39f8 with SMTP id h2-20020a05600c350200b003a60edc39f8mr12984251wmq.200.1662448551576; Tue, 06 Sep 2022 00:15:51 -0700 (PDT) Received: from poulhies-Precision-5550 (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id e5-20020adfe7c5000000b0022862e037e3sm7774367wrn.38.2022.09.06.00.15.50 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Sep 2022 00:15:51 -0700 (PDT) Date: Tue, 6 Sep 2022 09:15:50 +0200 To: gcc-patches@gcc.gnu.org Subject: [Ada] Fix a bug in the contract of formal ordered sets Message-ID: <20220906071550.GA1280361@poulhies-Precision-5550> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.9 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: Marc =?iso-8859-1?q?Poulhi=E8s?= Cc: Julien Bortolussi 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?1743203929451886086?= X-GMAIL-MSGID: =?utf-8?q?1743203929451886086?= There are 2 main issues in the postcondition of the function Replace of the formal ordered sets, in the sub package Generic_Keys. One is related to the fact that when the element is changed, the key is also changed. The second one is due to the fact that the arrival of the new element might modify the ordering of the set and thus the Positions might be modified. As a consequence, the postcondition might be false and thus fail at runtime. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-cforse.ads (Replace): Fix the postcondition. diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads --- a/gcc/ada/libgnat/a-cforse.ads +++ b/gcc/ada/libgnat/a-cforse.ads @@ -1598,7 +1598,7 @@ is -- Key now maps to New_Item - and Element (Container, Key) = New_Item + and Element (Container, Find (Container, Key)'Old) = New_Item -- New_Item is contained in Container @@ -1622,8 +1622,9 @@ is E_Right => Elements (Container), P_Left => Positions (Container)'Old, P_Right => Positions (Container), - Position => Find (Container, Key)) - and Positions (Container) = Positions (Container)'Old; + Position => Find (Container, Key)'Old) + and P.Keys_Included (Positions (Container), + Positions (Container)'Old); procedure Exclude (Container : in out Set; Key : Key_Type) with Global => null,