From 16b9e3c32d0c52334644021e5e0465b1c43d190e Mon Sep 17 00:00:00 2001 From: Ed Schonberg Date: Wed, 14 Aug 2019 09:51:34 +0000 Subject: [PATCH] [Ada] Crash on quantified expression in disabled assertion The defining identifier of a quantified expression may be the freeze point of its type. If the quantified expression appears in an assertion that is disavbled, the freeze node for that type may appear in a tree that will be discarded when the enclosing pragma is elaborated. To ensure that the freeze node is reachable for subsquent uses we must generate its freeze node explicitly when the quantified expression is analyzed. 2019-08-14 Ed Schonberg gcc/ada/ * exp_ch4.adb (Expand_N_Quantified_Expression): Freeze explicitly the type of the loop parameter. gcc/testsuite/ * gnat.dg/assert2.adb, gnat.dg/assert2.ads: New testcase. From-SVN: r274456 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/exp_ch4.adb | 22 ++++++++++++++++++++++ gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/assert2.adb | 5 +++++ gcc/testsuite/gnat.dg/assert2.ads | 15 +++++++++++++++ 5 files changed, 51 insertions(+) create mode 100644 gcc/testsuite/gnat.dg/assert2.adb create mode 100644 gcc/testsuite/gnat.dg/assert2.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c661a3832dd..99b551f1d0c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-08-14 Ed Schonberg + + * exp_ch4.adb (Expand_N_Quantified_Expression): Freeze + explicitly the type of the loop parameter. + 2019-08-14 Javier Miranda * sem_util.adb (New_Copy_Tree.Copy_Node_With_Replacement): diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 4404c5dca9d..00f9aae51a3 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -10337,8 +10337,30 @@ package body Exp_Ch4 is Flag : Entity_Id; Scheme : Node_Id; Stmts : List_Id; + Var : Entity_Id; begin + -- Ensure that the bound variable is properly frozen. We must do + -- this before expansion because the expression is about to be + -- converted into a loop, and resulting freeze nodes may end up + -- in the wrong place in the tree. + + if Present (Iter_Spec) then + Var := Defining_Identifier (Iter_Spec); + else + Var := Defining_Identifier (Loop_Spec); + end if; + + declare + P : Node_Id := Parent (N); + begin + while Nkind (P) in N_Subexpr loop + P := Parent (P); + end loop; + + Freeze_Before (P, Etype (Var)); + end; + -- Create the declaration of the flag which tracks the status of the -- quantified expression. Generate: diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 6b71b95ba3a..9923987ec42 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2019-08-14 Ed Schonberg + + * gnat.dg/assert2.adb, gnat.dg/assert2.ads: New testcase. + 2019-08-14 Eric Botcazou * gnat.dg/inline18.adb, gnat.dg/inline18.ads, diff --git a/gcc/testsuite/gnat.dg/assert2.adb b/gcc/testsuite/gnat.dg/assert2.adb new file mode 100644 index 00000000000..1328004ec75 --- /dev/null +++ b/gcc/testsuite/gnat.dg/assert2.adb @@ -0,0 +1,5 @@ +-- { dg-do compile } + +package body Assert2 is + procedure Dummy is null; +end Assert2; diff --git a/gcc/testsuite/gnat.dg/assert2.ads b/gcc/testsuite/gnat.dg/assert2.ads new file mode 100644 index 00000000000..adf9b921218 --- /dev/null +++ b/gcc/testsuite/gnat.dg/assert2.ads @@ -0,0 +1,15 @@ +package Assert2 + with SPARK_Mode +is + type Living is new Integer; + function Is_Martian (Unused : Living) return Boolean is (False); + + function Is_Green (Unused : Living) return Boolean is (True); + + pragma Assert + (for all M in Living => (if Is_Martian (M) then Is_Green (M))); + pragma Assert + (for all M in Living => (if Is_Martian (M) then not Is_Green (M))); + + procedure Dummy; +end Assert2; -- 2.30.2