OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Preserve Do_Range_Check flags in SPARK mode

Browse Source 
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
This commit is contained in:
Ed Schonberg 2018-10-09 15:04:58 +00:00 committed by Pierre-Marie de Rodat
parent 0ffbef9f35
commit 94a98e801a
2 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
gcc/ada/ChangeLog
View File

@ -1,3 +1,9 @@
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

5
gcc/ada/checks.adb
View File

@ -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);