[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

10 files changed, 126 insertions, 29 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 11cbcb0..2b8e6ae 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,25 @@
+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.
+
 2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Check_In_Out_States.Check_Constituent_Usage):
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;
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index b38b82b..52de7a1 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -158,7 +158,7 @@ package body Debug is
    --  d.1  Enable unnesting of nested procedures
    --  d.2  Allow statements in declarative part
    --  d.3  Output debugging information from Exp_Unst
-   --  d.4
+   --  d.4  Do not delete generated C file in case of errors
    --  d.5  Do not generate imported subprogram definitions in C code
    --  d.6
    --  d.7
@@ -762,6 +762,9 @@ package body Debug is
    --  d.3  Output debugging information from Exp_Unst, including the name of
    --       any unreachable subprograms that get deleted.
 
+   --  d.4  By default in case of an error during C generation, the .c or .h
+   --       file is delete. This flag keeps the C file.
+
    --  d.5  By default a subprogram imported generates a subprogram profile.
    --       This debug flag disables this generation when generating C code,
    --       assuming a proper #include will be used instead.
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 220ad93..bc52f41 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -46,6 +46,7 @@ with Namet;    use Namet;
 with Nlists;
 with Opt;      use Opt;
 with Osint;    use Osint;
+with Osint.C;  use Osint.C;
 with Output;   use Output;
 with Par_SCO;
 with Prepcomp;
@@ -1078,6 +1079,13 @@ begin
          Comperr.Delete_SCIL_Files;
       end if;
 
+      --  Ditto for old C files before regenerating new ones
+
+      if Generate_C_Code then
+         Delete_C_File;
+         Delete_H_File;
+      end if;
+
       --  Exit if compilation errors detected
 
       Errout.Finalize (Last_Call => False);
diff --git a/gcc/ada/osint-c.adb b/gcc/ada/osint-c.adb
index a24a5a7..919f188 100644
--- a/gcc/ada/osint-c.adb
+++ b/gcc/ada/osint-c.adb
@@ -292,6 +292,28 @@ package body Osint.C is
       end if;
    end Debug_File_Eol_Length;
 
+   -------------------
+   -- Delete_C_File --
+   -------------------
+
+   procedure Delete_C_File is
+      Dummy : Boolean;
+   begin
+      Set_File_Name ("c");
+      Delete_File (Name_Buffer (1 .. Name_Len), Dummy);
+   end Delete_C_File;
+
+   -------------------
+   -- Delete_H_File --
+   -------------------
+
+   procedure Delete_H_File is
+      Dummy : Boolean;
+   begin
+      Set_File_Name ("h");
+      Delete_File (Name_Buffer (1 .. Name_Len), Dummy);
+   end Delete_H_File;
+
    ---------------------------------
    -- Get_Output_Object_File_Name --
    ---------------------------------
diff --git a/gcc/ada/osint-c.ads b/gcc/ada/osint-c.ads
index 6819ec0..54ffb01 100644
--- a/gcc/ada/osint-c.ads
+++ b/gcc/ada/osint-c.ads
@@ -159,7 +159,7 @@ package Osint.C is
    --------------------------
 
    --  These routines are used by the compiler when the C translation option
-   --  is activated to write *.c and *.h files to the current object directory.
+   --  is activated to write *.c or *.h files to the current object directory.
    --  Each routine exists in a C and an H form for the two kinds of files.
    --  Only one of these files can be written at a time. Note that the files
    --  are written via the Output package routines, using Output_FD.
@@ -175,6 +175,11 @@ package Osint.C is
    --  Closes the file created by Create_C_File or Create_H file, flushing any
    --  buffers etc. from writes by Write_C_File and Write_H_File;
 
+   procedure Delete_C_File;
+   procedure Delete_H_File;
+   --  Deletes the .c or .h file corresponding to the source file which is
+   --  currently being compiled.
+
    ----------------------
    -- List File Output --
    ----------------------
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
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index c12356c..6780772 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -5440,7 +5440,9 @@ package body Sem_Res is
                              and then Expr_Value_R (Rop) = Ureal_0))
             then
                --  Specialize the warning message according to the operation.
