* [COMMITTED] ada: Add pragma Annotate for GNATcheck exemptions
@ 2023-08-03 12:09 Marc Poulhiès
0 siblings, 0 replies; 2+ messages in thread
From: Marc Poulhiès @ 2023-08-03 12:09 UTC (permalink / raw)
To: gcc-patches; +Cc: Sheri Bernstein
From: Sheri Bernstein <bernstein@adacore.com>
Exempt the GNATcheck rule "Improper_Returns" with the rationale
"early returns for performance".
gcc/ada/
* libgnat/s-aridou.adb: Add pragma to exempt Improper_Returns.
* libgnat/s-atopri.adb (Lock_Free_Try_Write): Likewise.
* libgnat/s-bitops.adb (Bit_Eq): Likewise.
* libgnat/s-carsi8.adb: Likewise.
* libgnat/s-carun8.adb: Likewise.
* libgnat/s-casi16.adb: Likewise.
* libgnat/s-casi32.adb: Likewise.
* libgnat/s-casi64.adb: Likewise.
* libgnat/s-caun16.adb: Likewise.
* libgnat/s-caun32.adb: Likewise.
* libgnat/s-caun64.adb: Likewise.
* libgnat/s-exponn.adb: Likewise.
* libgnat/s-expont.adb: Likewise.
* libgnat/s-valspe.adb: Likewise.
* libgnat/s-vauspe.adb: Likewise.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/s-aridou.adb | 4 ++++
gcc/ada/libgnat/s-atopri.adb | 5 +++++
gcc/ada/libgnat/s-bitops.adb | 5 +++++
gcc/ada/libgnat/s-carsi8.adb | 4 ++++
gcc/ada/libgnat/s-carun8.adb | 4 ++++
gcc/ada/libgnat/s-casi16.adb | 4 ++++
gcc/ada/libgnat/s-casi32.adb | 4 ++++
gcc/ada/libgnat/s-casi64.adb | 4 ++++
gcc/ada/libgnat/s-caun16.adb | 4 ++++
gcc/ada/libgnat/s-caun32.adb | 4 ++++
gcc/ada/libgnat/s-caun64.adb | 4 ++++
gcc/ada/libgnat/s-exponn.adb | 5 +++++
gcc/ada/libgnat/s-expont.adb | 5 +++++
gcc/ada/libgnat/s-valspe.adb | 5 +++++
gcc/ada/libgnat/s-vauspe.adb | 5 +++++
15 files changed, 66 insertions(+)
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 2f1fbd55453..beb56bfabe1 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -90,6 +90,9 @@ is
(On, "non-preelaborable call not allowed in preelaborated unit");
pragma Warnings (On, "non-static constant in preelaborated unit");
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
-----------------------
-- Local Subprograms --
-----------------------
@@ -3653,4 +3656,5 @@ is
end if;
end To_Pos_Int;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Arith_Double;
diff --git a/gcc/ada/libgnat/s-atopri.adb b/gcc/ada/libgnat/s-atopri.adb
index 9e23fa0ac91..5fc2a123a71 100644
--- a/gcc/ada/libgnat/s-atopri.adb
+++ b/gcc/ada/libgnat/s-atopri.adb
@@ -59,6 +59,9 @@ package body System.Atomic_Primitives is
new Atomic_Compare_Exchange (Atomic_Type);
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
if Expected /= Desired then
if Atomic_Type'Atomic_Always_Lock_Free then
return My_Atomic_Compare_Exchange (Ptr, Expected'Address, Desired);
@@ -68,6 +71,8 @@ package body System.Atomic_Primitives is
end if;
return True;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Lock_Free_Try_Write;
end System.Atomic_Primitives;
diff --git a/gcc/ada/libgnat/s-bitops.adb b/gcc/ada/libgnat/s-bitops.adb
index 30699d73175..acddd52892c 100644
--- a/gcc/ada/libgnat/s-bitops.adb
+++ b/gcc/ada/libgnat/s-bitops.adb
@@ -112,6 +112,9 @@ package body System.Bit_Ops is
RightB : constant Bits := To_Bits (Right);
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
if Llen /= Rlen then
return False;
@@ -134,6 +137,8 @@ package body System.Bit_Ops is
end if;
end;
end if;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Bit_Eq;
-------------
diff --git a/gcc/ada/libgnat/s-carsi8.adb b/gcc/ada/libgnat/s-carsi8.adb
index 807dceefc58..839f157a2ee 100644
--- a/gcc/ada/libgnat/s-carsi8.adb
+++ b/gcc/ada/libgnat/s-carsi8.adb
@@ -58,6 +58,9 @@ package body System.Compare_Array_Signed_8 is
function To_Big_Bytes is new
Ada.Unchecked_Conversion (System.Address, Big_Bytes_Ptr);
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
----------------------
-- Compare_Array_S8 --
----------------------
@@ -147,4 +150,5 @@ package body System.Compare_Array_Signed_8 is
end if;
end Compare_Array_S8_Unaligned;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Signed_8;
diff --git a/gcc/ada/libgnat/s-carun8.adb b/gcc/ada/libgnat/s-carun8.adb
index b0f2d94bf8a..b20e4e1b922 100644
--- a/gcc/ada/libgnat/s-carun8.adb
+++ b/gcc/ada/libgnat/s-carun8.adb
@@ -57,6 +57,9 @@ package body System.Compare_Array_Unsigned_8 is
function To_Big_Bytes is new
Ada.Unchecked_Conversion (System.Address, Big_Bytes_Ptr);
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
----------------------
-- Compare_Array_U8 --
----------------------
@@ -146,4 +149,5 @@ package body System.Compare_Array_Unsigned_8 is
end if;
end Compare_Array_U8_Unaligned;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Unsigned_8;
diff --git a/gcc/ada/libgnat/s-casi16.adb b/gcc/ada/libgnat/s-casi16.adb
index 6d35d33b9d7..fa529c9d559 100644
--- a/gcc/ada/libgnat/s-casi16.adb
+++ b/gcc/ada/libgnat/s-casi16.adb
@@ -58,6 +58,9 @@ package body System.Compare_Array_Signed_16 is
-- Compare_Array_S16 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_S16
(Left : System.Address;
Right : System.Address;
@@ -130,4 +133,5 @@ package body System.Compare_Array_Signed_16 is
end if;
end Compare_Array_S16;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Signed_16;
diff --git a/gcc/ada/libgnat/s-casi32.adb b/gcc/ada/libgnat/s-casi32.adb
index 52acd30794a..7ed9ec5c519 100644
--- a/gcc/ada/libgnat/s-casi32.adb
+++ b/gcc/ada/libgnat/s-casi32.adb
@@ -53,6 +53,9 @@ package body System.Compare_Array_Signed_32 is
-- Compare_Array_S32 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_S32
(Left : System.Address;
Right : System.Address;
@@ -113,4 +116,5 @@ package body System.Compare_Array_Signed_32 is
end if;
end Compare_Array_S32;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Signed_32;
diff --git a/gcc/ada/libgnat/s-casi64.adb b/gcc/ada/libgnat/s-casi64.adb
index 50b6f6d1cf9..f0211107baf 100644
--- a/gcc/ada/libgnat/s-casi64.adb
+++ b/gcc/ada/libgnat/s-casi64.adb
@@ -53,6 +53,9 @@ package body System.Compare_Array_Signed_64 is
-- Compare_Array_S64 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_S64
(Left : System.Address;
Right : System.Address;
@@ -113,4 +116,5 @@ package body System.Compare_Array_Signed_64 is
end if;
end Compare_Array_S64;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Signed_64;
diff --git a/gcc/ada/libgnat/s-caun16.adb b/gcc/ada/libgnat/s-caun16.adb
index 641cf292e71..43bf35b907a 100644
--- a/gcc/ada/libgnat/s-caun16.adb
+++ b/gcc/ada/libgnat/s-caun16.adb
@@ -58,6 +58,9 @@ package body System.Compare_Array_Unsigned_16 is
-- Compare_Array_U16 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_U16
(Left : System.Address;
Right : System.Address;
@@ -130,4 +133,5 @@ package body System.Compare_Array_Unsigned_16 is
end if;
end Compare_Array_U16;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Unsigned_16;
diff --git a/gcc/ada/libgnat/s-caun32.adb b/gcc/ada/libgnat/s-caun32.adb
index 2c0b7721297..0a5ca12144e 100644
--- a/gcc/ada/libgnat/s-caun32.adb
+++ b/gcc/ada/libgnat/s-caun32.adb
@@ -53,6 +53,9 @@ package body System.Compare_Array_Unsigned_32 is
-- Compare_Array_U32 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_U32
(Left : System.Address;
Right : System.Address;
@@ -113,4 +116,5 @@ package body System.Compare_Array_Unsigned_32 is
end if;
end Compare_Array_U32;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Unsigned_32;
diff --git a/gcc/ada/libgnat/s-caun64.adb b/gcc/ada/libgnat/s-caun64.adb
index 8a9720ffcb6..cca2069a62b 100644
--- a/gcc/ada/libgnat/s-caun64.adb
+++ b/gcc/ada/libgnat/s-caun64.adb
@@ -52,6 +52,9 @@ package body System.Compare_Array_Unsigned_64 is
-- Compare_Array_U64 --
-----------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
function Compare_Array_U64
(Left : System.Address;
Right : System.Address;
@@ -112,4 +115,5 @@ package body System.Compare_Array_Unsigned_64 is
end if;
end Compare_Array_U64;
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end System.Compare_Array_Unsigned_64;
diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb
index d7a5342b82a..a6b87eadd15 100644
--- a/gcc/ada/libgnat/s-exponn.adb
+++ b/gcc/ada/libgnat/s-exponn.adb
@@ -108,6 +108,9 @@ is
-- Ghost variable to hold Factor**Exp between Exp and Factor updates
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
-- We use the standard logarithmic approach, Exp gets shifted right
-- testing successive low order bits and Factor is the value of the
-- base raised to the next power of 2.
@@ -173,6 +176,8 @@ is
pragma Assert (Big (Result) = Big (Left) ** Right);
return Result;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Expon;
----------------------
diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb
index f6b030de50c..e8260610d58 100644
--- a/gcc/ada/libgnat/s-expont.adb
+++ b/gcc/ada/libgnat/s-expont.adb
@@ -108,6 +108,9 @@ is
-- Ghost variable to hold Factor**Exp between Exp and Factor updates
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "early returns for performance");
+
-- We use the standard logarithmic approach, Exp gets shifted right
-- testing successive low order bits and Factor is the value of the
-- base raised to the next power of 2.
@@ -173,6 +176,8 @@ is
pragma Assert (Big (Result) = Big (Left) ** Right);
return Result;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Expon;
----------------------
diff --git a/gcc/ada/libgnat/s-valspe.adb b/gcc/ada/libgnat/s-valspe.adb
index 56e6ed77209..e6d9df69bb7 100644
--- a/gcc/ada/libgnat/s-valspe.adb
+++ b/gcc/ada/libgnat/s-valspe.adb
@@ -67,6 +67,9 @@ is
function Last_Number_Ghost (Str : String) return Positive is
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "occurs in ghost code, not executable");
+
for J in Str'Range loop
if Str (J) not in '0' .. '9' | '_' then
return J - 1;
@@ -77,6 +80,8 @@ is
end loop;
return Str'Last;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Last_Number_Ghost;
end System.Val_Spec;
diff --git a/gcc/ada/libgnat/s-vauspe.adb b/gcc/ada/libgnat/s-vauspe.adb
index b2fe1870b86..c58fb218999 100644
--- a/gcc/ada/libgnat/s-vauspe.adb
+++ b/gcc/ada/libgnat/s-vauspe.adb
@@ -56,6 +56,9 @@ package body System.Value_U_Spec with SPARK_Mode is
function Last_Hexa_Ghost (Str : String) return Positive is
begin
+ pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+ "occurs in ghost code, not executable");
+
for J in Str'Range loop
if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
return J - 1;
@@ -67,6 +70,8 @@ package body System.Value_U_Spec with SPARK_Mode is
end loop;
return Str'Last;
+
+ pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
end Last_Hexa_Ghost;
-----------------------------
--
2.40.0
^ permalink raw reply [flat|nested] 2+ messages in thread
* [COMMITTED] ada: Add pragma Annotate for GNATcheck exemptions
@ 2023-10-19 14:41 Marc Poulhiès
0 siblings, 0 replies; 2+ messages in thread
From: Marc Poulhiès @ 2023-10-19 14:41 UTC (permalink / raw)
To: gcc-patches; +Cc: Sheri Bernstein
From: Sheri Bernstein <bernstein@adacore.com>
Exempt the GNATcheck rule "Unassigned_OUT_Parameters"
with the rationale "the OUT parameter is assigned by component".
gcc/ada/
* libgnat/s-imguti.adb (Set_Decimal_Digits): Add pragma to exempt
Unassigned_OUT_Parameters.
(Set_Floating_Invalid_Value): Likewise
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/s-imguti.adb | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/gcc/ada/libgnat/s-imguti.adb b/gcc/ada/libgnat/s-imguti.adb
index 4b9e27a7d8f..cb081108950 100644
--- a/gcc/ada/libgnat/s-imguti.adb
+++ b/gcc/ada/libgnat/s-imguti.adb
@@ -37,6 +37,8 @@ package body System.Img_Util is
-- Set_Decimal_Digits --
------------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Unassigned_OUT_Parameters",
+ "the OUT parameter is assigned by component");
procedure Set_Decimal_Digits
(Digs : in out String;
NDigs : Natural;
@@ -47,6 +49,8 @@ package body System.Img_Util is
Aft : Natural;
Exp : Natural)
is
+ pragma Annotate (Gnatcheck, Exempt_Off, "Unassigned_OUT_Parameters");
+
pragma Assert (NDigs >= 1);
pragma Assert (Digs'First = 1);
pragma Assert (Digs'First < Digs'Last);
@@ -413,6 +417,8 @@ package body System.Img_Util is
-- Set_Floating_Invalid_Value --
--------------------------------
+ pragma Annotate (Gnatcheck, Exempt_On, "Unassigned_OUT_Parameters",
+ "the OUT parameter is assigned by component");
procedure Set_Floating_Invalid_Value
(V : Floating_Invalid_Value;
S : out String;
@@ -421,6 +427,8 @@ package body System.Img_Util is
Aft : Natural;
Exp : Natural)
is
+ pragma Annotate (Gnatcheck, Exempt_Off, "Unassigned_OUT_Parameters");
+
procedure Set (C : Character);
-- Sets character C in output buffer
--
2.42.0
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2023-10-19 14:42 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-08-03 12:09 [COMMITTED] ada: Add pragma Annotate for GNATcheck exemptions Marc Poulhiès
2023-10-19 14:41 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).