-- 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;
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;
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.
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)),
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)),
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
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
-- 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
-- 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
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));
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));
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
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;
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
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;
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
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;
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;
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
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
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
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;
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;
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 ('.');
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);
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
----------------
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;
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);
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
----------------
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;
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);
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;
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
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.
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;
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;
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;
-- 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');
for J in 1 .. Scale + NF loop
Ndigs := Ndigs + 1;
+ pragma Assert (Ndigs <= Digs'Last);
Digs (Ndigs) := '0';
end loop;
for J in 1 .. NFrac - Maxdigs + 1 loop
Ndigs := Ndigs + 1;
+ pragma Assert (Ndigs <= Digs'Last);
Digs (Ndigs) := '0';
Scale := Scale - 1;
end loop;
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;
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;
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;
projects / gcc.git / commitdiff