diff options
| author | Sheri Bernstein <bernstein@adacore.com> | 2023-08-03 12:38:53 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-09-05 13:05:12 +0200 |
| commit | f9a68b454743fffe07fb51ed735510c2178ba14c (patch) | |
| tree | 6b173771600c10ae81c9e30cbde41e7ff7923d2d /gcc | |
| parent | 17fcc7df64b5b6574e8dd24095a0f146382e62c3 (diff) | |
| download | gcc-f9a68b454743fffe07fb51ed735510c2178ba14c.zip gcc-f9a68b454743fffe07fb51ed735510c2178ba14c.tar.gz gcc-f9a68b454743fffe07fb51ed735510c2178ba14c.tar.bz2 | |
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-vauspe.ads | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index beb56bf..6bcce59 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 a6f81d7..b276eed 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); |