From 9784779754d2861aa1b9c8d94da971f83e383e01 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Mon, 9 Nov 2020 14:13:58 +0100 Subject: [PATCH] [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. --- 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; -------------------------------- -- 2.30.2