From: Yannick Moy <moy@adacore.com>
Date: Tue, 18 May 2021 10:35:08 +0000 (+0200)
Subject: [Ada] Simplify handling of sure errors in GNATprove mode
X-Git-Tag: basepoints/gcc-13~6200
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a7f66404a62179ed8d759e8d454635f775cef016;p=thirdparty%2Fgcc.git

[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 76fd9b037fb2..61ce9c22c046 100644
--- 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 54d476ef590c..5791d3d99370 100644
--- 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 9d54309601ad..799f720e6733 100644
--- 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.