From: Piotr Trojanek <trojanek@adacore.com>
Date: Mon, 9 Nov 2020 13:13:58 +0000 (+0100)
Subject: [Ada] Fix folding of comparison operators in GNATprove mode
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9784779754d2861aa1b9c8d94da971f83e383e01;p=gcc.git

[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 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;
 
    --------------------------------