From 95c1628619e7f9d80aab6b2f662ef4c603eb6d77 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Tue, 9 Oct 2018 15:04:58 +0000 Subject: [PATCH] [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. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@264961 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 6 ++++++ gcc/ada/checks.adb | 5 ++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f6925bc9b50..54da439d226 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,11 @@ 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 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 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); -- 2.11.4.GIT