[gcc r11-5548] [Ada] Fix folding of comparison operators in GNATprove mode

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:9784779754d2861aa1b9c8d94da971f83e383e01

commit r11-5548-g9784779754d2861aa1b9c8d94da971f83e383e01
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Mon Nov 9 14:13:58 2020 +0100

    [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:
---
 gcc/ada/exp_util.adb | 11 +++++++++++
 gcc/ada/sem_res.adb  | 19 +------------------
 2 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 6d043fd1a62..11efd46651e 100644
--- 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 93641c96874..ed744ea749b 100644
--- 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;
 
    --------------------------------