diff options
author | Sheri Bernstein <bernstein@adacore.com> | 2023-07-25 17:16:55 +0000 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-08-03 14:07:36 +0200 |
commit | 4cd4d2733cabc293c1c03a5e4ba919464fe0d359 (patch) | |
tree | f571085e8b49200f2b80095d29f27478d28f1096 /gcc | |
parent | 65a31e22a81f94df87f8248f08a0308aa3d64431 (diff) | |
download | gcc-4cd4d2733cabc293c1c03a5e4ba919464fe0d359.zip gcc-4cd4d2733cabc293c1c03a5e4ba919464fe0d359.tar.gz gcc-4cd4d2733cabc293c1c03a5e4ba919464fe0d359.tar.bz2 |
ada: Add pragma Annotate for GNATcheck exemptions
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.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-atopri.adb | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-bitops.adb | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-carsi8.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-carun8.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-casi16.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-casi32.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-casi64.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-caun16.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-caun32.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-caun64.adb | 4 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-exponn.adb | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-expont.adb | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-valspe.adb | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-vauspe.adb | 5 |
15 files changed, 66 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 2f1fbd5..beb56bf 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 9e23fa0..5fc2a12 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 30699d7..acddd52 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 807dcee..839f157 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 b0f2d94b..b20e4e1 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 6d35d33..fa529c9 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 52acd30..7ed9ec5 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 50b6f6d..f021110 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 641cf29..43bf35b 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 2c0b772..0a5ca12 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 8a9720f..cca2069 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 d7a5342..a6b87ea 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 f6b030d..e826061 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 56e6ed7..e6d9df6 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 b2fe187..c58fb21 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; ----------------------------- |