-               --  The following warnings are for the case
+               --  When SPARK_Mode is On, force a warning instead of an error
+               --  in that case, as this likely corresponds to deactivated
+               --  code. The following warnings are for the case
 
                case Nkind (N) is
                   when N_Op_Divide =>
@@ -5459,23 +5461,26 @@ package body Sem_Res is
                           ("float division by zero, may generate "
                            & "'+'/'- infinity??", Right_Opnd (N));
 
-                        --  For all other cases, we get a Constraint_Error
+                     --  For all other cases, we get a Constraint_Error
 
                      else
                         Apply_Compile_Time_Constraint_Error
                           (N, "division by zero??", CE_Divide_By_Zero,
-                           Loc => Sloc (Right_Opnd (N)));
+                           Loc  => Sloc (Right_Opnd (N)),
+                           Warn => SPARK_Mode = On);
                      end if;
 
                   when N_Op_Rem =>
                      Apply_Compile_Time_Constraint_Error
                        (N, "rem with zero divisor??", CE_Divide_By_Zero,
-                        Loc => Sloc (Right_Opnd (N)));
+                        Loc  => Sloc (Right_Opnd (N)),
+                        Warn => SPARK_Mode = On);
 
                   when N_Op_Mod =>
                      Apply_Compile_Time_Constraint_Error
                        (N, "mod with zero divisor??", CE_Divide_By_Zero,
-                        Loc => Sloc (Right_Opnd (N)));
+                        Loc  => Sloc (Right_Opnd (N)),
+                        Warn => SPARK_Mode = On);
 
                   --  Division by zero can only happen with division, rem,
                   --  and mod operations.
@@ -5484,6 +5489,13 @@ package body Sem_Res is
                      raise Program_Error;
                end case;
 
+               --  In GNATprove mode, we enable the division check so that
+               --  GNATprove will issue a message if it cannot be proved.
+
+               if GNATprove_Mode then
+                  Activate_Division_Check (N);
+               end if;
+
             --  Otherwise just set the flag to check at run time
 
             else
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 1146b9d..348da03 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4574,9 +4574,16 @@ package body Sem_Util is
 
    begin
       --  If this is a warning, convert it into an error if we are in code
-      --  subject to SPARK_Mode being set ON.
+      --  subject to SPARK_Mode being set On, unless Warn is True to force a
+      --  warning. The rationale is that a compile-time constraint error should
+      --  lead to an error instead of a warning when SPARK_Mode is On, but in
+      --  a few cases we prefer to issue a warning and generate both a suitable
+      --  run-time error in GNAT and a suitable check message in GNATprove.
+      --  Those cases are those that likely correspond to deactivated SPARK
+      --  code, so that this kind of code can be compiled and analyzed instead
+      --  of being rejected.
 
-      Error_Msg_Warn := SPARK_Mode /= On;
+      Error_Msg_Warn := Warn or SPARK_Mode /= On;
 
       --  A static constraint error in an instance body is not a fatal error.
       --  we choose to inhibit the message altogether, because there is no
@@ -4648,8 +4655,6 @@ package body Sem_Util is
          --  evaluated.
 
          if not Is_Statically_Unevaluated (N) then
-            Error_Msg_Warn := SPARK_Mode /= On;
-
             if Present (Ent) then
                Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
             else
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index d8a9b52..494a9e4 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -135,7 +135,9 @@ package Sem_Util is
    --  is present, this is used instead. Warn is normally False. If it is
    --  True then the message is treated as a warning even though it does
    --  not end with a ? (this is used when the caller wants to parameterize
-   --  whether an error or warning is given).
+   --  whether an error or warning is given), or when the message should be
+   --  treated as a warning even when SPARK_Mode is On (which otherwise would
+   --  force an error).
 
    function Async_Readers_Enabled (Id : Entity_Id) return Boolean;
    --  Given the entity of an abstract state or a variable, determine whether