]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89b4aa1) | patch
ada: Add Assertion_Policy checks for assertion levels
authorViljar Indus <indus@adacore.com>
Tue, 2 Sep 2025 10:11:30 +0000 (13:11 +0300)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Mon, 15 Sep 2025 12:59:31 +0000 (14:59 +0200)
commit33f64b23787acff88f0970715342fa8e797016c5
treeb3a694dd8e276b8fd2e872f0ca114269c4e97e54tree
parent89b4aa18ca581cdb11f07d60d7ac05a7e556281ccommit | diff
ada: Add Assertion_Policy checks for assertion levels

Implement SPARK RM 6.9(19) check:

An Assertion_Policy pragma specifying an Assertion_Level policy shall not occur
within a ghost subprogram or package associated to an assertion level which depends
on this level.

gcc/ada/ChangeLog:

* sem_prag.adb (Analyze_Pragma): Add ghost level check to
Assertion_Policy.
gcc/ada/sem_prag.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git