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/sem_eval.adb | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) (limited to 'gcc/ada/sem_eval.adb') diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index 67d464c..9703943 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -1885,9 +1885,14 @@ package body Sem_Eval is -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "division by zero", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); Set_Raises_Constraint_Error (N); return; @@ -1903,10 +1908,16 @@ package body Sem_Eval is -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "mod with zero divisor", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); return; + else Result := Left_Int mod Right_Int; end if; @@ -1917,9 +1928,14 @@ package body Sem_Eval is -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "rem with zero divisor", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); return; else -- cgit v1.1