From 3c77943ebf24f7751cff692cf83fccc4866453e5 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 25 Apr 2017 10:08:00 +0000 Subject: [PATCH] checks.adb (Determine_Range_R): Special case type conversions from integer to float in order to get bounds in... 2017-04-25 Yannick Moy * checks.adb (Determine_Range_R): Special case type conversions from integer to float in order to get bounds in that case too. * eval_fat.adb (Machine): Avoid issuing warnings in GNATprove mode, for computations involved in interval checking. From-SVN: r247172 --- gcc/ada/ChangeLog | 7 +++++++ gcc/ada/checks.adb | 30 ++++++++++++++++++++++++++---- gcc/ada/eval_fat.adb | 29 ++++++++++++++++++++++------- 3 files changed, 55 insertions(+), 11 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0761514..3c9e1ac 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2017-04-25 Yannick Moy + + * checks.adb (Determine_Range_R): Special case type conversions + from integer to float in order to get bounds in that case too. + * eval_fat.adb (Machine): Avoid issuing warnings in GNATprove + mode, for computations involved in interval checking. + 2017-04-25 Hristian Kirtchev * checks.adb (Insert_Valid_Check): Partially reimplement validity diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index ece2f36..9bf008b 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -5119,11 +5119,33 @@ package body Checks is end if; end if; - -- For type conversion from one floating-point type to another, we - -- can refine the range using the converted value. - when N_Type_Conversion => - Determine_Range_R (Expression (N), OK1, Lor, Hir, Assume_Valid); + + -- For type conversion from one floating-point type to another, we + -- can refine the range using the converted value. + + if Is_Floating_Point_Type (Etype (Expression (N))) then + Determine_Range_R (Expression (N), OK1, Lor, Hir, Assume_Valid); + + -- When converting an integer to a floating-point type, determine + -- the range in integer first, and then convert the bounds. + + elsif Is_Discrete_Type (Etype (Expression (N))) then + declare + Lor_Int, Hir_Int : Uint; + begin + Determine_Range (Expression (N), OK1, Lor_Int, Hir_Int, + Assume_Valid); + + if OK1 then + Lor := Round_Machine (UR_From_Uint (Lor_Int)); + Hir := Round_Machine (UR_From_Uint (Hir_Int)); + end if; + end; + + else + OK1 := False; + end if; -- Nothing special to do for all other expression kinds diff --git a/gcc/ada/eval_fat.adb b/gcc/ada/eval_fat.adb index 4820844..394098a 100644 --- a/gcc/ada/eval_fat.adb +++ b/gcc/ada/eval_fat.adb @@ -25,6 +25,7 @@ with Einfo; use Einfo; with Errout; use Errout; +with Opt; use Opt; with Sem_Util; use Sem_Util; package body Eval_Fat is @@ -505,15 +506,23 @@ package body Eval_Fat is Emin_Den : constant UI := Machine_Emin_Value (RT) - Machine_Mantissa_Value (RT) + Uint_1; begin + -- Do not issue warnings about underflows in GNATprove mode, + -- as calling Machine as part of interval checking may lead + -- to spurious warnings. + if X_Exp < Emin_Den or not Has_Denormals (RT) then if Has_Signed_Zeros (RT) and then UR_Is_Negative (X) then - Error_Msg_N - ("floating-point value underflows to -0.0??", Enode); + if not GNATprove_Mode then + Error_Msg_N + ("floating-point value underflows to -0.0??", Enode); + end if; return Ureal_M_0; else - Error_Msg_N - ("floating-point value underflows to 0.0??", Enode); + if not GNATprove_Mode then + Error_Msg_N + ("floating-point value underflows to 0.0??", Enode); + end if; return Ureal_0; end if; @@ -543,10 +552,16 @@ package body Eval_Fat is UR_Is_Negative (X)); begin + -- Do not issue warnings about loss of precision in + -- GNATprove mode, as calling Machine as part of + -- interval checking may lead to spurious warnings. + if X_Frac_Denorm /= X_Frac then - Error_Msg_N - ("gradual underflow causes loss of precision??", - Enode); + if not GNATprove_Mode then + Error_Msg_N + ("gradual underflow causes loss of precision??", + Enode); + end if; X_Frac := X_Frac_Denorm; end if; end; -- 2.7.4