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