]> git.ipfire.org Git - thirdparty/gcc.git/commit - gcc/ada/sem_spark.ads
[Ada] SPARK support for pointers through ownership
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Mon, 1 Jul 2019 13:37:21 +0000 (13:37 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Mon, 1 Jul 2019 13:37:21 +0000 (13:37 +0000)
commitd087b9ca787d04fcfacfa41697ae6e0cf59e8794
tree46c2dd92b05281cafb8eb4cbb879a94e07e84387
parentfe48ee0a1a7a3f42268a344c3063fd0e234fe0ed
[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@272878 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb
gcc/ada/sem_spark.ads