From 930b81af5b0207585819ea9988a0f50d009940a7 Mon Sep 17 00:00:00 2001 From: Javier Miranda Date: Mon, 28 Nov 2022 09:15:54 +0000 Subject: [PATCH] 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. --- gcc/ada/ghost.adb | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 0f03285b0241..0d2a23dc0425 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. -- 2.47.2