diff options
| author | Ed Schonberg <schonberg@adacore.com> | 2018-12-11 11:10:17 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-12-11 11:10:17 +0000 |
| commit | 60c14ec73cb0a9fbff8e49e4a94f8b59236225e0 (patch) | |
| tree | f238fb80c1d51a486c9c9f67178cceee43b987d8 /gcc | |
| parent | 0b8ff545ed09781fdbe20f1a6b9388db9b912a3c (diff) | |
| download | gcc-60c14ec73cb0a9fbff8e49e4a94f8b59236225e0.zip gcc-60c14ec73cb0a9fbff8e49e4a94f8b59236225e0.tar.gz gcc-60c14ec73cb0a9fbff8e49e4a94f8b59236225e0.tar.bz2 | |
[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.
From-SVN: r266991
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | 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 <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 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, |