]> git.ipfire.org Git - thirdparty/gcc.git/commit
ada: Add rule check for call arguments
authorViljar Indus <indus@adacore.com>
Wed, 10 Sep 2025 09:47:19 +0000 (12:47 +0300)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Tue, 18 Nov 2025 15:05:09 +0000 (16:05 +0100)
commitb666b1c3f27c3d8751d5d902389fa05d7ea4a8d2
tree48d9bc390c7747e7c04d046acbf76ddf369ca1ab
parent3b5c0c0f3acf9cab725381484a7c2d0bf65c7456
ada: Add rule check for call arguments

Implement SPARK RM 6.9(18).

If an assignment to a part of a ghost variable occurs in a ghost entity,
then the variable should be assertion-level-dependent on this entity.
[This includes both assignment statements and passing a ghost variable as an
out or in out mode actual parameter.]

gcc/ada/ChangeLog:

* ghost.adb (Check_Procedure_Call_Levels): New function for
implementing the check.
* ghost.ads (Check_Procedure_Call_Levels): Likewise.
* sem_ch6.adb (Analyze_Procedure_Call): Check the levels after
the call has been resolved and the previous ghost region has
been restored.
gcc/ada/ghost.adb
gcc/ada/ghost.ads
gcc/ada/sem_ch6.adb