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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@247172 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 26 insertions, 4 deletions

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