From: Sheri Bernstein <bernst...@adacore.com>
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
