projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a2902a6) | patch
[Ada] SPARK support for pointers through ownership
authorYannick Moy <moy@adacore.com>
Mon, 1 Jul 2019 13:37:21 +0000 (13:37 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 1 Jul 2019 13:37:21 +0000 (13:37 +0000)
commit497ee82ba3b1f9e9154d978022ca51c88e49003e
tree46c2dd92b05281cafb8eb4cbb879a94e07e84387tree | snapshot
parenta2902a6f2347f480952b53f08d7868afc8116071commit | diff
[Ada] SPARK support for pointers through ownership

SPARK RM 3.10 is the final version of the pointer ownership rules. Start
changing the implementation accordingly. Anonymous access types are not
fully supported yet.

There is no impact on compilation.

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

gcc/ada/

* sem_spark.adb: Completely rework the algorithm for ownership
checking, as the rules in SPARK RM have changed a lot.
* sem_spark.ads: Update comments.

From-SVN: r272878
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_spark.adb diff | blob | history
gcc/ada/sem_spark.ads diff | blob | history
Domain: System / Toolchain;