projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5fc2669) | patch
[Ada] Support access types in GNATprove
authorYannick Moy <moy@adacore.com>
Tue, 11 Dec 2018 11:10:12 +0000 (11:10 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 11 Dec 2018 11:10:12 +0000 (11:10 +0000)
commit0b8ff545ed09781fdbe20f1a6b9388db9b912a3c
tree4372a99ed7ae99461a235a89e3437887d70aaa43tree
parent5fc26697366abd160c4e755b6fe25c778ac97784commit | diff
[Ada] Support access types in GNATprove

SPARK RM has been updated to support access types in SPARK. Part of this
support is that now SPARK RM 3.1 lists access types as having full
default initialization. Now updated.

There is no impact on compilation.

2018-12-11  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_util.adb (Has_Full_Default_Initialization): Consider
access types as having full default initialization.

From-SVN: r266990
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_util.adb diff | blob | history