diff mbox series

[COMMITTED] ada: Cannot reference ghost entity in class-wide precondition

Message ID 20230103093514.76112-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Cannot reference ghost entity in class-wide precondition |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès Jan. 3, 2023, 9:35 a.m. UTC 
  From: Javier Miranda <miranda@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/ghost.adb | 10 ++++++++++
 1 file changed, 10 insertions(+)
diff mbox series

Patch

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 0f03285b024..0d2a23dc042 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.