From: pmderodat Date: Tue, 11 Dec 2018 11:10:17 +0000 (+0000) Subject: [Ada] GNATprove: improve proofs for uninitialized constrained objects X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=81262845c3a4c3cd1412471c8958a72926f1f53e;p=thirdparty%2Fgcc.git [Ada] GNATprove: improve proofs for uninitialized constrained objects 2018-12-11 Ed Schonberg 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 4713510d848d..827ac096daca 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-12-11 Ed Schonberg + + * 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 * sem_util.adb (Has_Full_Default_Initialization): Consider diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 72dfd457e9e8..57e97fe61b1a 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,