[Ada] Avoid crash in GNATprove_Mode on allocator inside type

In the special mode for GNATprove, subtypes should be declared for
allocators when constraints are used. This was done previously but it
does not work inside spec expressions, as the declaration is not
inserted and analyzed in the AST in that case, leading to a later crash
on an incomplete entity. Thus, no declaration should be created in such
a case, letting GNATprove later reject such code due to the use of an
allocator in an interfering context.

2019-08-13  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_ch4.adb (Analyze_Allocator): Do not insert subtype
	declaration for allocator inside a spec expression.

gcc/testsuite/

	* gnat.dg/allocator2.adb, gnat.dg/allocator2.ads: New testcase.

From-SVN: r274345

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 55044f6e200f49b4ab2dd2b0b81b2c0222ad0dff..920650b9010d01192a9fddf9de250d4aea0a6cf9 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-13  Yannick Moy  <moy@adacore.com>
+
+       * sem_ch4.adb (Analyze_Allocator): Do not insert subtype
+       declaration for allocator inside a spec expression.
+
 2019-08-13  Yannick Moy  <moy@adacore.com>
 
        * sem_res.adb (Resolve_Call): Do not inline calls inside record

diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index c049f9db5883b853ea166f662e8bf8e07442d206..627257875ddfb195d9d8a196b31bda28d547fc37 100644 (file)
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -676,9 +676,15 @@ package body Sem_Ch4 is
 
                --  In GNATprove mode we need to preserve the link between
                --  the original subtype indication and the anonymous subtype,
-               --  to extend proofs to constrained acccess types.
-
-               if Expander_Active or else GNATprove_Mode then
+               --  to extend proofs to constrained acccess types. We only do
+               --  that outside of spec expressions, otherwise the declaration
+               --  cannot be inserted and analyzed. In such a case, GNATprove
+               --  later rejects the allocator as it is not used here in
+               --  a non-interfering context (SPARK 4.8(2) and 7.1.3(12)).
+
+               if Expander_Active
+                 or else (GNATprove_Mode and then not In_Spec_Expression)
+               then
                   Def_Id := Make_Temporary (Loc, 'S');
 
                   Insert_Action (E,

diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 3ae70d6ee5a17a6429dad8dd1d24d733edf8b8eb..0c5d9485dfbfab735a250b4ad7ad126d6dd01a62 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2019-08-13  Yannick Moy  <moy@adacore.com>
+
+       * gnat.dg/allocator2.adb, gnat.dg/allocator2.ads: New testcase.
+
 2019-08-13  Eric Botcazou  <ebotcazou@adacore.com>
 
        * gnat.dg/generic_inst9.adb, gnat.dg/generic_inst9.ads,

diff --git a/gcc/testsuite/gnat.dg/allocator2.adb b/gcc/testsuite/gnat.dg/allocator2.adb
new file mode 100644 (file)
index 0000000..495efd3
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/allocator2.adb
@@ -0,0 +1,6 @@
+--  { dg-do compile }
+--  { dg-options "-gnatd.F" }
+
+package body Allocator2 is
+   procedure Dummy is null;
+end Allocator2;

diff --git a/gcc/testsuite/gnat.dg/allocator2.ads b/gcc/testsuite/gnat.dg/allocator2.ads
new file mode 100644 (file)
index 0000000..7c4c228
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/allocator2.ads
@@ -0,0 +1,15 @@
+pragma SPARK_Mode;
+package Allocator2 is
+    type Nat_Array is array (Positive range <>) of Natural with
+      Default_Component_Value => 0;
+    type Nat_Stack (Max : Natural) is record
+       Content : Nat_Array (1 .. Max);
+    end record;
+    type Stack_Acc is access Nat_Stack;
+    type My_Rec is private;
+private
+    type My_Rec is record
+       My_Stack : Stack_Acc := new Nat_Stack (Max => 10);
+    end record;
+   procedure Dummy;
+end Allocator2;