diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2023-12-04 17:41:27 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2024-01-09 14:13:31 +0100 |
commit | da75ce88bde06bfcef2d454054f43ed430d96b00 (patch) | |
tree | f80d37d1ebe8a8734e6267712d8aba1f411e2c0d | |
parent | 9afbf898ce89f6bcb314ddf03da20abdf0ac79cd (diff) | |
download | gcc-da75ce88bde06bfcef2d454054f43ed430d96b00.zip gcc-da75ce88bde06bfcef2d454054f43ed430d96b00.tar.gz gcc-da75ce88bde06bfcef2d454054f43ed430d96b00.tar.bz2 |
ada: Remove side effects depending on the context of subtype declaration
In GNATprove mode the removal of side effects is only needed in certain
syntactic contexts, which include subtype declarations. Now this removal
is limited to genuine subtype declarations and not to itypes coming from
expressions where side effects are not expected.
gcc/ada/
* exp_util.adb (Possible_Side_Effect_In_SPARK): Refine handling of
itype declarations.
-rw-r--r-- | gcc/ada/exp_util.adb | 74 |
1 files changed, 63 insertions, 11 deletions
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index b9346a9..1df63ed 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -12012,19 +12012,71 @@ package body Exp_Util is function Possible_Side_Effect_In_SPARK (Exp : Node_Id) return Boolean is begin - -- Side-effect removal in SPARK should only occur when not inside a - -- generic and not doing a preanalysis, inside an object renaming or - -- a type declaration or a for-loop iteration scheme. + -- Side-effect removal in SPARK should only occur when not inside a + -- generic and not doing a preanalysis, inside an object renaming or + -- a type declaration or a for-loop iteration scheme. - return not Inside_A_Generic + if not Inside_A_Generic and then Full_Analysis - and then Nkind (Enclosing_Declaration (Exp)) in - N_Component_Declaration - | N_Full_Type_Declaration - | N_Iterator_Specification - | N_Loop_Parameter_Specification - | N_Object_Renaming_Declaration - | N_Subtype_Declaration; + then + + case Nkind (Enclosing_Declaration (Exp)) is + when N_Component_Declaration + | N_Full_Type_Declaration + | N_Iterator_Specification + | N_Loop_Parameter_Specification + | N_Object_Renaming_Declaration + => + return True; + + -- If the expression belongs to an itype declaration, then + -- check if side effects are allowed in the original + -- associated node. + + when N_Subtype_Declaration => + declare + Subt : constant Entity_Id := + Defining_Identifier (Enclosing_Declaration (Exp)); + begin + if Is_Itype (Subt) then + + -- When this routine is called while the itype + -- is being created, the entity might not yet be + -- decorated with the associated node, but should + -- have the related expression. + + if Present (Associated_Node_For_Itype (Subt)) then + return + Possible_Side_Effect_In_SPARK + (Associated_Node_For_Itype (Subt)); + + elsif Present (Related_Expression (Subt)) then + return + Possible_Side_Effect_In_SPARK + (Related_Expression (Subt)); + + -- When the itype doesn't have any indication of its + -- origin (which currently only happens for packed + -- array types created by freezing that shouldn't + -- be picked by GNATprove anyway), then we can + -- conservatively assume that the expression can + -- be kept as it appears in the source code. + + else + pragma Assert (Is_Packed_Array_Impl_Type (Subt)); + return False; + end if; + else + return True; + end if; + end; + + when others => + return False; + end case; + else + return False; + end if; end Possible_Side_Effect_In_SPARK; -- Local variables |