[Ada] Fix folding of comparison operators in GNATprove mode

gcc/ada/

	* exp_util.adb (Get_Current_Value_Condition): Don't use current
	value tracking in GNATprove mode.
	* sem_res.adb (Resolve_Comparison_Op): Remove incomplete
	special-casing for folding in GNATprove mode.

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 6d043fd1a624ca00488716ee6b840f2e0289b282..11efd46651e0130e55e0a7d8497a430b6c01bfdb 100644 (file)
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -6360,6 +6360,17 @@ package body Exp_Util is
          return;
       end if;
 
+      --  In GNATprove mode we don't want to use current value optimizer, in
+      --  particular for loop invariant expressions and other assertions that
+      --  act as cut points for proof. The optimizer often folds expressions
+      --  into True/False where they trivially follow from the previous
+      --  assignments, but this deprives proof from the information needed to
+      --  discharge checks that are beyond the scope of the value optimizer.
+
+      if GNATprove_Mode then
+         return;
+      end if;
+
       --  Otherwise examine current value
 
       declare

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 93641c9687463111bcdb0e3f2f61671717407169..ed744ea749bda4cda6620edb45508a3f12b5e3c6 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7457,24 +7457,7 @@ package body Sem_Res is
 
       Analyze_Dimension (N);
 
-      --  Evaluate the relation (note we do this after the above check since
-      --  this Eval call may change N to True/False). Skip this evaluation
-      --  inside assertions, in order to keep assertions as written by users
-      --  for tools that rely on these, e.g. GNATprove for loop invariants.
-      --  Except evaluation is still performed even inside assertions for
-      --  comparisons between values of universal type, which are useless
-      --  for static analysis tools, and not supported even by GNATprove.
-      --  ??? It is suspicious to disable evaluation only for comparison
-      --  operators and not, let's say, for calls to static functions.
-
-      if not GNATprove_Mode
-        or else In_Assertion_Expr = 0
-        or else (Is_Universal_Numeric_Type (Etype (L))
-                   and then
-                 Is_Universal_Numeric_Type (Etype (R)))
-      then
-         Eval_Relational_Op (N);
-      end if;
+      Eval_Relational_Op (N);
    end Resolve_Comparison_Op;
 
    --------------------------------