aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2020-04-10 19:30:13 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2020-06-17 04:14:00 -0400
commit4ffefb704a8e805278e72ed9bee7c94c0a1401d4 (patch)
tree819d449dce38e6440606cd6b86001de20f621772
parente9c85394fb16fd43a05cd9ee5dbca3e96cc68dfb (diff)
downloadgcc-4ffefb704a8e805278e72ed9bee7c94c0a1401d4.zip
gcc-4ffefb704a8e805278e72ed9bee7c94c0a1401d4.tar.gz
gcc-4ffefb704a8e805278e72ed9bee7c94c0a1401d4.tar.bz2
[Ada] Remove unnecessary special-casing of GNATprove expansion
2020-06-17 Piotr Trojanek <trojanek@adacore.com> 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.
-rw-r--r--gcc/ada/checks.adb10
-rw-r--r--gcc/ada/sem_ch3.adb4
-rw-r--r--gcc/ada/sem_ch6.adb8
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)