--- gcc/ada/sem_ch4.adb
+++ 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,

--- /dev/null
new file mode 100644
+++ 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;

--- /dev/null
new file mode 100644
+++ 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;