]> git.ipfire.org Git - thirdparty/gcc.git/commit
ada: Update of SPARK RM legality rules on ghost code
authorYannick Moy <moy@adacore.com>
Fri, 2 Feb 2024 17:20:06 +0000 (18:20 +0100)
committerMarc Poulhiès <poulhies@adacore.com>
Tue, 14 May 2024 08:19:50 +0000 (10:19 +0200)
commitdf48963b9553a51023c0d115bdf6205309e04bfe
tree5e8ed8d6ba931aedfab087b456a47bdfed6dbdc3
parent20dfaae2d1ba4749db13792105a32c5d8ef422e3
ada: Update of SPARK RM legality rules on ghost code

Update checking of ghost code after a small change in SPARK RM
rules 6.9(15) and 6.9(20), so that the Ghost assertion policy
that matters when checking the validity of a reference to a ghost entity
in an assertion expression is the Ghost assertion policy at the point
of declaration of the entity.

Also fix references to SPARK RM rules in comments, which were off by two
in many cases after the insertion of rules 13 and 14 regarding generic
instantiations.

gcc/ada/

* contracts.adb: Fix references to SPARK RM rules.
* freeze.adb: Same.
* ghost.adb: Fix references to SPARK RM rules.
(Check_Ghost_Context): Update checking of references to
ghost entities in assertion expressions.
* sem_ch6.adb: Fix references to SPARK RM rules.
* sem_prag.adb: Same.
gcc/ada/contracts.adb
gcc/ada/freeze.adb
gcc/ada/ghost.adb
gcc/ada/sem_ch6.adb
gcc/ada/sem_prag.adb