From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 391053857BA4; Tue, 5 Sep 2023 11:07:55 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 391053857BA4 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1693912075; bh=nmhESQg7Ou+NZL87PpcAzCk9mDUtEbjqgViDgyfdxjQ=; h=From:To:Subject:Date:From; b=iT9E36mUtthTcebg5AMAIz5IwytCJsBk3SoYadidv/b9VCpzdpTbvB9kjSvhk/48b WB2+L+I2WOm50UnTIzhjfs3nILnXqiZe+3iSg+GNZMwxJeDjtVk3u4YzlTBlYEh4xh 8/BVLCaySnu5R6hSZkXRoWbOWT7hu5I+7MmKqEmU= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-3680] ada: Remove GNATcheck violations X-Act-Checkin: gcc X-Git-Author: Sheri Bernstein X-Git-Refname: refs/heads/master X-Git-Oldrev: 17fcc7df64b5b6574e8dd24095a0f146382e62c3 X-Git-Newrev: f9a68b454743fffe07fb51ed735510c2178ba14c Message-Id: <20230905110755.391053857BA4@sourceware.org> Date: Tue, 5 Sep 2023 11:07:55 +0000 (GMT) List-Id: https://gcc.gnu.org/g:f9a68b454743fffe07fb51ed735510c2178ba14c commit r14-3680-gf9a68b454743fffe07fb51ed735510c2178ba14c Author: Sheri Bernstein Date: Thu Aug 3 12:38:53 2023 +0000 ada: Remove GNATcheck violations 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. Diff: --- 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 beb56bfabe1d..6bcce59cfeb8 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 a6f81d715c41..b276eed51050 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);