mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-01-11 10:05:02 +08:00
Code Issues Packages Projects Releases Wiki Activity

ada: Cannot reference ghost entity in class-wide precondition

Browse Source 
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.
This commit is contained in:
Javier Miranda 2022-11-28 09:15:54 +00:00 committed by Marc Poulhiès
parent e1e2b00703
commit 930b81af5b
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
gcc/ada/ghost.adb
View File

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