diff options
| author | Arnaud Charlet <charlet@adacore.com> | 2020-09-03 05:33:39 -0400 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-10-22 08:11:27 -0400 |
| commit | d4194d74faee24c9bded05ba1b523e52f8b40bf0 (patch) | |
| tree | 04497543315e76fda4e387202a90b5943503acfd /gcc/ada | |
| parent | 41a52050498ea809c7175e2a3ce682324d2a966c (diff) | |
| download | gcc-d4194d74faee24c9bded05ba1b523e52f8b40bf0.zip gcc-d4194d74faee24c9bded05ba1b523e52f8b40bf0.tar.gz gcc-d4194d74faee24c9bded05ba1b523e52f8b40bf0.tar.bz2 | |
[Ada] Add more annotations and assertions in the runtime
gcc/ada/
* libgnat/s-imenne.adb, libgnat/s-imgrea.adb: Add assertions.
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/libgnat/s-imenne.adb | 9 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-imgrea.adb | 7 |
2 files changed, 14 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/s-imenne.adb b/gcc/ada/libgnat/s-imenne.adb index 8409f6a..3052ea2 100644 --- a/gcc/ada/libgnat/s-imenne.adb +++ b/gcc/ada/libgnat/s-imenne.adb @@ -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)); diff --git a/gcc/ada/libgnat/s-imgrea.adb b/gcc/ada/libgnat/s-imgrea.adb index 244b79c..45d0ae5 100644 --- a/gcc/ada/libgnat/s-imgrea.adb +++ b/gcc/ada/libgnat/s-imgrea.adb @@ -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)), |