[multiple changes]

2016-04-18  Arnaud Charlet  <charlet@adacore.com>

	* 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  <moy@adacore.com>

	* 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  <moy@adacore.com>

	* 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

1 files changed, 16 insertions, 14 deletions

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;