checks.adb (Determine_Range_R): Special case type conversions from integer to…

checks.adb (Determine_Range_R): Special case type conversions from integer to float in order to get bounds in...

2017-04-25  Yannick Moy  <moy@adacore.com>

	* 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

+2017-04-25  Yannick Moy  <moy@adacore.com>
+
+	* 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  <kirtchev@adacore.com>
 
 	* checks.adb (Insert_Valid_Check): Partially reimplement validity

gcc/ada/checks.adb

@@ -5119,12 +5119,34 @@ package body Checks is
                end if;
             end if;
 
+         when N_Type_Conversion =>
+
             --  For type conversion from one floating-point type to another, we
             --  can refine the range using the converted value.
 
-         when N_Type_Conversion =>
+            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
 
          when others =>

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
+                  if not GNATprove_Mode then
                      Error_Msg_N
                        ("floating-point value underflows to -0.0??", Enode);
+                  end if;
                   return Ureal_M_0;
 
                else
+                  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
+                     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;