[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.

14 files changed, 229 insertions, 16 deletions

diff --git a/gcc/ada/libgnat/s-arit64.adb b/gcc/ada/libgnat/s-arit64.adb
index 060f352..937490e 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 11ec460..2da7f5a 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 412410e..0ed3d26 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 b544587..a598a12 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 8e59b30..ff62a34 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 605b85b..8409f6a 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 a2d7c46..06048eb 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 6000d44..840dadb 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 2b94472..112d62b 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 4d024ee..66332fe 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 f62a25d..e2952ee 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 68b1fdc..a37e879 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 914121d..02195e3 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 90a8f41..9ac9621 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;