From f9a68b454743fffe07fb51ed735510c2178ba14c Mon Sep 17 00:00:00 2001
From: Sheri Bernstein <bernstein@adacore.com>
Date: Thu, 3 Aug 2023 12:38:53 +0000
Subject: [PATCH] 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.
---
 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);
-- 
2.47.2