+2017-04-25 Yannick Moy <moy@adacore.com>
+
+ * checks.adb (Apply_Scalar_Range_Check): Analyze precisely
+ conversions from float to integer in GNATprove mode.
+ (Apply_Type_Conversion_Checks): Make sure in GNATprove mode
+ to call Apply_Type_Conversion_Checks, so that range checks
+ are properly positioned when needed on conversions, including
+ when converting from float to integer. (Determine_Range): In
+ GNATprove mode, take into account the possibility of conversion
+ from float to integer.
+ * sem_res.adb (Resolve_Type_Conversion): Only enforce range
+ check on conversions from fixed-point to integer, not anymore
+ on conversions from floating-point to integer, when in GNATprove
+ mode.
+
2017-04-25 Yannick Moy <moy@adacore.com>
* checks.adb (Determine_Range_R): Special case type conversions
-- The additional less-precise tests below catch these cases
+ -- In GNATprove_Mode, also deal with the case of a conversion from
+ -- floating-point to integer. It is only possible because analysis
+ -- in GNATprove rules out the possibility of a NaN or infinite value.
+
-- Note: skip this if we are given a source_typ, since the point of
-- supplying a Source_Typ is to stop us looking at the expression.
-- We could sharpen this test to be out parameters only ???
if Is_Discrete_Type (Target_Typ)
- and then Is_Discrete_Type (Etype (Expr))
+ and then (Is_Discrete_Type (Etype (Expr))
+ or else (GNATprove_Mode
+ and then Is_Floating_Point_Type (Etype (Expr))))
and then not Is_Unconstrained_Subscr_Ref
and then No (Source_Typ)
then
declare
Tlo : constant Node_Id := Type_Low_Bound (Target_Typ);
Thi : constant Node_Id := Type_High_Bound (Target_Typ);
- Lo : Uint;
- Hi : Uint;
begin
if Compile_Time_Known_Value (Tlo)
declare
Lov : constant Uint := Expr_Value (Tlo);
Hiv : constant Uint := Expr_Value (Thi);
+ Lo : Uint;
+ Hi : Uint;
begin
-- If range is null, we for sure have a constraint error
-- Otherwise determine range of value
- Determine_Range (Expr, OK, Lo, Hi, Assume_Valid => True);
+ if Is_Discrete_Type (Etype (Expr)) then
+ Determine_Range (Expr, OK, Lo, Hi,
+ Assume_Valid => True);
+
+ -- When converting a float to an integer type, determine the
+ -- range in real first, and then convert the bounds using
+ -- UR_To_Uint which correctly rounds away from zero when
+ -- half way between two integers, as required by normal
+ -- Ada 95 rounding semantics. It is only possible because
+ -- analysis in GNATprove rules out the possibility of a NaN
+ -- or infinite value.
+
+ elsif GNATprove_Mode
+ and then Is_Floating_Point_Type (Etype (Expr))
+ then
+ declare
+ Lor : Ureal;
+ Hir : Ureal;
+ begin
+ Determine_Range_R (Expr, OK, Lor, Hir,
+ Assume_Valid => True);
+
+ if OK then
+ Lo := UR_To_Uint (Lor);
+ Hi := UR_To_Uint (Hir);
+ end if;
+ end;
+ end if;
if OK then
if not Range_Checks_Suppressed (Target_Type)
and then not Range_Checks_Suppressed (Expr_Type)
then
- if Float_To_Int then
+ if Float_To_Int
+ and then not GNATprove_Mode
+ then
Apply_Float_Conversion_Check (Expr, Target_Type);
else
Apply_Scalar_Range_Check
end case;
- -- For type conversion from one discrete type to another, we can
- -- refine the range using the converted value.
-
when N_Type_Conversion =>
- Determine_Range (Expression (N), OK1, Lor, Hir, Assume_Valid);
+
+ -- For type conversion from one discrete type to another, we can
+ -- refine the range using the converted value.
+
+ if Is_Discrete_Type (Etype (Expression (N))) then
+ Determine_Range (Expression (N), OK1, Lor, Hir, Assume_Valid);
+
+ -- When converting a float to an integer type, determine the range
+ -- in real first, and then convert the bounds using UR_To_Uint
+ -- which correctly rounds away from zero when half way between two
+ -- integers, as required by normal Ada 95 rounding semantics. It
+ -- is only possible because analysis in GNATprove rules out the
+ -- possibility of a NaN or infinite value.
+
+ elsif GNATprove_Mode
+ and then Is_Floating_Point_Type (Etype (Expression (N)))
+ then
+ declare
+ Lor_Real, Hir_Real : Ureal;
+ begin
+ Determine_Range_R (Expression (N), OK1, Lor_Real, Hir_Real,
+ Assume_Valid);
+
+ if OK1 then
+ Lor := UR_To_Uint (Lor_Real);
+ Hir := UR_To_Uint (Hir_Real);
+ end if;
+ end;
+
+ else
+ OK1 := False;
+ end if;
-- Nothing special to do for all other expression kinds
end if;
end if;
- -- If at this stage we have a real to integer conversion, make sure
- -- that the Do_Range_Check flag is set, because such conversions in
- -- general need a range check. We only need this if expansion is off
- -- or we are in GNATProve mode.
+ -- If at this stage we have a real to integer conversion, make sure that
+ -- the Do_Range_Check flag is set, because such conversions in general
+ -- need a range check. We only need this if expansion is off, or we are
+ -- in GNATprove mode and the conversion if from fixed-point to integer
+ -- (as floating-point to integer conversions are now handled in
+ -- GNATprove mode).
if Nkind (N) = N_Type_Conversion
- and then (GNATprove_Mode or not Expander_Active)
+ and then not Expander_Active
and then Is_Integer_Type (Target_Typ)
- and then Is_Real_Type (Operand_Typ)
+ and then (Is_Real_Type (Operand_Typ)
+ or else (GNATprove_Mode
+ and then Is_Fixed_Point_Type (Operand_Typ)))
then
Set_Do_Range_Check (Operand);
end if;
git://gcc.gnu.org / gcc.git / commitdiff