[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  <schonberg@adacore.com>

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c661a3832ddfa840b1f65549ba1a24e6719968e4..99b551f1d0cb4f8bb4fa6a0e55d079cf51e813e5 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-14  Ed Schonberg  <schonberg@adacore.com>
+
+       * exp_ch4.adb (Expand_N_Quantified_Expression): Freeze
+       explicitly the type of the loop parameter.
+
 2019-08-14  Javier Miranda  <miranda@adacore.com>
 
        * 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 4404c5dca9da406107fd0a3ed1274602691a1cd6..00f9aae51a3ee63cbbe438b9e9d06f291f58437f 100644 (file)
--- 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 6b71b95ba3a5a57ba19a734fccf5e4ed76e40872..9923987ec42df71bbff52ec871583de09366f130 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2019-08-14  Ed Schonberg  <schonberg@adacore.com>
+
+       * gnat.dg/assert2.adb, gnat.dg/assert2.ads: New testcase.
+
 2019-08-14  Eric Botcazou  <ebotcazou@adacore.com>
 
        * 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 (file)
index 0000000..1328004
--- /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 (file)
index 0000000..adf9b92
--- /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;