From 6be763897bcabab90eeae0dfda963531802a4ae9 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 8 Apr 2020 23:38:51 +0200 Subject: [PATCH] [Ada] Fix expansion of "for X of Y loop" in GNATprove 2020-06-17 Piotr Trojanek gcc/ada/ * sem_ch5.adb (Analyze_Iterator_Specification): Enable expansion that creates a renaming that removes side effects from the iterated object in the GNATprove mode; then analyze reference to this renaming (it is required for GNATprove and harmless for GNAT). --- gcc/ada/sem_ch5.adb | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 95ada06..01f0b50 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2214,8 +2214,8 @@ package body Sem_Ch5 is -- If the domain of iteration is an expression, create a declaration for -- it, so that finalization actions are introduced outside of the loop. - -- The declaration must be a renaming because the body of the loop may - -- assign to elements. + -- The declaration must be a renaming (both in GNAT and GNATprove + -- modes), because the body of the loop may assign to elements. if not Is_Entity_Name (Iter_Name) @@ -2224,14 +2224,15 @@ package body Sem_Ch5 is -- doing expansion. and then (Nkind (Parent (N)) /= N_Quantified_Expression - or else Operating_Mode = Check_Semantics) + or else (Operating_Mode = Check_Semantics + and then not GNATprove_Mode)) -- Do not perform this expansion when expansion is disabled, where the -- temporary may hide the transformation of a selected component into -- a prefixed function call, and references need to see the original -- expression. - and then Expander_Active + and then (Expander_Active or GNATprove_Mode) then declare Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name); @@ -2319,6 +2320,7 @@ package body Sem_Ch5 is Insert_Actions (Parent (Parent (N)), New_List (Decl)); Rewrite (Name (N), New_Occurrence_Of (Id, Loc)); + Analyze (Name (N)); Set_Etype (Id, Typ); Set_Etype (Name (N), Typ); end; -- 2.7.4