projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bc1146e) | patch
[Ada] Skip code not in SPARK for ownership analysis
authorYannick Moy <moy@adacore.com>
Thu, 4 Jul 2019 08:05:45 +0000 (08:05 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 4 Jul 2019 08:05:45 +0000 (08:05 +0000)
commit3d53efa6921534027dbe5d408ac274736dc43d9c
treecbe1337290a3094b40be86882efc5619e8258685tree
parentbc1146e5e0979421b5dc2c9c005c355443c2fe24commit | diff
[Ada] Skip code not in SPARK for ownership analysis

Ownership rules for pointer support should only apply to code marked in
SPARK. There is no impact on compilation.

2019-07-04  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_spark.adb (Check_Package_Spec, Check_Package_Body): Only
analyze parts of the code marked in SPARK.

From-SVN: r273052
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_spark.adb diff | blob | history