diff options
| author | Ed Schonberg <schonberg@adacore.com> | 2018-10-09 15:04:58 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-10-09 15:04:58 +0000 |
| commit | 94a98e801a6889e791aee63fcdbb6ee173d0259e (patch) | |
| tree | e8b3ed61cd25937d2f439f3e254621e48d2d3756 /gcc | |
| parent | 0ffbef9f3553b6f9841f01ac5ff61850af63b219 (diff) | |
| download | gcc-94a98e801a6889e791aee63fcdbb6ee173d0259e.zip gcc-94a98e801a6889e791aee63fcdbb6ee173d0259e.tar.gz gcc-94a98e801a6889e791aee63fcdbb6ee173d0259e.tar.bz2 | |
[Ada] Preserve Do_Range_Check flags in SPARK mode
2018-10-09 Ed Schonberg <schonberg@adacore.com>
gcc/ada/
* checks.adb (Apply_Type_Conversion_Checks): Use GNATprove_Mode
rather than SPARK_mode in order to preserve the Do_Range_Check
flag for verification purposes.
From-SVN: r264961
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 6 | ||||
| -rw-r--r-- | gcc/ada/checks.adb | 5 |
2 files changed, 8 insertions, 3 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f6925bc..54da439 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,11 @@ 2018-10-09 Ed Schonberg <schonberg@adacore.com> + * checks.adb (Apply_Type_Conversion_Checks): Use GNATprove_Mode + rather than SPARK_mode in order to preserve the Do_Range_Check + flag for verification purposes. + +2018-10-09 Ed Schonberg <schonberg@adacore.com> + * exp_aggr.adb (Expand_Array_Aggregate): If it is not possible to build in place an aggregate with component associations, set the Warnings_Off flag on the generated temporary, to prevent diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 5cefbbd..6176886 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -3555,9 +3555,8 @@ package body Checks is -- in SPARK_Mode, where the explicit constraint check will -- not be generated. - if SPARK_Mode = On - or else (not Is_Fixed_Point_Type (Expr_Type) - and then not Is_Fixed_Point_Type (Target_Type)) + if GNATprove_Mode + or else not Is_Fixed_Point_Type (Expr_Type) then Apply_Scalar_Range_Check (Expr, Target_Type, Fixed_Int => Conv_OK); |