[Ada] Add more annotations and assertions in the runtime
authorArnaud Charlet <charlet@adacore.com>
Thu, 3 Sep 2020 09:33:39 +0000 (05:33 -0400)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 22 Oct 2020 12:11:27 +0000 (08:11 -0400)
gcc/ada/

* libgnat/s-imenne.adb, libgnat/s-imgrea.adb: Add assertions.

gcc/ada/libgnat/s-imenne.adb
gcc/ada/libgnat/s-imgrea.adb

index 8409f6a4a4811efb0dc59483c620e44c7112184d..3052ea23ffc32caeaf15ed8e72c14648c0cc6eb7 100644 (file)
@@ -61,6 +61,9 @@ package body System.Img_Enum_New is
 
       IndexesT : constant Index_Table_Ptr := To_Index_Table_Ptr (Indexes);
 
+      pragma Assert (Pos in IndexesT'Range);
+      pragma Assert (Pos + 1 in IndexesT'Range);
+
       Start : constant Natural := Natural (IndexesT (Pos));
       Next  : constant Natural := Natural (IndexesT (Pos + 1));
 
@@ -102,6 +105,9 @@ package body System.Img_Enum_New is
 
       IndexesT : constant Index_Table_Ptr := To_Index_Table_Ptr (Indexes);
 
+      pragma Assert (Pos in IndexesT'Range);
+      pragma Assert (Pos + 1 in IndexesT'Range);
+
       Start : constant Natural := Natural (IndexesT (Pos));
       Next  : constant Natural := Natural (IndexesT (Pos + 1));
 
@@ -143,6 +149,9 @@ package body System.Img_Enum_New is
 
       IndexesT : constant Index_Table_Ptr := To_Index_Table_Ptr (Indexes);
 
+      pragma Assert (Pos in IndexesT'Range);
+      pragma Assert (Pos + 1 in IndexesT'Range);
+
       Start : constant Natural := Natural (IndexesT (Pos));
       Next  : constant Natural := Natural (IndexesT (Pos + 1));
 
index 244b79c1c194d88e6bc5dae936daca3465bce22c..45d0ae59b7bf11d2b1d95be460475d8c7d49208c 100644 (file)
@@ -376,17 +376,20 @@ package body System.Img_Real is
          --  be significantly more efficient than the Long_Long_Unsigned one.
 
          if X < Powten (Unsdigs) then
+            pragma Assert (X in 0.0 .. Long_Long_Float (Unsigned'Last));
             Ndigs := 0;
             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.
 
          else
+            pragma Assert (X < Powten (Maxdigs));
+            pragma Assert
+              (X in 0.0 .. Long_Long_Float (Long_Long_Unsigned'Last));
+
             Ndigs := 0;
             Set_Image_Long_Long_Unsigned
               (Long_Long_Unsigned (Long_Long_Float'Truncation (X)),