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 0f03285b024174acac0d690e2bc1a97800c9e190..0d2a23dc04252882d77d813d5047688ce15d22d3 100644 (file)
--- 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.