]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a688a02) | patch
ada: Fix checking of SPARK RM on ghost with concurrent part
authorYannick Moy <moy@adacore.com>
Mon, 27 May 2024 10:06:47 +0000 (12:06 +0200)
committerMarc Poulhiès <poulhies@adacore.com>
Thu, 20 Jun 2024 08:50:58 +0000 (10:50 +0200)
commit4c98b695fd8ee8246d84ba954dd59ddb87ac16d7
tree0f658dad85de347885ac1d2e6a960f8c8c9cd760tree
parenta688a0281946b1cc11333ca548db031a9aa0e9fdcommit | diff
ada: Fix checking of SPARK RM on ghost with concurrent part

SPARK RM 6.9(21) forbids a ghost type to have concurrent parts.
This was not enforced, instead only the type itself was checked to
be concurrent. Now fixed.

gcc/ada/

* ghost.adb (Check_Ghost_Type): Fix checking.
gcc/ada/ghost.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git