From: Liaiss Merzougue Date: Mon, 13 Jan 2020 12:07:26 +0000 (+0100) Subject: [Ada] Codepeer remarks take into account X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0d9f29d52e134c02fafee222be655189d9050f2;p=gcc.git [Ada] Codepeer remarks take into account gcc/ada/ * libgnat/s-carsi8.adb (Compare_Array_S8): Add pragma Assert to avoid warning concerning Left_Len and RighLen value regarding Bytes_Compared_As_Words. * libgnat/s-carun8.adb (Compare_Array_U8): Likewise. * libgnat/s-geveop.adb (Binary_Operation, Unary_Operation): Add pragma Assert concerning divide by 0 warning. * libgnat/s-imgcha.adb (Image_Character): Code update to prevent constant operation warning. (Image_Character): Add pragma Assert concerning the unchecked String size. * libgnat/s-imgdec.adb (Round): Upate loop code to prevent warning concerning Digs'First access. (Round): Add pragma assert. (Set): Add pragma Assert for the unchecked string size. (Set_Digits): Add pragma Assert for the input range. (Set_Decimal_Digits): Add pragma Assert. (Set_Blank_And_Sign): Add pragma Assert for the input range. * libgnat/s-arit64.adb (DoubleDivide): Add pragma Assert concerning Du /= 0. (Multiply_With_Ovflo_Check): Add pragma Annotate to avoid warning concerning unsigned -> signed conversion. * libgnat/s-imguns.adb (Set_Image_Unsigned): Add pragma Assert to prevent overflow check warning. Add pragma Assert for controlling S'First = 1. * libgnat/s-imgrea.adb (Image_Floating_Point, Set, Set_Digs, Set_Special_Fill, Convert_Integer): Add pragma Annotate to prevent overflow check warning. (Set_Image_Real): Add pragma Annotate to avoid dead code warning on float check. Add pragma Assert to prevent overflow check warning. * libgnat/s-imgwiu.adb (Set_Digits, Set_Image_Width_Unsigned): Add pragma assert to prevent overflow check warning. * libgnat/s-imgllu.adb (Set_Image_Long_Long_Unsigned): Add pragma assert to prevent overflow check warning. * libgnat/s-imgint.adb (Set_Digits): Add Assert for input constraint and to prevent overflow check warning, create Non_Positive subtype, and change the T parameter as Non_Positive instead Integer. (Set_Image_Integer): Add pragma assert to prevent overflow check warning. * libgnat/s-imglli.adb (Set_Digits): Add Assert for input constraint and to prevent overflow check warning, create Non_Positive subtype, and change the T parameter as Non_Positive instead Integer. (Set_Image_Long_Long_Integer): Add pragma assert to prevent overflow check warning. * libgnat/s-fatgen.adb (Decompose, Pred, Succ): Add pragma Annotate to prevent dead code due to invalid float check. * libgnat/s-imenne.adb (Image_Enumeration_8, Image_Enumeration_16, Image_Enumeration_32): Add pragma Assert to prevent overflow check warning. Add Names_Index subtype for restricting Index_table content. --- diff --git a/gcc/ada/libgnat/s-arit64.adb b/gcc/ada/libgnat/s-arit64.adb index 060f352a853..937490e4bde 100644 --- a/gcc/ada/libgnat/s-arit64.adb +++ b/gcc/ada/libgnat/s-arit64.adb @@ -214,6 +214,15 @@ package body System.Arith_64 is -- Perform the actual division + pragma Assert (Du /= 0); + -- Multiplication of 2-limbs arguments Yu and Zu leads to 4-limbs + -- result (where each limb is 32bits). Cases where 4 limbs are needed + -- require Yhi/=0 and Zhi/=0 and lead to early exit. Remaining cases + -- where 3 limbs are needed correspond to Hi(T2)/=0 and lead to + -- early exit. Thus at this point result fits in 2 limbs which are + -- exactly Lo(T2) and Lo(T1), which corresponds to the value of Du. + -- As the case where one of Yu or Zu is null also led to early exit, + -- Du/=0 here. Qu := Xu / Du; Ru := Xu rem Du; @@ -305,12 +314,16 @@ package body System.Arith_64 is if X >= 0 then if Y >= 0 then return To_Pos_Int (T2); + pragma Annotate (CodePeer, Intentional, "precondition", + "Intentional Unsigned->Signed conversion"); else return To_Neg_Int (T2); end if; else -- X < 0 if Y < 0 then return To_Pos_Int (T2); + pragma Annotate (CodePeer, Intentional, "precondition", + "Intentional Unsigned->Signed conversion"); else return To_Neg_Int (T2); end if; @@ -476,6 +489,12 @@ package body System.Arith_64 is Zhi := Hi (Zu); Zlo := Lo (Zu); + pragma Assert (Zhi /= 0); + -- Hi(Zu)/=0 before normalization. The sequence of Shift_Left + -- operations results in the leading bit of Zu being 1 by moving + -- the leftmost 1-bit in Zu to leading position, thus Zhi=Hi(Zu)/=0 + -- here. + -- Note that when we scale up the dividend, it still fits in four -- digits, since we already tested for overflow, and scaling does -- not change the invariant that (D (1) & D (2)) < Zu. diff --git a/gcc/ada/libgnat/s-carsi8.adb b/gcc/ada/libgnat/s-carsi8.adb index 11ec4601cce..2da7f5a5f9f 100644 --- a/gcc/ada/libgnat/s-carsi8.adb +++ b/gcc/ada/libgnat/s-carsi8.adb @@ -97,6 +97,13 @@ package body System.Compare_Array_Signed_8 is end if; end loop; + pragma Assert (Left_Len >= Bytes_Compared_As_Words); + pragma Assert (Right_Len >= Bytes_Compared_As_Words); + -- Left_Len and Right_Len are always greater or equal to + -- Bytes_Compared_As_Words because: + -- * Compare_Len is min (Left_Len, Right_Len) + -- * Words_To_Compare = Compare_Len / 4 + -- * Bytes_Compared_As_Words = Words_To_Compare * 4 return Compare_Array_S8_Unaligned (AddA (Left, Address (Bytes_Compared_As_Words)), AddA (Right, Address (Bytes_Compared_As_Words)), diff --git a/gcc/ada/libgnat/s-carun8.adb b/gcc/ada/libgnat/s-carun8.adb index 412410e6028..0ed3d268129 100644 --- a/gcc/ada/libgnat/s-carun8.adb +++ b/gcc/ada/libgnat/s-carun8.adb @@ -98,6 +98,13 @@ package body System.Compare_Array_Unsigned_8 is end if; end loop; + pragma Assert (Left_Len >= Bytes_Compared_As_Words); + pragma Assert (Right_Len >= Bytes_Compared_As_Words); + -- Left_Len and Right_Len are always greater or equal to + -- Bytes_Compared_As_Words because: + -- * Compare_Len is min (Left_Len, Right_Len) + -- * Words_To_Compare = Compare_Len / 4 + -- * Bytes_Compared_As_Words = Words_To_Compare * 4 return Compare_Array_U8_Unaligned (AddA (Left, Address (Bytes_Compared_As_Words)), AddA (Right, Address (Bytes_Compared_As_Words)), diff --git a/gcc/ada/libgnat/s-fatgen.adb b/gcc/ada/libgnat/s-fatgen.adb index b5445874f98..a598a124390 100644 --- a/gcc/ada/libgnat/s-fatgen.adb +++ b/gcc/ada/libgnat/s-fatgen.adb @@ -172,10 +172,14 @@ package body System.Fat_Gen is elsif X > T'Safe_Last then Frac := Invrad; + pragma Annotate (CodePeer, Intentional, "dead code", + "Check float range."); Expo := T'Machine_Emax + 1; elsif X < T'Safe_First then Frac := -Invrad; + pragma Annotate (CodePeer, Intentional, "dead code", + "Check float range."); Expo := T'Machine_Emax + 2; -- how many extra negative values? else @@ -217,6 +221,8 @@ package body System.Fat_Gen is while Ax < R_Neg_Power (Expbits'Last) loop Ax := Ax * R_Power (Expbits'Last); + pragma Annotate (CodePeer, Intentional, "dead code", + "Check float range."); Ex := Ex - Log_Power (Expbits'Last); end loop; pragma Annotate @@ -424,7 +430,11 @@ package body System.Fat_Gen is -- For infinities, return unchanged elsif X < T'First or else X > T'Last then + pragma Annotate (CodePeer, Intentional, "condition predetermined", + "Check for invalid float"); return X; + pragma Annotate (CodePeer, Intentional, "dead code", + "Check float range."); -- Subtract from the given number a number equivalent to the value -- of its least significant bit. Given that the most significant bit @@ -673,7 +683,11 @@ package body System.Fat_Gen is -- For infinities, return unchanged elsif X < T'First or else X > T'Last then + pragma Annotate (CodePeer, Intentional, "condition predetermined", + "Check for invalid float"); return X; + pragma Annotate (CodePeer, Intentional, "dead code", + "Check float range."); -- Add to the given number a number equivalent to the value -- of its least significant bit. Given that the most significant bit diff --git a/gcc/ada/libgnat/s-geveop.adb b/gcc/ada/libgnat/s-geveop.adb index 8e59b30982d..ff62a344c14 100644 --- a/gcc/ada/libgnat/s-geveop.adb +++ b/gcc/ada/libgnat/s-geveop.adb @@ -66,6 +66,13 @@ package body System.Generic_Vector_Operations is function VP is new Ada.Unchecked_Conversion (Address, Vector_Ptr); function EP is new Ada.Unchecked_Conversion (Address, Element_Ptr); + pragma Assert (VI > 0); + -- VI = VU + -- VU = Vectors.Vector'Size / Storage_Unit + -- Vector'Size = System.Word_Size + -- System.Word_Size is a multiple of Storage_Unit + -- Vector'Size > Storage_Unit + -- VI > 0 SA : constant Address := AddA (XA, To_Address ((Integer_Address (Length) / VI * VI) and Unaligned)); @@ -111,6 +118,13 @@ package body System.Generic_Vector_Operations is function VP is new Ada.Unchecked_Conversion (Address, Vector_Ptr); function EP is new Ada.Unchecked_Conversion (Address, Element_Ptr); + pragma Assert (VI > 0); + -- VI = VU + -- VU = Vectors.Vector'Size / Storage_Unit + -- Vector'Size = System.Word_Size + -- System.Word_Size is a multiple of Storage_Unit + -- Vector'Size > Storage_Unit + -- VI > 0 SA : constant Address := AddA (XA, To_Address ((Integer_Address (Length) / VI * VI) and Unaligned)); diff --git a/gcc/ada/libgnat/s-imenne.adb b/gcc/ada/libgnat/s-imenne.adb index 605b85bf932..8409f6a4a48 100644 --- a/gcc/ada/libgnat/s-imenne.adb +++ b/gcc/ada/libgnat/s-imenne.adb @@ -49,8 +49,11 @@ package body System.Img_Enum_New is pragma Assert (S'First = 1); type Natural_8 is range 0 .. 2 ** 7 - 1; + subtype Names_Index is + Natural_8 range Natural_8 (Names'First) + .. Natural_8 (Names'Last) + 1; subtype Index is Natural range Natural'First .. Names'Length; - type Index_Table is array (Index) of Natural_8; + type Index_Table is array (Index) of Names_Index; type Index_Table_Ptr is access Index_Table; function To_Index_Table_Ptr is @@ -61,6 +64,13 @@ package body System.Img_Enum_New is Start : constant Natural := Natural (IndexesT (Pos)); Next : constant Natural := Natural (IndexesT (Pos + 1)); + pragma Assert (Next - 1 >= Start); + pragma Assert (Start >= Names'First); + pragma Assert (Next - 1 <= Names'Last); + + pragma Assert (Next - Start <= S'Last); + -- The caller should guarantee that S is large enough to contain the + -- enumeration image. begin S (1 .. Next - Start) := Names (Start .. Next - 1); P := Next - Start; @@ -80,8 +90,11 @@ package body System.Img_Enum_New is pragma Assert (S'First = 1); type Natural_16 is range 0 .. 2 ** 15 - 1; + subtype Names_Index is + Natural_16 range Natural_16 (Names'First) + .. Natural_16 (Names'Last) + 1; subtype Index is Natural range Natural'First .. Names'Length; - type Index_Table is array (Index) of Natural_16; + type Index_Table is array (Index) of Names_Index; type Index_Table_Ptr is access Index_Table; function To_Index_Table_Ptr is @@ -92,6 +105,13 @@ package body System.Img_Enum_New is Start : constant Natural := Natural (IndexesT (Pos)); Next : constant Natural := Natural (IndexesT (Pos + 1)); + pragma Assert (Next - 1 >= Start); + pragma Assert (Start >= Names'First); + pragma Assert (Next - 1 <= Names'Last); + + pragma Assert (Next - Start <= S'Last); + -- The caller should guarantee that S is large enough to contain the + -- enumeration image. begin S (1 .. Next - Start) := Names (Start .. Next - 1); P := Next - Start; @@ -111,8 +131,11 @@ package body System.Img_Enum_New is pragma Assert (S'First = 1); type Natural_32 is range 0 .. 2 ** 31 - 1; + subtype Names_Index is + Natural_32 range Natural_32 (Names'First) + .. Natural_32 (Names'Last) + 1; subtype Index is Natural range Natural'First .. Names'Length; - type Index_Table is array (Index) of Natural_32; + type Index_Table is array (Index) of Names_Index; type Index_Table_Ptr is access Index_Table; function To_Index_Table_Ptr is @@ -123,6 +146,13 @@ package body System.Img_Enum_New is Start : constant Natural := Natural (IndexesT (Pos)); Next : constant Natural := Natural (IndexesT (Pos + 1)); + pragma Assert (Next - 1 >= Start); + pragma Assert (Start >= Names'First); + pragma Assert (Next - 1 <= Names'Last); + + pragma Assert (Next - Start <= S'Last); + -- The caller should guarantee that S is large enough to contain the + -- enumeration image. begin S (1 .. Next - Start) := Names (Start .. Next - 1); P := Next - Start; diff --git a/gcc/ada/libgnat/s-imgcha.adb b/gcc/ada/libgnat/s-imgcha.adb index a2d7c46757b..06048eb64f1 100644 --- a/gcc/ada/libgnat/s-imgcha.adb +++ b/gcc/ada/libgnat/s-imgcha.adb @@ -140,8 +140,12 @@ package body System.Img_Char is declare VP : constant Natural := Character'Pos (V); begin - S (1 .. 9) := "RESERVED_"; - S (10) := Character'Val (48 + VP / 100); + pragma Assert (S'First = 1 and S'Last >= 12); + -- As described in the header description, this procedure + -- doesn't check the size of the string provided by the caller + -- and suppose S'First is 1. + S (1 .. 10) := "RESERVED_1"; + -- Since C1_Range is 127..159, the first character is always 1 S (11) := Character'Val (48 + (VP / 10) mod 10); S (12) := Character'Val (48 + VP mod 10); P := 12; diff --git a/gcc/ada/libgnat/s-imgdec.adb b/gcc/ada/libgnat/s-imgdec.adb index 6000d444bef..840dadbdd1f 100644 --- a/gcc/ada/libgnat/s-imgdec.adb +++ b/gcc/ada/libgnat/s-imgdec.adb @@ -72,6 +72,10 @@ package body System.Img_Dec is Aft : Natural; Exp : Natural) is + pragma Assert (NDigs >= 1); + pragma Assert (Digs'First = 1); + pragma Assert (Digs'First < Digs'Last); + Minus : constant Boolean := (Digs (Digs'First) = '-'); -- Set True if input is negative @@ -135,6 +139,10 @@ package body System.Img_Dec is procedure Round (N : Integer) is D : Character; + pragma Assert (NDigs >= 1); + pragma Assert (Digs'First = 1); + pragma Assert (Digs'First < Digs'Last); + begin -- Nothing to do if rounding past the last digit we have @@ -164,10 +172,17 @@ package body System.Img_Dec is else LD := N; + pragma Assert (LD >= 1); + -- In this case, we have N < LD and N >= FD. FD is a Natural, + -- So we can conclude, LD >= 1 ND := LD - 1; + pragma Assert (N + 1 <= Digs'Last); if Digs (N + 1) >= '5' then - for J in reverse 2 .. N loop + for J in reverse Digs'First + 1 .. Digs'First + N - 1 loop + pragma Assert (Digs (J) in '0' .. '9' | ' ' | '-'); + -- Because it is a decimal image, we can assume that + -- it can only contain these characters. D := Character'Succ (Digs (J)); if D <= '9' then @@ -196,6 +211,17 @@ package body System.Img_Dec is procedure Set (C : Character) is begin + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done as documented in the header : updating P to + -- point to the last character stored, the caller promises that the + -- buffer is large enough and no check is made for this. + -- Constraint_Error will not necessarily be raised if this + -- requirement is violated, since it is perfectly valid to compile + -- this unit with checks off. + -- + -- Due to codepeer limitation, codepeer should be used with switch: + -- -no-propagation system.img_dec.set_decimal_digits.set P := P + 1; S (P) := C; end Set; @@ -230,6 +256,9 @@ package body System.Img_Dec is procedure Set_Digits (S, E : Natural) is begin + pragma Assert (S >= Digs'First and E <= Digs'Last); + -- S and E should be in the Digs array range + -- TBC: Analysis should be completed for J in S .. E loop Set (Digs (J)); end loop; @@ -254,8 +283,10 @@ package body System.Img_Dec is if Exp > 0 then Set_Blanks_And_Sign (Fore - 1); Round (Digits_After_Point + 2); + Set (Digs (FD)); FD := FD + 1; + pragma Assert (ND >= 1); ND := ND - 1; Set ('.'); @@ -388,6 +419,9 @@ package body System.Img_Dec is else Set_Blanks_And_Sign (Fore - Digits_Before_Point); + pragma Assert (FD + Digits_Before_Point - 1 >= 0); + -- In this branch, we have Digits_Before_Point > 0. It is the + -- else of test (Digits_Before_Point <= 0) Set_Digits (FD, FD + Digits_Before_Point - 1); Set ('.'); Set_Digits (FD + Digits_Before_Point, LD); diff --git a/gcc/ada/libgnat/s-imgint.adb b/gcc/ada/libgnat/s-imgint.adb index 2b94472157c..112d62bcc4c 100644 --- a/gcc/ada/libgnat/s-imgint.adb +++ b/gcc/ada/libgnat/s-imgint.adb @@ -31,8 +31,10 @@ package body System.Img_Int is + subtype Non_Positive is Integer range Integer'First .. 0; + procedure Set_Digits - (T : Integer; + (T : Non_Positive; S : in out String; P : in out Natural); -- Set digits of absolute value of T, which is zero or negative. We work @@ -66,16 +68,26 @@ package body System.Img_Int is ---------------- procedure Set_Digits - (T : Integer; + (T : Non_Positive; S : in out String; P : in out Natural) is begin if T <= -10 then Set_Digits (T / 10, S, P); + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the Set_Image_Integer + -- specification, the caller guarantees that S is long enough to + -- hold the result. P := P + 1; S (P) := Character'Val (48 - (T rem 10)); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the Set_Image_Integer + -- specification, the caller guarantees that S is long enough to + -- hold the result. P := P + 1; S (P) := Character'Val (48 - T); end if; @@ -94,6 +106,10 @@ package body System.Img_Int is if V >= 0 then Set_Digits (-V, S, P); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := '-'; Set_Digits (V, S, P); diff --git a/gcc/ada/libgnat/s-imglli.adb b/gcc/ada/libgnat/s-imglli.adb index 4d024eef959..66332fe0fca 100644 --- a/gcc/ada/libgnat/s-imglli.adb +++ b/gcc/ada/libgnat/s-imglli.adb @@ -31,8 +31,11 @@ package body System.Img_LLI is + subtype Non_Positive is Long_Long_Integer + range Long_Long_Integer'First .. 0; + procedure Set_Digits - (T : Long_Long_Integer; + (T : Non_Positive; S : in out String; P : in out Natural); -- Set digits of absolute value of T, which is zero or negative. We work @@ -66,16 +69,26 @@ package body System.Img_LLI is ---------------- procedure Set_Digits - (T : Long_Long_Integer; + (T : Non_Positive; S : in out String; P : in out Natural) is begin if T <= -10 then Set_Digits (T / 10, S, P); + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done as documented in the Set_Image_Long_Long_Integer + -- specification: The caller guarantees that S is long enough to + -- hold the result. P := P + 1; S (P) := Character'Val (48 - (T rem 10)); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done as documented in the Set_Image_Long_Long_Integer + -- specification: The caller guarantees that S is long enough to + -- hold the result. P := P + 1; S (P) := Character'Val (48 - T); end if; @@ -93,6 +106,10 @@ package body System.Img_LLI is if V >= 0 then Set_Digits (-V, S, P); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done as documented in the specification: + -- The caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := '-'; Set_Digits (V, S, P); diff --git a/gcc/ada/libgnat/s-imgllu.adb b/gcc/ada/libgnat/s-imgllu.adb index f62a25d7be6..e2952ee0825 100644 --- a/gcc/ada/libgnat/s-imgllu.adb +++ b/gcc/ada/libgnat/s-imgllu.adb @@ -61,10 +61,18 @@ package body System.Img_LLU is begin if V >= 10 then Set_Image_Long_Long_Unsigned (V / 10, S, P); + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, the + -- caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (48 + (V rem 10)); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, the + -- caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (48 + V); end if; diff --git a/gcc/ada/libgnat/s-imgrea.adb b/gcc/ada/libgnat/s-imgrea.adb index 68b1fdc6ffd..a37e8790c49 100644 --- a/gcc/ada/libgnat/s-imgrea.adb +++ b/gcc/ada/libgnat/s-imgrea.adb @@ -99,6 +99,11 @@ package body System.Img_Real is if (not Is_Negative (V) and then V <= Long_Long_Float'Last) or else (not Long_Long_Float'Signed_Zeros and then V = -0.0) then + pragma Annotate (CodePeer, False_Positive, "condition predetermined", + "CodePeer analysis ignores NaN and Inf values"); + pragma Assert (S'Last > 1); + -- The caller is responsible for S to be large enough for all + -- Image_Floating_Point operation. S (1) := ' '; P := 1; else @@ -376,6 +381,8 @@ package body System.Img_Real is Set_Image_Unsigned (Unsigned (Long_Long_Float'Truncation (X)), Digs, Ndigs); + pragma Annotate (CodePeer, False_Positive, "overflow check", + "The X integer part fits in unsigned"); -- But if we want more digits than fit in Unsigned, we have to use -- the Long_Long_Unsigned routine after all. @@ -394,6 +401,12 @@ package body System.Img_Real is procedure Set (C : Character) is begin + pragma Assert (P in S'First - 1 .. S'Last - 1); + -- No check is done as documented in the header: updating P to point + -- to the last character stored, the caller promises that the buffer + -- is large enough and no check is made for this. Constraint_Error + -- will not necessarily be raised if this requirement is violated, + -- since it is perfectly valid to compile this unit with checks off. P := P + 1; S (P) := C; end Set; @@ -424,6 +437,8 @@ package body System.Img_Real is procedure Set_Digs (S, E : Natural) is begin + pragma Assert (S >= Digs'First and E <= Digs'Last); + -- S and E should be in the Digs array range for J in S .. E loop Set (Digs (J)); end loop; @@ -437,9 +452,13 @@ package body System.Img_Real is F : Natural; begin + pragma Assert ((Fore + Aft - N + 1) in Natural); + -- Fore + Aft - N + 1 should be in the Natural range F := Fore + 1 + Aft - N; if Exp /= 0 then + pragma Assert (F + Exp + 1 <= Natural'Last); + -- F + Exp + 1 should be in the Natural range F := F + Exp + 1; end if; @@ -487,24 +506,23 @@ package body System.Img_Real is -- an infinite value, so we print Inf. if V > Long_Long_Float'Last then - pragma Annotate - (CodePeer, Intentional, "test always true", "test for infinity"); - + pragma Annotate (CodePeer, False_Positive, "dead code", + "CodePeer analysis ignores NaN and Inf values"); Set ('+'); Set ('I'); Set ('n'); Set ('f'); Set_Special_Fill (4); - -- In all other cases we print NaN elsif V < Long_Long_Float'First then Set ('-'); + pragma Annotate (CodePeer, False_Positive, "dead code", + "CodePeer analysis ignores NaN and Inf values"); Set ('I'); Set ('n'); Set ('f'); Set_Special_Fill (4); - else Set ('N'); Set ('a'); @@ -597,6 +615,7 @@ package body System.Img_Real is for J in 1 .. Scale + NF loop Ndigs := Ndigs + 1; + pragma Assert (Ndigs <= Digs'Last); Digs (Ndigs) := '0'; end loop; @@ -663,6 +682,7 @@ package body System.Img_Real is for J in 1 .. NFrac - Maxdigs + 1 loop Ndigs := Ndigs + 1; + pragma Assert (Ndigs <= Digs'Last); Digs (Ndigs) := '0'; Scale := Scale - 1; end loop; diff --git a/gcc/ada/libgnat/s-imguns.adb b/gcc/ada/libgnat/s-imguns.adb index 914121dda6d..02195e3c3d3 100644 --- a/gcc/ada/libgnat/s-imguns.adb +++ b/gcc/ada/libgnat/s-imguns.adb @@ -58,13 +58,21 @@ package body System.Img_Uns is S : in out String; P : in out Natural) is + pragma Assert (S'First = 1); begin if V >= 10 then Set_Image_Unsigned (V / 10, S, P); + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (48 + (V rem 10)); - else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (48 + V); end if; diff --git a/gcc/ada/libgnat/s-imgwiu.adb b/gcc/ada/libgnat/s-imgwiu.adb index 90a8f413aa5..9ac9621e99c 100644 --- a/gcc/ada/libgnat/s-imgwiu.adb +++ b/gcc/ada/libgnat/s-imgwiu.adb @@ -102,9 +102,17 @@ package body System.Img_WIU is begin if T >= 10 then Set_Digits (T / 10); + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (T mod 10 + Character'Pos ('0')); else + pragma Assert (P >= (S'First - 1) and P < S'Last and + P < Natural'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. P := P + 1; S (P) := Character'Val (T + Character'Pos ('0')); end if; @@ -123,12 +131,19 @@ package body System.Img_WIU is T := P; while F > Start loop + pragma Assert (T >= S'First and T <= S'Last and + F >= S'First and F <= S'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. S (T) := S (F); T := T - 1; F := F - 1; end loop; for J in Start + 1 .. T loop + pragma Assert (J >= S'First and J <= S'Last); + -- No check is done since, as documented in the specification, + -- the caller guarantees that S is long enough to hold the result. S (J) := ' '; end loop; end if;