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.
This commit is contained in:
parent
65a31e22a8
commit
4cd4d2733c
15 changed files with 66 additions and 0 deletions
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
||||
-------------
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
||||
----------------------
|
||||
|
|
|
@ -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;
|
||||
|
||||
----------------------
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
||||
-----------------------------
|
||||
|
|
Loading…
Add table
Reference in a new issue