From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 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-wm1-x32d.google.com with SMTP id d5so6356321wms.5 for ; Tue, 06 Sep 2022 00:15:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :from:to:cc:subject:date; bh=cVyanA9VlvZpOFuxA2EKlExDqm2WguJpn1ujBWDHkJo=; b=Pwue9+6UMacbVYM30Rvw+waF8M3RzZ0e9PsFj17JTyoG7ab9w3dP5FU9LxAwFdaft/ GszUuHt4K1XZBw++atVnbpwMtNzAj/Xh/qUXQm4+TMhsgnUTBm3YHcdjrWUb9KWgWA6L njbWDmgjmYt8HNGO1URSoX1dnI9yQJKLgkQ0M4OCgnCLBGUAp+Zn1OM4QMv6gPINqRPW 6eV4Xe73h5Ig+S1vOgvQtVS2Qhq++sV4H8unOZWZ5buDT3nZUvmxQsIyvHlrP5s27oxX UtDwB+unvLOVo2XpapDHFa9ovIlWuzdyIRmNyIXRUH/kh5V56BnaC9Q5rPjNuXA6TPl2 On2g== 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-Google-Smtp-Source: AA6agR5SWNWKsF/lqf2ea5MfkUEA+RutsPq/dc91L0ZoiWCmLFBUffFyK8Df0lHhNvZFre1uXDtpMw== 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 From: Marc =?iso-8859-1?Q?Poulhi=E8s?= To: gcc-patches@gcc.gnu.org Cc: Julien Bortolussi Subject: [Ada] Fix a bug in the contract of formal ordered sets Message-ID: <20220906071550.GA1280361@poulhies-Precision-5550> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="FL5UXtIhxfXey3p5" 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 List-Id: --FL5UXtIhxfXey3p5 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. --FL5UXtIhxfXey3p5 Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" 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, --FL5UXtIhxfXey3p5--