[Ada] Crash processing sources under GNATprove debug mode
authorJavier Miranda <miranda@adacore.com>
Mon, 16 Jul 2018 14:10:27 +0000 (14:10 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 16 Jul 2018 14:10:27 +0000 (14:10 +0000)
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

gcc/ada/ChangeLog
gcc/ada/exp_ch5.adb
gcc/testsuite/ChangeLog
gcc/testsuite/gnat.dg/iter2.adb [new file with mode: 0644]
gcc/testsuite/gnat.dg/iter2.ads [new file with mode: 0644]

index d041f5620431c337d84af557fd7dbf8aa4f252a9..bff06e6be436213eff682bb4689b9d6b729fe2f2 100644 (file)
@@ -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.
index e0cff915bca95334ee54c1f9af4f9c2f05a737e6..7371ee33acb6648da6e24e192f3acb0993f103cd 100644 (file)
@@ -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))),
index 57c599742592c594245f1043a3ff7a0bd48a7004..f73096e0f30e8c4fb9192b980639d190a69457b4 100644 (file)
@@ -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 (file)
index 0000000..e5819a0
--- /dev/null
@@ -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 (file)
index 0000000..2178630
--- /dev/null
@@ -0,0 +1,5 @@
+package Iter2
+   with SPARK_Mode
+is
+   function To_String (Name : String) return String;
+end Iter2;