diff options
| author | Javier Miranda <miranda@adacore.com> | 2022-11-28 09:15:54 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-01-03 10:29:52 +0100 |
| commit | 930b81af5b0207585819ea9988a0f50d009940a7 (patch) | |
| tree | cf407e9393fa07c2afb249ff8f629e1911565d3b | |
| parent | e1e2b0070302169fbf3f3fd95a13ec819e71e2a5 (diff) | |
| download | gcc-930b81af5b0207585819ea9988a0f50d009940a7.zip gcc-930b81af5b0207585819ea9988a0f50d009940a7.tar.gz gcc-930b81af5b0207585819ea9988a0f50d009940a7.tar.bz2 | |
ada: Cannot reference ghost entity in class-wide precondition
gcc/ada/
* ghost.adb (Is_OK_Declaration): A reference to a Ghost entity may
appear within the class-wide precondition of a helper subprogram.
This context is treated as suitable because it was already
verified when we were analyzing the original class-wide
precondition.
| -rw-r--r-- | gcc/ada/ghost.adb | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 0f03285..0d2a23d 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -261,6 +261,16 @@ package body Ghost is then return True; + -- A reference to a Ghost entity may appear within the class-wide + -- precondition of a helper subprogram. This context is treated + -- as suitable because it was already verified when we were + -- analyzing the original class-wide precondition. + + elsif Is_Subprogram (Current_Scope) + and then Present (Class_Preconditions_Subprogram (Current_Scope)) + then + return True; + -- References to Ghost entities may be relocated in internally -- generated bodies. |