From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 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-x333.google.com with SMTP id 5b1f17b1804b1-402c46c49f4so23649665e9.1 for ; Tue, 05 Sep 2023 04:08:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1693912082; x=1694516882; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=kxMz3hvLngNNc2iFdzlxO2Hx8HqUQ9NYNH7vsjTTotE=; b=cny9rbnajJLRd7TtIA+JIqTls3VpnZ2U7PcsjDz7xbvyKkBcCVQOvAyl4D3/vDh9qh S4qScMphvwOPfC4SVo3q7r4JTI6VCKkjCiFodRyh1tXYz29ZAqTnlnWMCc2ogZtLhUqT XvarbN3O7KJFhngV6UOhtiucXAt7Q2UQEXWrvdhfxOY9D/vYBS2CmFXUIqm5HilD4i9c VU2xVrsHyEy8mNivcNWfgxHBJ4zvB6DrVD7U13OKWJBT8At0tL6I3XqkwRHl1xsiClc4 3kK/tIlIenGyTrKECVYzmKd+5tHdzOJrJbF483CrcWGGkh6DhubAuxnh1KGbdrOdrh0M EI2w== 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-Google-Smtp-Source: AGHT+IG6pBzGuCcYE/gASozv2r3yCPk6uklqB87wElyKSACdb5hkC/dzEaP86ijV48aRXbiDwT+fBQ== 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) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= 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 Content-Transfer-Encoding: 8bit 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 List-Id: 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); -- 2.40.0