From patchwork Tue Sep 5 11:07:59 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: 137499 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:ab0a:0:b0:3f2:4152:657d with SMTP id m10csp1605599vqo; Tue, 5 Sep 2023 04:10:21 -0700 (PDT) X-Google-Smtp-Source: AGHT+IFzV5cLOEJ1FcaYTTumCQ9YvJzUVLpUvmi6r8VqqX5QIM/c7ob8UxKvAWmeNgAx9zBloHnD X-Received: by 2002:a17:907:b18:b0:9a6:4f23:9d8f with SMTP id h24-20020a1709070b1800b009a64f239d8fmr4032430ejl.47.1693912221424; Tue, 05 Sep 2023 04:10:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1693912221; cv=none; d=google.com; s=arc-20160816; b=KByBMO5ChkcY+dD1eNgdD/4SWaCsnJJWkl9p2gmmV3aImjz1jlZZgIcVxfWI5P+ZSw 1eYJAd5ef9LUU9ZApYXpRnAP48CrIC+mFn625Ycw2tROOMehNEJ1t6Sl2lotvl3DJjLM ynFVGC8naN0gZ0aeweGm5Zn6CoCwHPihFI/IHUafQyeNGe2s0NLDXu/BO1Km5DS6RQ7v ExV/v7IP0m8VdqTRSmgDGSv24ezCqiclvtKYrPJDg7u/cMhvrj0R4FRa+W3IflUWBUMU 0k6S9B5TTN3nvaNFGwobglONUUjv/c3jn5s4NyqQWbWhFgNRh7JX+29i4KbMmDE2rKr4 kBVg== 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=kxMz3hvLngNNc2iFdzlxO2Hx8HqUQ9NYNH7vsjTTotE=; fh=TQgQFHlWkFxdBV4U28EkGDBgG4nPpypv77B7Up3yEzk=; b=DwEzx2WOgIAvgOk7gk0kFs4T5Ivcl5ySE5qszlZb3MoiMeyRSGcEzwor4Sm3N3/sge TbDsGvzSw+maMlEg6gjFTsurerjeKW0eirs1iyNnXAnZadq9Rdhd8FYQ8Q1XN+AukkZ+ sIHgseAY+1HtWftkMRJSg3qf/6AeBTWUqwUjjZvyQszOdyqVKbHTXxN2vQf5v1mtvV98 EvqLTgzt8ZxwfBcaETCOeP81fNBg6k2hl1oKsQ8oGOHB/usWSyF9mkulGVoxsk5UBhBI hpRD9k2BILKLwPQJCnSbJrB34j7TW9kvUK0efDpMSJ/L7BU+bjAFj6cKcTLxT+mbzSgC rpIw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b="bUwFh/ug"; 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 (ip-8-43-85-97.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id vi15-20020a170907d40f00b0099bc8469e26si7038796ejc.923.2023.09.05.04.10.21 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 05 Sep 2023 04:10:21 -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="bUwFh/ug"; 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 0C2483830B7B for ; Tue, 5 Sep 2023 11:08:55 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 0C2483830B7B DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1693912135; bh=kxMz3hvLngNNc2iFdzlxO2Hx8HqUQ9NYNH7vsjTTotE=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=bUwFh/ugnt8iGNQKRs7toupCHxp4EtDLy8vjy/+c+NLu/bp6+KBVX30JX6BJ8+uKV YrGcmmNAJKKhFQenCdfhl9jAOoUYih85oUu7CRvpv5q+dg51NmRMY+5zpRsybvUvxs mG+GX6fS9jNZ2YXluXuTqk+XVx/HpLoAeMuQ53d8= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x333.google.com (mail-wm1-x333.google.com [IPv6:2a00:1450:4864:20::333]) by sourceware.org (Postfix) with ESMTPS id E9DBF3857700 for ; Tue, 5 Sep 2023 11:08:02 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org E9DBF3857700 Received: by mail-wm1-x333.google.com with SMTP id 5b1f17b1804b1-402c46c49f4so23649665e9.1 for ; Tue, 05 Sep 2023 04:08:02 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1693912082; x=1694516882; 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=kxMz3hvLngNNc2iFdzlxO2Hx8HqUQ9NYNH7vsjTTotE=; b=RddnX0q0OKHLNX9hCfq6lOu0MdsZ6KQIoRFLp9ziq1NrLfGrzAnM/mDwknnALEslxp zOvHFw7b3MJxMTHO9walPHuEbrVuTvwY/iet6EJG4iV8Y5YlUq7K3sR8LAdNIPs+nrN3 X+DYF8fYDPnAPfyC5RC9EVZJQZxVEV0yPSxRgJTprQ/CqFJUTC9GriuUDtQE9fvnqCC2 4j9sjlgjLFTGauFnVr2czHwOp3yd0DdzrxnTMREaqmDNrtFiDWUeoOdOWhhWeDhJOPQc /7CnyAjXTOTx6vuh7PcjwSWO6hlXoDbrlE1AvfDjM1SiUvY79culOqT2GBPipEGDV06L B5oA== X-Gm-Message-State: AOJu0YxKONWxVN7//zRS2wzzOtBURLRVivp0djzxtf7P9cbB3XugZxnS g2VFEbIY3uQ3aJGA/XNyyPP/+ijBRjJ8JSu7n8kREw== X-Received: by 2002:a05:600c:1c15:b0:401:5443:55a1 with SMTP id j21-20020a05600c1c1500b00401544355a1mr9026211wms.3.1693912081567; Tue, 05 Sep 2023 04:08:01 -0700 (PDT) Received: from poulhies-Precision-5550.lan ([2001:861:3382:1a90:20fc:79e4:455c:1075]) by smtp.gmail.com with ESMTPSA id r16-20020a05600c299000b00400268671c6sm16495591wmd.13.2023.09.05.04.08.00 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 05 Sep 2023 04:08:00 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Sheri Bernstein Subject: [COMMITTED] ada: Remove GNATcheck violations Date: Tue, 5 Sep 2023 13:07:59 +0200 Message-Id: <20230905110759.562386-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 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.30 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: INBOX X-GMAIL-THRID: 1776195701270563609 X-GMAIL-MSGID: 1776195701270563609 From: Sheri Bernstein Use pragma Annotate to exempt GNATcheck violations that are related to proof code. Specifically, exempt rules "Metrics_LSLOC" and "Metrics_Cyclomatic_Complexity" whose limits are exceeded due to proof code, and exempt rule "Discriminated_Records" for a variant record that is only used in proof code. gcc/ada/ * libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC. (Double_Divide): Add pragma to exempt Metrics_Cyclomatic_Complexity. (Scaled_Divide): Likewise. * libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt Discriminated_Records. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-aridou.adb | 11 +++++++++++ gcc/ada/libgnat/s-vauspe.ads | 3 +++ 2 files changed, 14 insertions(+) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index beb56bfabe1..6bcce59cfeb 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -29,6 +29,9 @@ -- -- ------------------------------------------------------------------------------ +pragma Annotate (Gnatcheck, Exempt_On, "Metrics_LSLOC", + "limit exceeded due to proof code"); + with Ada.Unchecked_Conversion; with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations; @@ -814,6 +817,8 @@ is -- Double_Divide -- ------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Metrics_Cyclomatic_Complexity", + "limit exceeded due to proof code"); procedure Double_Divide (X, Y, Z : Double_Int; Q, R : out Double_Int; @@ -1221,6 +1226,7 @@ is Prove_Signs; end Double_Divide; + pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_Cyclomatic_Complexity"); --------- -- Le3 -- @@ -1899,6 +1905,8 @@ is -- Scaled_Divide -- ------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Metrics_Cyclomatic_Complexity", + "limit exceeded due to proof code"); procedure Scaled_Divide (X, Y, Z : Double_Int; Q, R : out Double_Int; @@ -3317,6 +3325,7 @@ is Prove_Sign_R; Prove_Signs; end Scaled_Divide; + pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_Cyclomatic_Complexity"); ---------- -- Sub3 -- @@ -3658,3 +3667,5 @@ is pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Arith_Double; + +pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_LSLOC"); diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index a6f81d715c4..b276eed5105 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -68,6 +68,8 @@ is when others => raise Program_Error) with Ghost; + pragma Annotate (Gnatcheck, Exempt_On, "Discriminated_Records", + "variant record only used in proof code"); type Uns_Option (Overflow : Boolean := False) is record case Overflow is when True => @@ -76,6 +78,7 @@ is Value : Uns := 0; end case; end record; + pragma Annotate (Gnatcheck, Exempt_Off, "Discriminated_Records"); function Wrap_Option (Value : Uns) return Uns_Option is (Overflow => False, Value => Value);