From: Javier Miranda <miranda@adacore.com>
Date: Mon, 16 Jul 2018 14:10:27 +0000 (+0000)
Subject: [Ada] Crash processing sources under GNATprove debug mode
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a3b7645bffbaf3dadf1f9cfccd93c6fba3e0834d;p=gcc.git

[Ada] Crash processing sources under GNATprove debug mode

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.

2018-07-16  Javier Miranda  <miranda@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.

From-SVN: r262707
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d041f562043..bff06e6be43 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-07-16  Javier Miranda  <miranda@adacore.com>
+
+	* 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.
+
 2018-07-16  Yannick Moy  <moy@adacore.com>
 
 	* inline.adb (Has_Single_Return): Rewrap comment.
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index e0cff915bca..7371ee33acb 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/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))),
diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 57c59974259..f73096e0f30 100644
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2018-07-16  Javier Miranda  <miranda@adacore.com>
+
+	* gnat.dg/iter2.adb, gnat.dg/iter2.ads: New testcase.
+
 2018-07-16  Richard Biener  <rguenther@suse.de>
 
 	PR lto/86523
diff --git a/gcc/testsuite/gnat.dg/iter2.adb b/gcc/testsuite/gnat.dg/iter2.adb
new file mode 100644
index 00000000000..e5819a031b7
--- /dev/null
+++ b/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;
diff --git a/gcc/testsuite/gnat.dg/iter2.ads b/gcc/testsuite/gnat.dg/iter2.ads
new file mode 100644
index 00000000000..2178630944a
--- /dev/null
+++ b/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;