From 60c14ec73cb0a9fbff8e49e4a94f8b59236225e0 Mon Sep 17 00:00:00 2001 From: Ed Schonberg Date: Tue, 11 Dec 2018 11:10:17 +0000 Subject: [PATCH] [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. From-SVN: r266991 --- gcc/ada/ChangeLog | 7 +++++++ gcc/ada/sem_ch4.adb | 7 +++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 4713510..827ac09 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 72dfd45..57e97fe 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, -- 2.7.4