From: Ed Schonberg Date: Tue, 9 Oct 2018 15:04:58 +0000 (+0000) Subject: [Ada] Preserve Do_Range_Check flags in SPARK mode X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94a98e801a6889e791aee63fcdbb6ee173d0259e;p=gcc.git [Ada] Preserve Do_Range_Check flags in SPARK mode 2018-10-09 Ed Schonberg 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f6925bc9b50..54da439d226 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2018-10-09 Ed Schonberg + + * 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 * exp_aggr.adb (Expand_Array_Aggregate): If it is not possible diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 5cefbbd8415..61768865ce1 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);