diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -365,6 +365,17 @@ package body Ghost is if Is_Ghost_Pragma (Prag) then return True; + -- A pragma may not be analyzed, so that its Ghost status is + -- not determined yet, but it is guaranteed to be Ghost when + -- referencing a Ghost entity. + + elsif Prag_Nam in Name_Annotate + | Name_Compile_Time_Error + | Name_Compile_Time_Warning + | Name_Unreferenced + then + return True; + -- An assertion expression pragma is Ghost when it contains a -- reference to a Ghost entity (SPARK RM 6.9(10)), except for -- predicate pragmas (SPARK RM 6.9(11)). @@ -444,14 +455,6 @@ package body Ghost is if Ghost_Mode > None then return True; - -- A Ghost type may be referenced in a use_type clause - -- (SPARK RM 6.9.10). - - elsif Present (Parent (Context)) - and then Nkind (Parent (Context)) = N_Use_Type_Clause - then - return True; - -- Routine Expand_Record_Extension creates a parent subtype without -- inserting it into the tree. There is no good way of recognizing -- this special case as there is no parent. Try to approximate the @@ -482,6 +485,46 @@ package body Ghost is then return True; + -- A Ghost type may be referenced in a use or use_type clause + -- (SPARK RM 6.9(10)). + + elsif Present (Parent (Par)) + and then Nkind (Parent (Par)) in N_Use_Package_Clause + | N_Use_Type_Clause + then + return True; + + -- The context is an attribute definition clause for a Ghost + -- entity. + + elsif Nkind (Parent (Par)) = N_Attribute_Definition_Clause + and then Par = Name (Parent (Par)) + then + return True; + + -- The context is the instantiation or renaming of a Ghost + -- entity. + + elsif Nkind (Parent (Par)) in N_Generic_Instantiation + | N_Renaming_Declaration + | N_Generic_Renaming_Declaration + and then Par = Name (Parent (Par)) + then + return True; + + -- In the context of an instantiation, accept currently Ghost + -- arguments for formal subprograms, as SPARK does not provide + -- a way to distinguish Ghost formal parameters from non-Ghost + -- ones. Illegal use of such arguments in a non-Ghost context + -- will lead to errors inside the instantiation. + + elsif Nkind (Parent (Par)) = N_Generic_Association + and then (Nkind (Par) in N_Has_Entity + and then Present (Entity (Par)) + and then Is_Subprogram (Entity (Par))) + then + return True; + elsif Is_OK_Declaration (Par) then return True; @@ -593,6 +636,13 @@ package body Ghost is return; end if; + -- When assertions are enabled, compiler generates code for ghost + -- entities, that is not subject to Ghost policy. + + if not Comes_From_Source (Ghost_Ref) then + return; + end if; + -- Once it has been established that the reference to the Ghost entity -- is within a suitable context, ensure that the policy at the point of -- declaration and at the point of use match. diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb --- a/gcc/ada/sem_ch2.adb +++ b/gcc/ada/sem_ch2.adb @@ -26,6 +26,7 @@ with Atree; use Atree; with Einfo; use Einfo; with Einfo.Utils; use Einfo.Utils; +with Ghost; use Ghost; with Namet; use Namet; with Opt; use Opt; with Restrict; use Restrict; @@ -34,6 +35,7 @@ with Sem_Ch8; use Sem_Ch8; with Sem_Dim; use Sem_Dim; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; +with Sinfo.Utils; use Sinfo.Utils; with Stand; use Stand; with Uintp; use Uintp; @@ -77,6 +79,18 @@ package body Sem_Ch2 is Find_Direct_Name (N); end if; + -- A Ghost entity must appear in a specific context. Only do this + -- checking on non-overloaded expressions, as otherwise we need to + -- wait for resolution, and the checking is done in Resolve_Entity_Name. + + if Nkind (N) in N_Expanded_Name | N_Identifier + and then Present (Entity (N)) + and then Is_Ghost_Entity (Entity (N)) + and then not Is_Overloaded (N) + then + Check_Ghost_Context (Entity (N), N); + end if; + Analyze_Dimension (N); end Analyze_Identifier; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2119,6 +2119,13 @@ package body Sem_Ch5 is Mutate_Ekind (Id, E_Label); Set_Etype (Id, Standard_Void_Type); Set_Enclosing_Scope (Id, Current_Scope); + + -- A label declared within a Ghost region becomes Ghost (SPARK RM + -- 6.9(2)). + + if Ghost_Mode > None then + Set_Is_Ghost_Entity (Id); + end if; end Analyze_Implicit_Label_Declaration; ------------------------------