public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r14-3680] ada: Remove GNATcheck violations
@ 2023-09-05 11:07 Marc Poulhi?s
0 siblings, 0 replies; only message in thread
From: Marc Poulhi?s @ 2023-09-05 11:07 UTC (permalink / raw)
To: gcc-cvs
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);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-09-05 11:07 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-09-05 11:07 [gcc r14-3680] ada: Remove GNATcheck violations Marc Poulhi?s
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).