From: Yannick Moy <moy@adacore.com>
Date: Tue, 25 Apr 2017 10:08:00 +0000 (+0000)
Subject: checks.adb (Determine_Range_R): Special case type conversions from integer to float... 
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c77943ebf24f7751cff692cf83fccc4866453e5;p=gcc.git

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
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 07615147138..3c9e1ac2391 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+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
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index ece2f367c16..9bf008ba69c 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 48208444bde..394098ad7a1 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;