[Ada] Preserve Do_Range_Check flags in SPARK mode
authorEd Schonberg <schonberg@adacore.com>
Tue, 9 Oct 2018 15:04:58 +0000 (15:04 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Oct 2018 15:04:58 +0000 (15:04 +0000)
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

gcc/ada/ChangeLog
gcc/ada/checks.adb

index f6925bc9b501b6787fdb4c96f6346095c05d23ed..54da439d226d7c69b9645688313b84b791e53ede 100644 (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
index 5cefbbd8415942ccd2dec47f5b85e3842ff5e75e..61768865ce140e55d42433508e8598f401d1e542 100644 (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);