From a3b7645bffbaf3dadf1f9cfccd93c6fba3e0834d Mon Sep 17 00:00:00 2001 From: Javier Miranda Date: Mon, 16 Jul 2018 14:10:27 +0000 Subject: [PATCH] [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 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 | 6 ++++++ gcc/ada/exp_ch5.adb | 11 ++++++++--- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/iter2.adb | 28 ++++++++++++++++++++++++++++ gcc/testsuite/gnat.dg/iter2.ads | 5 +++++ 5 files changed, 51 insertions(+), 3 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/iter2.adb create mode 100644 gcc/testsuite/gnat.dg/iter2.ads 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 + + * 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 * 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 + + * gnat.dg/iter2.adb, gnat.dg/iter2.ads: New testcase. + 2018-07-16 Richard Biener 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, ""); + 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; -- 2.30.2