]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0a32656) | patch
ada: Update the condition for ghost call arguments
authorViljar Indus <indus@adacore.com>
Tue, 9 Sep 2025 12:00:56 +0000 (15:00 +0300)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Mon, 29 Sep 2025 09:43:37 +0000 (11:43 +0200)
commit840899585a23ae346235035aca4842b3d1358180
tree1f099cf5fb38c3d03088301bb2da07fdf2f2b6e7tree | snapshot
parent0a32656dc3efd67aa1ec8b6543867fc8262c2da6commit | diff
ada: Update the condition for ghost call arguments

The SPARK RM specifies that the levels between the argument and
the call shall have the same level.

gcc/ada/ChangeLog:

* ghost.adb (Check_Procedure_Call_Policies): Update the check
between the levels of the argument and the call.
gcc/ada/ghost.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git