This change makes sure that the Do_Range_Check flag is set in -gnatc or
GNATprove mode for type conversions from real to integer. This makes sure
that SPARK2014 programs properly verify that such conversions cannot raise
an exception due to an out of range value. The following test compiled
with -gnatdt generates a tree that has one instance of Do_Range_Check
being set.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-08-04 Robert Dewar <de...@adacore.com>
* sem_res.adb (Resolve_Type_Conversion): Set Do_Range_Check on
conversion from a real type to an integer type.
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 213537)
+++ sem_res.adb (working copy)
@@ -10322,11 +10322,11 @@
-- odd subtype coming from the bounds).
if (Is_Entity_Name (Orig_N)
- and then
- (Etype (Entity (Orig_N)) = Orig_T
- or else
- (Ekind (Entity (Orig_N)) = E_Loop_Parameter
- and then Covers (Orig_T, Etype (Entity (Orig_N))))))
+ and then
+ (Etype (Entity (Orig_N)) = Orig_T
+ or else
+ (Ekind (Entity (Orig_N)) = E_Loop_Parameter
+ and then Covers (Orig_T, Etype (Entity (Orig_N))))))
-- If not an entity, then type of expression must match
@@ -10504,6 +10504,17 @@
Apply_Predicate_Check (N, Target_Typ);
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.
+
+ if Nkind (N) = N_Type_Conversion
+ and then Is_Integer_Type (Target_Typ)
+ and then Is_Real_Type (Operand_Typ)
+ then
+ Set_Do_Range_Check (Operand);
+ end if;
end Resolve_Type_Conversion;
----------------------
