diff options
| author | Yannick Moy <moy@adacore.com> | 2017-04-25 10:09:31 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-04-25 12:09:31 +0200 |
| commit | d8ee014f291458a3518ea516619e75faf24aca17 (patch) | |
| tree | c073b26e5d471ac891115b0d2173abf751c6f1b1 /gcc/ada/usage.adb | |
| parent | 3c77943ebf24f7751cff692cf83fccc4866453e5 (diff) | |
| download | gcc-d8ee014f291458a3518ea516619e75faf24aca17.zip gcc-d8ee014f291458a3518ea516619e75faf24aca17.tar.gz gcc-d8ee014f291458a3518ea516619e75faf24aca17.tar.bz2 | |
checks.adb (Apply_Scalar_Range_Check): Analyze precisely conversions from float to integer in GNATprove mode.
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.
From-SVN: r247173
Diffstat (limited to 'gcc/ada/usage.adb')
0 files changed, 0 insertions, 0 deletions