From 4ffefb704a8e805278e72ed9bee7c94c0a1401d4 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 10 Apr 2020 19:30:13 +0200 Subject: [PATCH] [Ada] Remove unnecessary special-casing of GNATprove expansion 2020-06-17 Piotr Trojanek gcc/ada/ * checks.adb (Generate_Range_Check): Simplify redundant condition. * sem_ch3.adb (Check_Initialization, Process_Discriminants): Likewise. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Likewise. --- gcc/ada/checks.adb | 10 +++++----- gcc/ada/sem_ch3.adb | 4 ++-- gcc/ada/sem_ch6.adb | 8 +------- 3 files changed, 8 insertions(+), 14 deletions(-) diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 52cf61f..aab9e33 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -7001,12 +7001,12 @@ package body Checks is return; end if; - -- Here a check is needed. If the expander is not active, or if we are - -- in GNATProve mode, then simply set the Do_Range_Check flag and we - -- are done. In both these cases, we just want to see the range check - -- flag set, we do not want to generate the explicit range check code. + -- Here a check is needed. If the expander is not active (which is also + -- the case in GNATprove mode), then simply set the Do_Range_Check flag + -- and we are done. We just want to see the range check flag set, we do + -- not want to generate the explicit range check code. - if GNATprove_Mode or else not Expander_Active then + if not Expander_Active then Set_Do_Range_Check (N); return; end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index facd57c4d..54b2f62 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -11804,7 +11804,7 @@ package body Sem_Ch3 is -- In gnatc or gnatprove mode, make sure set Do_Range_Check flag gets -- set unless we can be sure that no range check is required. - if (GNATprove_Mode or not Expander_Active) + if not Expander_Active and then Is_Scalar_Type (T) and then not Is_In_Range (Exp, T, Assume_Valid => True) then @@ -19853,7 +19853,7 @@ package body Sem_Ch3 is -- In gnatc or gnatprove mode, make sure set Do_Range_Check flag -- gets set unless we can be sure that no range check is required. - if (GNATprove_Mode or not Expander_Active) + if not Expander_Active and then not Is_In_Range (Expression (Discr), Discr_Type, Assume_Valid => True) diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 1b3cba8..b60133a 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4402,13 +4402,7 @@ package body Sem_Ch6 is -- Handle inlining - -- Note: Normally we don't do any inlining if expansion is off, since - -- we won't generate code in any case. An exception arises in GNATprove - -- mode where we want to expand some calls in place, even with expansion - -- disabled, since the inlining eases formal verification. - - if not GNATprove_Mode - and then Expander_Active + if Expander_Active and then Serious_Errors_Detected = 0 and then Present (Spec_Id) and then Has_Pragma_Inline (Spec_Id) -- 2.7.4