From 520c0201ebc60741a955d451bb6e9cc57c268014 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 18 Apr 2016 14:33:46 +0200 Subject: [multiple changes] 2016-04-18 Arnaud Charlet * osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New. * gnat1drv.adb (Gnat1drv): Delete old C files before regenerating them. * debug.adb: Reserve -gnatd.4 to force generation of C files. 2016-04-18 Yannick Moy * sem_eval.adb (Eval_Arithmetic_Op): Do not issue error on static division by zero, instead possibly issue a warning. * sem_res.adb (Resolve_Arithmetic_Op): Do not issue error on static division by zero, instead add check flag on original expression. * sem_util.adb, sem_util.ads (Compile_Time_Constraint_Error): Only issue error when both SPARK_Mode is On and Warn is False. 2016-04-18 Yannick Moy * checks.adb (Apply_Scalar_Range_Check): Force warning instead of error when SPARK_Mode is On, on index out of bounds, and set check flag for GNATprove. From-SVN: r235138 --- gcc/ada/checks.adb | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'gcc/ada/checks.adb') diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index a3ea477..e6eab0c 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2749,19 +2749,22 @@ package body Checks is -- Set to True if Expr should be regarded as a real value even though -- the type of Expr might be discrete. - procedure Bad_Value; - -- Procedure called if value is determined to be out of range + procedure Bad_Value (Warn : Boolean := False); + -- Procedure called if value is determined to be out of range. Warn is + -- True to force a warning instead of an error, even when SPARK_Mode is + -- On. --------------- -- Bad_Value -- --------------- - procedure Bad_Value is + procedure Bad_Value (Warn : Boolean := False) is begin Apply_Compile_Time_Constraint_Error (Expr, "value not in range of}??", CE_Range_Check_Failed, - Ent => Target_Typ, - Typ => Target_Typ); + Ent => Target_Typ, + Typ => Target_Typ, + Warn => Warn); end Bad_Value; -- Start of processing for Apply_Scalar_Range_Check @@ -2968,18 +2971,17 @@ package body Checks is if Lov > Hiv then - -- In GNATprove mode, do not issue a message in that case - -- (which would be an error stopping analysis), as this - -- likely corresponds to deactivated code based on a - -- given configuration (say, dead code inside a loop over - -- the empty range). Instead, we enable the range check - -- so that GNATprove will issue a message if it cannot be - -- proved. + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + + Bad_Value (Warn => SPARK_Mode = On); + + -- In GNATprove mode, we enable the range check so that + -- GNATprove will issue a message if it cannot be proved. if GNATprove_Mode then Enable_Range_Check (Expr); - else - Bad_Value; end if; return; -- cgit v1.1