[Ada] GNATprove: improve proofs for uninitialized constrained objects

2018-12-11  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* 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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@266991 138bc75d-0d04-0410-961f-82ee72b054a4

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4713510d848db00cfa92e2a7a17509acfdd43470..827ac096daca5f60c88231e7e6d6dbcc2f16b1ba 100644 (file)
--- 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 72dfd457e9e87018b6562ce8f79e30a4962c04b7..57e97fe61b1a3168890ae3beb73dd5701476a0d4 100644 (file)
--- 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,