Folding of comparison operators was disabled for GNATprove in assertion
expressions (except for some special cases). However, folding itself is
harmless. The problem was only in the current value optimizer, which
interferes with assertions that act as cut points for proof.
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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
--- 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;
--------------------------------
