[Ada] Crash processing sources under GNATprove debug mode

[Pierre-Marie de Rodat]

Processing sources under -gnatd.F the frontend may crash on
an iterator of the form 'for X of ...' over an array if the
iterator is located in an inlined subprogram.

Tested on x86_64-pc-linux-gnu, committed on trunk

2018-07-16  Javier Miranda  <mira...@adacore.com>

gcc/ada/

        * exp_ch5.adb (Expand_Iterator_Loop_Over_Array): Code cleanup. Required
        to avoid generating an ill-formed tree that confuses gnatprove causing
        it to blowup.

gcc/testsuite/

        * gnat.dg/iter2.adb, gnat.dg/iter2.ads: New testcase.
--- gcc/ada/exp_ch5.adb
+++ gcc/ada/exp_ch5.adb
@@ -3711,9 +3711,14 @@ package body Exp_Ch5 is
 
       Ind_Comp :=
         Make_Indexed_Component (Loc,
-          Prefix      => Relocate_Node (Array_Node),
+          Prefix      => New_Copy_Tree (Array_Node),
           Expressions => New_List (New_Occurrence_Of (Iterator, Loc)));
 
+      --  Propagate the original node to the copy since the analysis of the
+      --  following object renaming declaration relies on the original node.
+
+      Set_Original_Node (Prefix (Ind_Comp), Original_Node (Array_Node));
+
       Prepend_To (Stats,
         Make_Object_Renaming_Declaration (Loc,
           Defining_Identifier => Id,
@@ -3755,7 +3760,7 @@ package body Exp_Ch5 is
                   Defining_Identifier         => Iterator,
                   Discrete_Subtype_Definition =>
                     Make_Attribute_Reference (Loc,
-                      Prefix         => Relocate_Node (Array_Node),
+                      Prefix         => New_Copy_Tree (Array_Node),
                       Attribute_Name => Name_Range,
                       Expressions    => New_List (
                         Make_Integer_Literal (Loc, Dim1))),
@@ -3792,7 +3797,7 @@ package body Exp_Ch5 is
                         Defining_Identifier         => Iterator,
                         Discrete_Subtype_Definition =>
                           Make_Attribute_Reference (Loc,
-                            Prefix         => Relocate_Node (Array_Node),
+                            Prefix         => New_Copy_Tree (Array_Node),
                             Attribute_Name => Name_Range,
                             Expressions    => New_List (
                               Make_Integer_Literal (Loc, Dim1))),

--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/iter2.adb
@@ -0,0 +1,28 @@
+--  { dg-do compile }
+--  { dg-options "-gnatd.F -gnatws" }
+
+package body Iter2
+   with SPARK_Mode
+is
+   function To_String (Name : String) return String
+   is
+      procedure Append (Result : in out String;
+                        Data   :        String)
+        with Inline_Always;
+      procedure Append (Result : in out String;
+                        Data   :        String)
+      is
+      begin
+         for C of Data
+         loop
+            Result (1) := C;
+         end loop;
+      end Append;
+
+      Result : String (1 .. 3);
+   begin
+      Append (Result, "</" & Name & ">");
+      return Result;
+   end To_String;
+
+end Iter2;

--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/iter2.ads
@@ -0,0 +1,5 @@
+package Iter2
+   with SPARK_Mode
+is
+   function To_String (Name : String) return String;
+end Iter2;