diff options
| author | Viljar Indus <indus@adacore.com> | 2025-09-10 12:47:19 +0300 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2025-11-18 16:05:09 +0100 |
| commit | b666b1c3f27c3d8751d5d902389fa05d7ea4a8d2 (patch) | |
| tree | 48d9bc390c7747e7c04d046acbf76ddf369ca1ab /libjava/classpath/java/io/FileNotFoundException.java | |
| parent | 3b5c0c0f3acf9cab725381484a7c2d0bf65c7456 (diff) | |
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.
Diffstat (limited to 'libjava/classpath/java/io/FileNotFoundException.java')
0 files changed, 0 insertions, 0 deletions