procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[Ada] Add more annotations and assertions in the runtime

Browse source 
gcc/ada/

	* libgnat/s-imenne.adb, libgnat/s-imgrea.adb: Add assertions.
This commit is contained in:
Arnaud Charlet 2020-09-03 05:33:39 -04:00 • committed by Pierre-Marie de Rodat
parent 41a5205049
commit d4194d74fa
2 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
gcc/ada/libgnat/s-imenne.adb
View 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));

7
gcc/ada/libgnat/s-imgrea.adb
View 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)),