From patchwork Mon May 29 08:28:53 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: 100141 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:994d:0:b0:3d9:f83d:47d9 with SMTP id k13csp1360649vqr; Mon, 29 May 2023 01:30:59 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ5XveyEUZ9w629BKfuqI4r3+PLvmC8zoPvrI45zwBkaIYIHrhNIM3QSL1REM0GLt9EHXMKU X-Received: by 2002:a05:6402:1152:b0:514:9b60:ea65 with SMTP id g18-20020a056402115200b005149b60ea65mr2841846edw.16.1685349059476; Mon, 29 May 2023 01:30:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1685349059; cv=none; d=google.com; s=arc-20160816; b=rcfa5Ic36Yseg2VTcO2rtjY2iQp5te8FQ5p/tXF7g+k6cS5qlGmUug2TUCsSBl7v78 khbebYpyax8WTbS7DvvnndVKH6oIuTi5kJ5lLDF52lSDYn6zY7cIpsMVdWkYPcXkMBkL sovEKH9HeVYUiexV8UgvKXA/s0w5Gi8sbrcRppTYke3ipgBLORSP9klB4pup8cPZZdRQ ZKM6rHUc5mtPbBrHPKlJ4VlXtWPHQcW4TfyUGTa6wgafLQPKbdZBDw6PKdWgnvi4pxPY /qJlq+HEZPPOulA1EDBTMOS9MLb+KGS/4YqNkodPYfW6w/s2XKPJm4kBhV7hN1Ob2RRB kbHg== 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=umWQMhCkpq6zPqG2qf+6cjaYV62+oUdmLnip+524hbE=; b=Gai3TWg/tRkMsU9F7w5UwBLDSJVte8gTtueSdDCgksUqCULx9l7REqZqyorEpIzT/D EvZkBXxqPTFkWFPf1ao12SbsJ8sYMlDaCYDg4qbrrhmzYHZbE+iYD7loKO445RPh4dSE LluqscWjZZysu/6M7ylroyGkatIFkoT4VFRPAVX6p4WNmcsZxXTGpNnQ8+XHOU/AEYc0 z9SMhQOnVmpFh0i96sa2yMGHoescqB71G/oLpKBVZ/0O2wiiO+UpF6zCx7lTwlHnmSbV 1M7EXpgVD4iBCevW92tYRhEKjBq+AF6wbrQ20Wu2mQqjb1vQUlDK9YdTMYmGrqO+MEFH 0FNA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=nHKcMK3a; 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 bc14-20020a056402204e00b00510d197e881si3186323edb.255.2023.05.29.01.30.59 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 May 2023 01:30:59 -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=nHKcMK3a; 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 F1D9E3853556 for ; Mon, 29 May 2023 08:30:07 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org F1D9E3853556 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1685349008; bh=umWQMhCkpq6zPqG2qf+6cjaYV62+oUdmLnip+524hbE=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=nHKcMK3aANaNQqhaQQAEYqpUrfOKpcf0JXsPi2xOOklY2Eij5qxyBtFZtTDc+L7Dj 4NAa4HgTEBMgJkkeLTaNAw3+8clSdXmVnVUw+EMFRRXZHP+ZH1lib0QkcOLg9ibPaQ RGpDZ01+cGRmUr/DUHWW8fBiZsxR11V6uWa0qQZw= 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 81867385700B for ; Mon, 29 May 2023 08:28:55 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 81867385700B Received: by mail-wr1-x42a.google.com with SMTP id ffacd0b85a97d-30789a4c537so1707273f8f.0 for ; Mon, 29 May 2023 01:28:55 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1685348934; x=1687940934; 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=umWQMhCkpq6zPqG2qf+6cjaYV62+oUdmLnip+524hbE=; b=H7LFlj1t8sp/N9g8uL/F92JVF3o/YyhTXtuR1p+JGBFXGzt6YVNgULCiPJjShPn1et KAtWycFsL5QIxJk6Ncl6hlNm5dZllsMnZrXAUOuDqsWlT5ASR8/yTR9qE26nGy25uEki ZVzUGyEXlyeV0ZByakUTq082JnwovwMh/ikBSqdVyVVbh4XCS6gEvisQ27oSjMj0LJmV vV7i8FmILpDNcJHmf2xlGVT6V+0OmRQAY3MjDVYHub8syGaIMdeB9jZW9CqKXupiODnY MN/fcQTaXUCg2dVOLCLx/AZy/+ysnML78yWob2Bmnrzc941w/74tpH0LLgNWGwpMyftx W/ig== X-Gm-Message-State: AC+VfDyvb2kli3Diw8ejSW2YwQifJSXgV2CTD1owKBla1G0XOuBzdrFg Q9FXj0uXwKOM287xE7FCi4lXsZvSvsZjTTNONlKGsA== X-Received: by 2002:a5d:6191:0:b0:306:2b40:1258 with SMTP id j17-20020a5d6191000000b003062b401258mr8545436wru.21.1685348934375; Mon, 29 May 2023 01:28:54 -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 a2-20020a056000100200b00306415ac69asm12870839wrx.15.2023.05.29.01.28.53 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 May 2023 01:28:53 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Restore SPARK_Mode On for numerical functions Date: Mon, 29 May 2023 10:28:53 +0200 Message-Id: <20230529082853.2409094-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 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 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?1767216575157297132?= X-GMAIL-MSGID: =?utf-8?q?1767216575157297132?= From: Yannick Moy GNATprove has ad-hoc support for the standard numerical functions, which consists in emitting an unprovable preconditions on cases which could lead to an overflow. These functions are thus valid to call from SPARK code. gcc/ada/ * libgnat/a-ngelfu.ads: Restore SPARK_Mode from context. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-ngelfu.ads | 6 ------ 1 file changed, 6 deletions(-) diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads index ae06ea710eb..f6d6c9643af 100644 --- a/gcc/ada/libgnat/a-ngelfu.ads +++ b/gcc/ada/libgnat/a-ngelfu.ads @@ -116,17 +116,14 @@ is Post => (if X = 0.0 then Tan'Result = 0.0); function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Tan can overflow for some values of X and Cycle Pre => Cycle > 0.0 and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.25 * Cycle, Post => (if X = 0.0 then Tan'Result = 0.0); function Cot (X : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Cot can overflow for some values of X Pre => X /= 0.0; function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Cot can overflow for some values of X and Cycle Pre => Cycle > 0.0 and then X /= 0.0 and then Float_Type'Base'Remainder (X, Cycle) /= 0.0 @@ -179,11 +176,9 @@ is Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0); function Sinh (X : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Sinh can overflow for some values of X Post => (if X = 0.0 then Sinh'Result = 0.0); function Cosh (X : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Cosh can overflow for some values of X Post => Cosh'Result >= 1.0 and then (if X = 0.0 then Cosh'Result = 1.0); @@ -192,7 +187,6 @@ is and then (if X = 0.0 then Tanh'Result = 0.0); function Coth (X : Float_Type'Base) return Float_Type'Base with - SPARK_Mode => Off, -- Coth can overflow for some values of X Pre => X /= 0.0, Post => abs Coth'Result >= 1.0;