From d4194d74faee24c9bded05ba1b523e52f8b40bf0 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 3 Sep 2020 05:33:39 -0400 Subject: [PATCH] [Ada] Add more annotations and assertions in the runtime gcc/ada/ * libgnat/s-imenne.adb, libgnat/s-imgrea.adb: Add assertions. --- gcc/ada/libgnat/s-imenne.adb | 9 +++++++++ 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 8409f6a4a48..3052ea23ffc 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 244b79c1c19..45d0ae59b7b 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)), -- 2.30.2