diff mbox series

[Ada] Simplify handling of sure errors in GNATprove mode

Message ID 20210707162503.GA2542979@adacore.com
State New
Headers show
Series [Ada] Simplify handling of sure errors in GNATprove mode | expand

Commit Message

Pierre-Marie de Rodat July 7, 2021, 4:25 p.m. UTC 
In cases where it is known statically that an exception will be raised,
the frontend inserts a node of kind N_Raise_xxx_Error. This node kind
was previously not supported in GNATprove, which required special
handling for these cases in GNATprove mode. This is not needed anymore.

Tested on x86_64-pc-linux-gnu, committed on trunk

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 mbox series

Patch

diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
--- 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
--- 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
--- 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.