From: Javier Miranda <miranda@adacore.com>
Date: Mon, 28 Nov 2022 09:15:54 +0000 (+0000)
Subject: ada: Cannot reference ghost entity in class-wide precondition
X-Git-Tag: basepoints/gcc-14~2248
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=930b81af5b0207585819ea9988a0f50d009940a7;p=thirdparty%2Fgcc.git

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.
---

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.