[Ada] Simplify handling of sure errors in GNATprove mode

gcc/ada/

	* checks.adb (Apply_Scalar_Range_Check): Remove special case for
	GNATprove mode.
	* sem_res.adb (Resolve_Arithmetic_Op): Same.
	* sem_util.adb (Apply_Compile_Time_Constraint_Error): Same.

diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 76fd9b0..61ce9c2 100644 (file)
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -3323,13 +3323,6 @@ package body Checks is
 
                      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);
-                     end if;
-
                      return;
                   end if;
 

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 54d476e..5791d3d 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6151,13 +6151,6 @@ 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 9d54309..799f720 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1533,17 +1533,6 @@ package body Sem_Util is
       Discard_Node
         (Compile_Time_Constraint_Error (N, Msg, Ent, Loc, Warn => Warn));
 
-      --  In GNATprove mode, do not replace the node with an exception raised.
-      --  In such a case, either the call to Compile_Time_Constraint_Error
-      --  issues an error which stops analysis, or it issues a warning in
-      --  a few cases where a suitable check flag is set for GNATprove to
-      --  generate a check message.
-
-      if GNATprove_Mode then
-         Set_Raises_Constraint_Error (N);
-         return;
-      end if;
-
       --  Now we replace the node by an N_Raise_Constraint_Error node
       --  This does not need reanalyzing, so set it as analyzed now.