[Ada] Fix expansion of "for X of Y loop" in GNATprove

2020-06-17  Piotr Trojanek  <trojanek@adacore.com>

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).

diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 95ada06..01f0b50 100644 (file)
--- 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;