[gcc r14-3680] ada: Remove GNATcheck violations

[Marc Poulhi?s <dkm@gcc.gnu.org>]

https://gcc.gnu.org/g:f9a68b454743fffe07fb51ed735510c2178ba14c

commit r14-3680-gf9a68b454743fffe07fb51ed735510c2178ba14c
Author: Sheri Bernstein <bernstein@adacore.com>
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);