Function Determine_Range_R is used in GNATprove to compute the maximal
bounds of floating-point expressions. This computation now also deals
with type conversion expressions, for conversions from integer to float.
This allows to prove more checks (range and overflow) in GNATprove with
a simple interval analysis rather than with calling provers.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-04-25 Yannick Moy <m...@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.
Index: checks.adb
===================================================================
--- checks.adb (revision 247170)
+++ checks.adb (working copy)
@@ -5119,12 +5119,34 @@
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
when others =>
Index: eval_fat.adb
===================================================================
--- eval_fat.adb (revision 247135)
+++ eval_fat.adb (working copy)
@@ -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 @@
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 @@
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;
