projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0b8ff54) | patch
[Ada] GNATprove: improve proofs for uninitialized constrained objects
authorEd Schonberg <schonberg@adacore.com>
Tue, 11 Dec 2018 11:10:17 +0000 (11:10 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 11 Dec 2018 11:10:17 +0000 (11:10 +0000)
commit60c14ec73cb0a9fbff8e49e4a94f8b59236225e0
treef238fb80c1d51a486c9c9f67178cceee43b987d8tree
parent0b8ff545ed09781fdbe20f1a6b9388db9b912a3ccommit | diff
[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
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_ch4.adb diff | blob | history