diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4713510d848..827ac096dac 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-12-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Analyze_Allocator): In GNATprove mode build a
+	subtype declaration if the allocator has a subtype indication
+	with a constraint. This allows additional proofs to be applied
+	to allocators that designate uninitialized constrained objects.
+
 2018-12-11  Yannick Moy  <moy@adacore.com>
 
 	* sem_util.adb (Has_Full_Default_Initialization): Consider
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 72dfd457e9e..57e97fe61b1 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -171,7 +171,6 @@ package body Sem_Ch4 is
    --  being called. The caller will have verified that the object is legal
    --  for the call. If the remaining parameters match, the first parameter
    --  will rewritten as a dereference if needed, prior to completing analysis.
-
    procedure Check_Misspelled_Selector
      (Prefix : Entity_Id;
       Sel    : Node_Id);
@@ -675,7 +674,11 @@ package body Sem_Ch4 is
                   return;
                end if;
 
-               if Expander_Active then
+               --  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
                   Def_Id := Make_Temporary (Loc, 'S');
 
                   Insert_Action (E,