[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.
This commit is contained in:
parent
e9c85394fb
commit
4ffefb704a
@ -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;
|
||||
|
@ -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)
|
||||
|
@ -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)
|
||||
|
Loading…
Reference in New Issue
Block a user