1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
9 -- Copyright (C) 2014-2024, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
27 with Aspects
; use Aspects
;
28 with Atree
; use Atree
;
29 with Einfo
; use Einfo
;
30 with Einfo
.Entities
; use Einfo
.Entities
;
31 with Einfo
.Utils
; use Einfo
.Utils
;
32 with Elists
; use Elists
;
33 with Errout
; use Errout
;
34 with Nlists
; use Nlists
;
35 with Nmake
; use Nmake
;
37 with Sem_Aux
; use Sem_Aux
;
38 with Sem_Disp
; use Sem_Disp
;
39 with Sem_Eval
; use Sem_Eval
;
40 with Sem_Prag
; use Sem_Prag
;
41 with Sem_Res
; use Sem_Res
;
42 with Sem_Util
; use Sem_Util
;
43 with Sinfo
; use Sinfo
;
44 with Sinfo
.Nodes
; use Sinfo
.Nodes
;
45 with Sinfo
.Utils
; use Sinfo
.Utils
;
46 with Snames
; use Snames
;
55 -- The following table contains all ignored Ghost nodes that must be
56 -- eliminated from the tree by routine Remove_Ignored_Ghost_Code.
58 package Ignored_Ghost_Nodes
is new Table
.Table
(
59 Table_Component_Type
=> Node_Id
,
60 Table_Index_Type
=> Int
,
62 Table_Initial
=> Alloc
.Ignored_Ghost_Nodes_Initial
,
63 Table_Increment
=> Alloc
.Ignored_Ghost_Nodes_Increment
,
64 Table_Name
=> "Ignored_Ghost_Nodes");
66 -----------------------
67 -- Local subprograms --
68 -----------------------
70 function Whole_Object_Ref
(Ref
: Node_Id
) return Node_Id
;
71 -- For a name that denotes an object, returns a name that denotes the whole
72 -- object, declared by an object declaration, formal parameter declaration,
73 -- etc. For example, for P.X.Comp (J), if P is a package X is a record
74 -- object, this returns P.X.
76 function Ghost_Entity
(Ref
: Node_Id
) return Entity_Id
;
77 pragma Inline
(Ghost_Entity
);
78 -- Obtain the entity of a Ghost entity from reference Ref. Return Empty if
79 -- no such entity exists.
81 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
);
82 pragma Inline
(Install_Ghost_Mode
);
83 -- Install Ghost mode Mode as the Ghost mode in effect
85 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
);
86 pragma Inline
(Install_Ghost_Region
);
87 -- Install a Ghost region comprised of mode Mode and ignored region start
90 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean;
91 -- Determine whether declaration or body N is subject to aspect or pragma
92 -- Ghost. This routine must be used in cases where pragma Ghost has not
93 -- been analyzed yet, but the context needs to establish the "ghostness"
96 procedure Mark_Ghost_Declaration_Or_Body
99 -- Mark the defining entity of declaration or body N as Ghost depending on
100 -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
103 procedure Record_Ignored_Ghost_Node
(N
: Node_Or_Entity_Id
);
104 -- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
105 -- later elimination.
107 ----------------------------
108 -- Check_Ghost_Completion --
109 ----------------------------
111 procedure Check_Ghost_Completion
112 (Prev_Id
: Entity_Id
;
113 Compl_Id
: Entity_Id
)
115 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
118 -- Nothing to do if one of the views is missing
120 if No
(Prev_Id
) or else No
(Compl_Id
) then
123 -- The Ghost policy in effect at the point of declaration and at the
124 -- point of completion must match (SPARK RM 6.9(16)).
126 elsif Is_Checked_Ghost_Entity
(Prev_Id
)
127 and then Policy
= Name_Ignore
129 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
131 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
132 Error_Msg_N
("\& declared with ghost policy `Check`", Prev_Id
);
133 Error_Msg_N
("\& completed # with ghost policy `Ignore`", Prev_Id
);
135 elsif Is_Ignored_Ghost_Entity
(Prev_Id
)
136 and then Policy
= Name_Check
138 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
140 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
141 Error_Msg_N
("\& declared with ghost policy `Ignore`", Prev_Id
);
142 Error_Msg_N
("\& completed # with ghost policy `Check`", Prev_Id
);
144 end Check_Ghost_Completion
;
146 -------------------------
147 -- Check_Ghost_Context --
148 -------------------------
150 procedure Check_Ghost_Context
(Ghost_Id
: Entity_Id
; Ghost_Ref
: Node_Id
) is
151 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
);
152 -- Verify that the Ghost policy at the point of declaration of entity Id
153 -- matches the policy at the point of reference Ref. If this is not the
154 -- case emit an error at Ref.
156 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean;
157 -- Determine whether node Context denotes a Ghost-friendly context where
158 -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
160 function In_Aspect_Or_Pragma_Predicate
(N
: Node_Id
) return Boolean;
161 -- Return True iff N is enclosed in an aspect or pragma Predicate
163 -------------------------
164 -- Is_OK_Ghost_Context --
165 -------------------------
167 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean is
168 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean;
169 -- Determine whether node Decl is a suitable context for a reference
170 -- to a Ghost entity. To qualify as such, Decl must either
172 -- * Define a Ghost entity
174 -- * Be subject to pragma Ghost
176 function Is_OK_Pragma
(Prag
: Node_Id
; Id
: Entity_Id
) return Boolean;
177 -- Determine whether node Prag is a suitable context for a reference
178 -- to a Ghost entity Id. To qualify as such, Prag must either
180 -- * Be an assertion expression pragma
182 -- * Denote pragma Global, Depends, Initializes, Refined_Global,
183 -- Refined_Depends or Refined_State.
185 -- * Specify an aspect of a Ghost entity
187 -- * Contain a reference to a Ghost entity
189 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean;
190 -- Determine whether node Stmt is a suitable context for a reference
191 -- to a Ghost entity. To qualify as such, Stmt must either
193 -- * Denote a procedure call to a Ghost procedure
195 -- * Denote an assignment statement whose target is Ghost
197 -----------------------
198 -- Is_OK_Declaration --
199 -----------------------
201 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean is
202 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean;
203 -- Determine whether node N appears in the profile of a subprogram
206 --------------------------------
207 -- In_Subprogram_Body_Profile --
208 --------------------------------
210 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean is
211 Spec
: constant Node_Id
:= Parent
(N
);
214 -- The node appears in a parameter specification in which case
215 -- it is either the parameter type or the default expression or
216 -- the node appears as the result definition of a function.
219 (Nkind
(N
) = N_Parameter_Specification
221 (Nkind
(Spec
) = N_Function_Specification
222 and then N
= Result_Definition
(Spec
)))
223 and then Nkind
(Parent
(Spec
)) = N_Subprogram_Body
;
224 end In_Subprogram_Body_Profile
;
231 -- Start of processing for Is_OK_Declaration
234 if Is_Ghost_Declaration
(Decl
) then
239 -- A reference to a Ghost entity may appear within the profile of
240 -- a subprogram body. This context is treated as suitable because
241 -- it duplicates the context of the corresponding spec. The real
242 -- check was already performed during the analysis of the spec.
244 elsif In_Subprogram_Body_Profile
(Decl
) then
247 -- A reference to a Ghost entity may appear within an expression
248 -- function which is still being analyzed. This context is treated
249 -- as suitable because it is not yet known whether the expression
250 -- function is an initial declaration or a completion. The real
251 -- check is performed when the expression function is expanded.
253 elsif Nkind
(Decl
) = N_Expression_Function
254 and then not Analyzed
(Decl
)
258 -- A reference to a Ghost entity may appear within the class-wide
259 -- precondition of a helper subprogram. This context is treated
260 -- as suitable because it was already verified when we were
261 -- analyzing the original class-wide precondition.
263 elsif Is_Subprogram
(Current_Scope
)
264 and then Present
(Class_Preconditions_Subprogram
(Current_Scope
))
268 -- References to Ghost entities may be relocated in internally
271 elsif Nkind
(Decl
) = N_Subprogram_Body
272 and then not Comes_From_Source
(Decl
)
274 Subp_Id
:= Corresponding_Spec
(Decl
);
276 if Present
(Subp_Id
) then
278 -- The context is the internally built _Wrapped_Statements
279 -- procedure, which is OK because the real check was done
280 -- before contract expansion activities.
282 if Chars
(Subp_Id
) = Name_uWrapped_Statements
then
285 -- The context is the internally built predicate function,
286 -- which is OK because the real check was done before the
287 -- predicate function was generated.
289 elsif Is_Predicate_Function
(Subp_Id
) then
294 Original_Node
(Unit_Declaration_Node
(Subp_Id
));
296 -- The original context is an expression function that
297 -- has been split into a spec and a body. The context is
298 -- OK as long as the initial declaration is Ghost.
300 if Nkind
(Subp_Decl
) = N_Expression_Function
then
301 return Is_Ghost_Declaration
(Subp_Decl
);
305 -- Otherwise this is either an internal body or an internal
306 -- completion. Both are OK because the real check was done
307 -- before expansion activities.
315 end Is_OK_Declaration
;
321 function Is_OK_Pragma
(Prag
: Node_Id
; Id
: Entity_Id
) return Boolean
323 procedure Check_Policies
(Prag_Nam
: Name_Id
);
324 -- Verify that the Ghost policy in effect at the point of the
325 -- declaration of Ghost entity Id (if present) is the same as the
326 -- assertion policy for pragma name Prag_Nam. Emit an error if
327 -- this is not the case.
333 procedure Check_Policies
(Prag_Nam
: Name_Id
) is
334 AP
: constant Name_Id
:= Check_Kind
(Prag_Nam
);
337 -- If the Ghost policy in effect at the point of the
338 -- declaration of Ghost entity Id is Ignore, then the assertion
339 -- policy of the pragma must be Ignore (SPARK RM 6.9(20)).
342 and then not Is_Checked_Ghost_Entity
(Id
)
343 and then AP
/= Name_Ignore
346 ("incompatible ghost policies in effect",
349 ("\ghost entity & has policy `Ignore`",
350 Ghost_Ref
, Ghost_Id
);
352 Error_Msg_Name_1
:= AP
;
354 ("\assertion expression has policy %", Ghost_Ref
);
363 -- Start of processing for Is_OK_Pragma
366 if Nkind
(Prag
) = N_Pragma
then
367 Prag_Id
:= Get_Pragma_Id
(Prag
);
368 Prag_Nam
:= Original_Aspect_Pragma_Name
(Prag
);
370 -- A pragma that applies to a Ghost construct or specifies an
371 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
373 if Is_Ghost_Pragma
(Prag
) then
376 -- A pragma may not be analyzed, so that its Ghost status is
377 -- not determined yet, but it is guaranteed to be Ghost when
378 -- referencing a Ghost entity.
380 elsif Prag_Nam
in Name_Annotate
381 | Name_Compile_Time_Error
382 | Name_Compile_Time_Warning
387 -- An assertion expression pragma is Ghost when it contains a
388 -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
389 -- predicate pragmas (SPARK RM 6.9(11)).
391 elsif Assertion_Expression_Pragma
(Prag_Id
)
392 and then Prag_Id
/= Pragma_Predicate
394 -- Ensure that the assertion policy and the Ghost policy are
395 -- compatible (SPARK RM 6.9(20)).
397 Check_Policies
(Prag_Nam
);
400 -- Several pragmas that may apply to a non-Ghost entity are
401 -- treated as Ghost when they contain a reference to a Ghost
402 -- entity (SPARK RM 6.9(11)).
404 elsif Prag_Nam
in Name_Global
407 | Name_Refined_Global
408 | Name_Refined_Depends
418 ---------------------
419 -- Is_OK_Statement --
420 ---------------------
422 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean is
424 -- An assignment statement is Ghost when the target is a Ghost
427 if Nkind
(Stmt
) = N_Assignment_Statement
then
428 return Is_Ghost_Assignment
(Stmt
);
430 -- A procedure call is Ghost when it calls a Ghost procedure
432 elsif Nkind
(Stmt
) = N_Procedure_Call_Statement
then
433 return Is_Ghost_Procedure_Call
(Stmt
);
437 -- An if statement is a suitable context for a Ghost entity if it
438 -- is the byproduct of assertion expression expansion. Note that
439 -- the assertion expression may not be related to a Ghost entity,
440 -- but it may still contain references to Ghost entities.
442 elsif Nkind
(Stmt
) = N_If_Statement
443 and then Comes_From_Check_Or_Contract
(Stmt
)
455 -- Start of processing for Is_OK_Ghost_Context
458 -- The context is Ghost when it appears within a Ghost package or
461 if Ghost_Mode
> None
then
464 -- Routine Expand_Record_Extension creates a parent subtype without
465 -- inserting it into the tree. There is no good way of recognizing
466 -- this special case as there is no parent. Try to approximate the
469 elsif No
(Parent
(Context
)) and then Is_Tagged_Type
(Ghost_Id
) then
472 -- Otherwise climb the parent chain looking for a suitable Ghost
477 while Present
(Par
) loop
478 if Is_Ignored_Ghost_Node
(Par
) then
481 -- It is not possible to check correct use of Ghost entities
482 -- in generic instantiations until after the generic has been
483 -- resolved. Postpone that verification to after resolution.
485 elsif Nkind
(Par
) = N_Generic_Association
then
488 -- A reference to a Ghost entity can appear within an aspect
489 -- specification (SPARK RM 6.9(10)). The precise checking will
490 -- occur when analyzing the corresponding pragma. We make an
491 -- exception for predicate aspects other than Ghost_Predicate
492 -- that only allow referencing a Ghost entity when the
493 -- corresponding type declaration is Ghost (SPARK RM 6.9(11)).
495 elsif Nkind
(Par
) = N_Aspect_Specification
497 (Get_Aspect_Id
(Par
) = Aspect_Ghost_Predicate
498 or else not Same_Aspect
499 (Get_Aspect_Id
(Par
), Aspect_Predicate
))
503 -- A Ghost type may be referenced in a use or use_type clause
504 -- (SPARK RM 6.9(10)).
506 elsif Present
(Parent
(Par
))
507 and then Nkind
(Parent
(Par
)) in N_Use_Package_Clause
512 -- The context is an attribute definition clause for a Ghost
515 elsif Nkind
(Parent
(Par
)) = N_Attribute_Definition_Clause
516 and then Par
= Name
(Parent
(Par
))
520 -- The context is the instantiation or renaming of a Ghost
523 elsif Nkind
(Parent
(Par
)) in N_Generic_Instantiation
524 | N_Renaming_Declaration
525 | N_Generic_Renaming_Declaration
526 and then Par
= Name
(Parent
(Par
))
530 -- In the case of the renaming of a ghost object, the type
531 -- itself may be ghost.
533 elsif Nkind
(Parent
(Par
)) = N_Object_Renaming_Declaration
534 and then (Par
= Subtype_Mark
(Parent
(Par
))
535 or else Par
= Access_Definition
(Parent
(Par
)))
539 elsif Is_OK_Declaration
(Par
) then
542 elsif Is_OK_Pragma
(Par
, Ghost_Id
) then
545 elsif Is_OK_Statement
(Par
) then
548 -- Prevent the search from going too far
550 elsif Is_Body_Or_Package_Declaration
(Par
) then
557 -- The expansion of assertion expression pragmas and attribute Old
558 -- may cause a legal Ghost entity reference to become illegal due
559 -- to node relocation. Check the In_Assertion_Expr counter as last
560 -- resort to try and infer the original legal context.
562 if In_Assertion_Expr
> 0 then
565 -- Otherwise the context is not suitable for a reference to a
572 end Is_OK_Ghost_Context
;
574 ------------------------
575 -- Check_Ghost_Policy --
576 ------------------------
578 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
) is
579 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
582 -- The Ghost policy in effect a the point of declaration and at the
583 -- point of use must match (SPARK RM 6.9(15)).
585 if Is_Checked_Ghost_Entity
(Id
)
586 and then Policy
= Name_Ignore
587 and then Known_To_Be_Assigned
(Ref
)
589 Error_Msg_Sloc
:= Sloc
(Ref
);
591 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
592 Error_Msg_NE
("\& declared with ghost policy `Check`", Ref
, Id
);
593 Error_Msg_NE
("\& used # with ghost policy `Ignore`", Ref
, Id
);
595 elsif Is_Ignored_Ghost_Entity
(Id
) and then Policy
= Name_Check
then
596 Error_Msg_Sloc
:= Sloc
(Ref
);
598 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
599 Error_Msg_NE
("\& declared with ghost policy `Ignore`", Ref
, Id
);
600 Error_Msg_NE
("\& used # with ghost policy `Check`", Ref
, Id
);
602 end Check_Ghost_Policy
;
604 -----------------------------------
605 -- In_Aspect_Or_Pragma_Predicate --
606 -----------------------------------
608 function In_Aspect_Or_Pragma_Predicate
(N
: Node_Id
) return Boolean is
611 while Present
(Par
) loop
612 if Nkind
(Par
) = N_Pragma
613 and then Get_Pragma_Id
(Par
) = Pragma_Predicate
617 elsif Nkind
(Par
) = N_Aspect_Specification
618 and then Same_Aspect
(Get_Aspect_Id
(Par
), Aspect_Predicate
)
622 -- Stop the search when it's clear it cannot be inside an aspect
625 elsif Is_Declaration
(Par
)
626 or else Is_Statement
(Par
)
627 or else Is_Body
(Par
)
636 end In_Aspect_Or_Pragma_Predicate
;
638 -- Start of processing for Check_Ghost_Context
641 -- Class-wide pre/postconditions of ignored pragmas are preanalyzed
642 -- to report errors on wrong conditions; however, ignored pragmas may
643 -- also have references to ghost entities and we must disable checking
644 -- their context to avoid reporting spurious errors.
646 if Inside_Class_Condition_Preanalysis
then
650 -- When assertions are enabled, compiler generates code for ghost
651 -- entities, that is not subject to Ghost policy.
653 if not Comes_From_Source
(Ghost_Ref
) then
657 -- Once it has been established that the reference to the Ghost entity
658 -- is within a suitable context, ensure that the policy at the point of
659 -- declaration and at the point of use match.
661 if Is_OK_Ghost_Context
(Ghost_Ref
) then
662 if Present
(Ghost_Id
) then
663 Check_Ghost_Policy
(Ghost_Id
, Ghost_Ref
);
666 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
667 -- its behavior or value (SPARK RM 6.9(10,11)).
670 Error_Msg_N
("ghost entity cannot appear in this context", Ghost_Ref
);
672 -- When the Ghost entity appears in a pragma Predicate, explain the
673 -- reason for this being illegal, and suggest a fix instead.
675 if In_Aspect_Or_Pragma_Predicate
(Ghost_Ref
) then
677 ("\as predicates are checked in membership tests, "
678 & "the type and its predicate must be both ghost",
681 ("\either make the type ghost "
682 & "or use a Ghost_Predicate "
683 & "or use a type invariant on a private type", Ghost_Ref
);
686 end Check_Ghost_Context
;
688 ------------------------------------------------
689 -- Check_Ghost_Context_In_Generic_Association --
690 ------------------------------------------------
692 procedure Check_Ghost_Context_In_Generic_Association
696 function Emit_Error_On_Ghost_Reference
698 return Traverse_Result
;
699 -- Determine wether N denotes a reference to a ghost entity, and if so
702 -----------------------------------
703 -- Emit_Error_On_Ghost_Reference --
704 -----------------------------------
706 function Emit_Error_On_Ghost_Reference
708 return Traverse_Result
711 if Is_Entity_Name
(N
)
712 and then Present
(Entity
(N
))
713 and then Is_Ghost_Entity
(Entity
(N
))
715 Error_Msg_N
("ghost entity cannot appear in this context", N
);
716 Error_Msg_Sloc
:= Sloc
(Formal
);
717 Error_Msg_NE
("\formal & was not declared as ghost #", N
, Formal
);
722 end Emit_Error_On_Ghost_Reference
;
724 procedure Check_Ghost_References
is
725 new Traverse_Proc
(Emit_Error_On_Ghost_Reference
);
727 -- Start of processing for Check_Ghost_Context_In_Generic_Association
730 -- The context is ghost when it appears within a Ghost package or
733 if Ghost_Mode
> None
then
736 -- The context is ghost if Formal is explicitly marked as ghost
738 elsif Is_Ghost_Entity
(Formal
) then
742 Check_Ghost_References
(Actual
);
744 end Check_Ghost_Context_In_Generic_Association
;
746 ---------------------------------------------
747 -- Check_Ghost_Formal_Procedure_Or_Package --
748 ---------------------------------------------
750 procedure Check_Ghost_Formal_Procedure_Or_Package
754 Is_Default
: Boolean := False)
757 if not Is_Ghost_Entity
(Formal
) then
761 if Present
(Actual
) and then Is_Ghost_Entity
(Actual
) then
766 Error_Msg_N
("ghost procedure expected as default", N
);
767 Error_Msg_NE
("\formal & is declared as ghost", N
, Formal
);
770 if Ekind
(Formal
) = E_Procedure
then
771 Error_Msg_N
("ghost procedure expected for actual", N
);
773 Error_Msg_N
("ghost package expected for actual", N
);
776 Error_Msg_Sloc
:= Sloc
(Formal
);
777 Error_Msg_NE
("\formal & was declared as ghost #", N
, Formal
);
779 end Check_Ghost_Formal_Procedure_Or_Package
;
781 ---------------------------------
782 -- Check_Ghost_Formal_Variable --
783 ---------------------------------
785 procedure Check_Ghost_Formal_Variable
788 Is_Default
: Boolean := False)
790 Actual_Obj
: constant Entity_Id
:= Get_Enclosing_Deep_Object
(Actual
);
792 if not Is_Ghost_Entity
(Formal
) then
797 or else not Is_Ghost_Entity
(Actual_Obj
)
800 Error_Msg_N
("ghost object expected as default", Actual
);
801 Error_Msg_NE
("\formal & is declared as ghost", Actual
, Formal
);
803 Error_Msg_N
("ghost object expected for mutable actual", Actual
);
804 Error_Msg_Sloc
:= Sloc
(Formal
);
805 Error_Msg_NE
("\formal & was declared as ghost #", Actual
, Formal
);
808 end Check_Ghost_Formal_Variable
;
810 ----------------------------
811 -- Check_Ghost_Overriding --
812 ----------------------------
814 procedure Check_Ghost_Overriding
816 Overridden_Subp
: Entity_Id
)
818 Deriv_Typ
: Entity_Id
;
819 Over_Subp
: Entity_Id
;
822 if Present
(Subp
) and then Present
(Overridden_Subp
) then
823 Over_Subp
:= Ultimate_Alias
(Overridden_Subp
);
824 Deriv_Typ
:= Find_Dispatching_Type
(Subp
);
826 -- A Ghost primitive of a non-Ghost type extension cannot override an
827 -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
829 if Is_Ghost_Entity
(Subp
)
830 and then Present
(Deriv_Typ
)
831 and then not Is_Ghost_Entity
(Deriv_Typ
)
832 and then not Is_Ghost_Entity
(Over_Subp
)
833 and then not Is_Abstract_Subprogram
(Over_Subp
)
835 Error_Msg_N
("incompatible overriding in effect", Subp
);
837 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
838 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
840 Error_Msg_Sloc
:= Sloc
(Subp
);
841 Error_Msg_N
("\overridden # with ghost subprogram", Subp
);
844 -- A non-Ghost primitive of a type extension cannot override an
845 -- inherited Ghost primitive (SPARK RM 6.9(8)).
847 if Is_Ghost_Entity
(Over_Subp
)
848 and then not Is_Ghost_Entity
(Subp
)
849 and then not Is_Abstract_Subprogram
(Subp
)
851 Error_Msg_N
("incompatible overriding in effect", Subp
);
853 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
854 Error_Msg_N
("\& declared # as ghost subprogram", Subp
);
856 Error_Msg_Sloc
:= Sloc
(Subp
);
857 Error_Msg_N
("\overridden # with non-ghost subprogram", Subp
);
860 if Present
(Deriv_Typ
)
861 and then not Is_Ignored_Ghost_Entity
(Deriv_Typ
)
863 -- When a tagged type is either non-Ghost or checked Ghost and
864 -- one of its primitives overrides an inherited operation, the
865 -- overridden operation of the ancestor type must be ignored Ghost
866 -- if the primitive is ignored Ghost (SPARK RM 6.9(19)).
868 if Is_Ignored_Ghost_Entity
(Subp
) then
870 -- Both the parent subprogram and overriding subprogram are
873 if Is_Ignored_Ghost_Entity
(Over_Subp
) then
876 -- The parent subprogram carries policy Check
878 elsif Is_Checked_Ghost_Entity
(Over_Subp
) then
880 ("incompatible ghost policies in effect", Subp
);
882 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
884 ("\& declared # with ghost policy `Check`", Subp
);
886 Error_Msg_Sloc
:= Sloc
(Subp
);
888 ("\overridden # with ghost policy `Ignore`", Subp
);
890 -- The parent subprogram is non-Ghost
894 ("incompatible ghost policies in effect", Subp
);
896 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
897 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
899 Error_Msg_Sloc
:= Sloc
(Subp
);
901 ("\overridden # with ghost policy `Ignore`", Subp
);
904 -- When a tagged type is either non-Ghost or checked Ghost and
905 -- one of its primitives overrides an inherited operation, the
906 -- the primitive of the tagged type must be ignored Ghost if the
907 -- overridden operation is ignored Ghost (SPARK RM 6.9(19)).
909 elsif Is_Ignored_Ghost_Entity
(Over_Subp
) then
911 -- Both the parent subprogram and the overriding subprogram are
914 if Is_Ignored_Ghost_Entity
(Subp
) then
917 -- The overriding subprogram carries policy Check
919 elsif Is_Checked_Ghost_Entity
(Subp
) then
921 ("incompatible ghost policies in effect", Subp
);
923 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
925 ("\& declared # with ghost policy `Ignore`", Subp
);
927 Error_Msg_Sloc
:= Sloc
(Subp
);
929 ("\overridden # with Ghost policy `Check`", Subp
);
931 -- The overriding subprogram is non-Ghost
935 ("incompatible ghost policies in effect", Subp
);
937 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
939 ("\& declared # with ghost policy `Ignore`", Subp
);
941 Error_Msg_Sloc
:= Sloc
(Subp
);
943 ("\overridden # with non-ghost subprogram", Subp
);
948 end Check_Ghost_Overriding
;
950 ---------------------------
951 -- Check_Ghost_Primitive --
952 ---------------------------
954 procedure Check_Ghost_Primitive
(Prim
: Entity_Id
; Typ
: Entity_Id
) is
956 -- The Ghost policy in effect at the point of declaration of a primitive
957 -- operation and a tagged type must match (SPARK RM 6.9(18)).
959 if Is_Tagged_Type
(Typ
) then
960 if Is_Checked_Ghost_Entity
(Prim
)
961 and then Is_Ignored_Ghost_Entity
(Typ
)
963 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
965 Error_Msg_Sloc
:= Sloc
(Typ
);
967 ("\tagged type & declared # with ghost policy `Ignore`",
970 Error_Msg_Sloc
:= Sloc
(Prim
);
972 ("\primitive subprogram & declared # with ghost policy `Check`",
975 elsif Is_Ignored_Ghost_Entity
(Prim
)
976 and then Is_Checked_Ghost_Entity
(Typ
)
978 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
980 Error_Msg_Sloc
:= Sloc
(Typ
);
982 ("\tagged type & declared # with ghost policy `Check`",
985 Error_Msg_Sloc
:= Sloc
(Prim
);
987 ("\primitive subprogram & declared # with ghost policy `Ignore`",
991 end Check_Ghost_Primitive
;
993 ----------------------------
994 -- Check_Ghost_Refinement --
995 ----------------------------
997 procedure Check_Ghost_Refinement
999 State_Id
: Entity_Id
;
1001 Constit_Id
: Entity_Id
)
1004 if Is_Ghost_Entity
(State_Id
) then
1005 if Is_Ghost_Entity
(Constit_Id
) then
1007 -- The Ghost policy in effect at the point of abstract state
1008 -- declaration and constituent must match (SPARK RM 6.9(17)).
1010 if Is_Checked_Ghost_Entity
(State_Id
)
1011 and then Is_Ignored_Ghost_Entity
(Constit_Id
)
1013 Error_Msg_Sloc
:= Sloc
(Constit
);
1014 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
1017 ("\abstract state & declared with ghost policy `Check`",
1020 ("\constituent & declared # with ghost policy `Ignore`",
1023 elsif Is_Ignored_Ghost_Entity
(State_Id
)
1024 and then Is_Checked_Ghost_Entity
(Constit_Id
)
1026 Error_Msg_Sloc
:= Sloc
(Constit
);
1027 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
1030 ("\abstract state & declared with ghost policy `Ignore`",
1033 ("\constituent & declared # with ghost policy `Check`",
1037 -- A constituent of a Ghost abstract state must be a Ghost entity
1038 -- (SPARK RM 7.2.2(12)).
1042 ("constituent of ghost state & must be ghost",
1046 end Check_Ghost_Refinement
;
1048 ----------------------
1049 -- Check_Ghost_Type --
1050 ----------------------
1052 procedure Check_Ghost_Type
(Typ
: Entity_Id
) is
1053 Conc_Typ
: Entity_Id
;
1054 Full_Typ
: Entity_Id
;
1057 if Is_Ghost_Entity
(Typ
)
1058 and then Comes_From_Source
(Typ
)
1063 if Is_Single_Concurrent_Type
(Typ
) then
1064 Conc_Typ
:= Anonymous_Object
(Typ
);
1065 Full_Typ
:= Conc_Typ
;
1067 elsif Has_Protected
(Typ
)
1068 or else Has_Task
(Typ
)
1073 -- A Ghost type cannot be concurrent (SPARK RM 6.9(21)). Verify this
1074 -- legality rule first to give a finer-grained diagnostic.
1076 if Present
(Conc_Typ
) then
1077 Error_Msg_N
("ghost type & cannot be concurrent", Conc_Typ
);
1080 -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
1082 if Is_Effectively_Volatile
(Full_Typ
) then
1083 Error_Msg_N
("ghost type & cannot be volatile", Full_Typ
);
1086 end Check_Ghost_Type
;
1092 function Ghost_Entity
(Ref
: Node_Id
) return Entity_Id
is
1093 Obj_Ref
: constant Node_Id
:= Ultimate_Prefix
(Ref
);
1096 -- When the reference denotes a subcomponent, recover the related whole
1097 -- object (SPARK RM 6.9(1)).
1099 if Is_Entity_Name
(Obj_Ref
) then
1100 return Entity
(Obj_Ref
);
1102 -- Otherwise the reference cannot possibly denote a Ghost entity
1109 --------------------------------
1110 -- Implements_Ghost_Interface --
1111 --------------------------------
1113 function Implements_Ghost_Interface
(Typ
: Entity_Id
) return Boolean is
1114 Iface_Elmt
: Elmt_Id
;
1117 -- Traverse the list of interfaces looking for a Ghost interface
1119 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
1120 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
1121 while Present
(Iface_Elmt
) loop
1122 if Is_Ghost_Entity
(Node
(Iface_Elmt
)) then
1126 Next_Elmt
(Iface_Elmt
);
1131 end Implements_Ghost_Interface
;
1137 procedure Initialize
is
1139 Ignored_Ghost_Nodes
.Init
;
1141 -- Set the soft link which enables Atree.Mark_New_Ghost_Node to record
1142 -- an ignored Ghost node or entity.
1144 Set_Ignored_Ghost_Recording_Proc
(Record_Ignored_Ghost_Node
'Access);
1147 ------------------------
1148 -- Install_Ghost_Mode --
1149 ------------------------
1151 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
) is
1153 Install_Ghost_Region
(Mode
, Empty
);
1154 end Install_Ghost_Mode
;
1156 --------------------------
1157 -- Install_Ghost_Region --
1158 --------------------------
1160 procedure Install_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
1162 -- The context is already within an ignored Ghost region. Maintain the
1163 -- start of the outermost ignored Ghost region.
1165 if Present
(Ignored_Ghost_Region
) then
1168 -- The current region is the outermost ignored Ghost region. Save its
1171 elsif Present
(N
) and then Mode
= Ignore
then
1172 Ignored_Ghost_Region
:= N
;
1174 -- Otherwise the current region is not ignored, nothing to save
1177 Ignored_Ghost_Region
:= Empty
;
1181 end Install_Ghost_Region
;
1183 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
) is
1185 Install_Ghost_Region
(Name_To_Ghost_Mode
(Mode
), N
);
1186 end Install_Ghost_Region
;
1188 -------------------------
1189 -- Is_Ghost_Assignment --
1190 -------------------------
1192 function Is_Ghost_Assignment
(N
: Node_Id
) return Boolean is
1196 -- An assignment statement is Ghost when its target denotes a Ghost
1199 if Nkind
(N
) = N_Assignment_Statement
then
1200 Id
:= Ghost_Entity
(Name
(N
));
1202 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
1206 end Is_Ghost_Assignment
;
1208 ----------------------------------
1209 -- Is_Ghost_Attribute_Reference --
1210 ----------------------------------
1212 function Is_Ghost_Attribute_Reference
(N
: Node_Id
) return Boolean is
1214 return Nkind
(N
) = N_Attribute_Reference
1215 and then Attribute_Name
(N
) = Name_Initialized
;
1216 end Is_Ghost_Attribute_Reference
;
1218 --------------------------
1219 -- Is_Ghost_Declaration --
1220 --------------------------
1222 function Is_Ghost_Declaration
(N
: Node_Id
) return Boolean is
1226 -- A declaration is Ghost when it elaborates a Ghost entity or is
1227 -- subject to pragma Ghost.
1229 if Is_Declaration
(N
) then
1230 Id
:= Defining_Entity
(N
);
1232 return Is_Ghost_Entity
(Id
) or else Is_Subject_To_Ghost
(N
);
1236 end Is_Ghost_Declaration
;
1238 ---------------------
1239 -- Is_Ghost_Pragma --
1240 ---------------------
1242 function Is_Ghost_Pragma
(N
: Node_Id
) return Boolean is
1244 return Is_Checked_Ghost_Pragma
(N
) or else Is_Ignored_Ghost_Pragma
(N
);
1245 end Is_Ghost_Pragma
;
1247 -----------------------------
1248 -- Is_Ghost_Procedure_Call --
1249 -----------------------------
1251 function Is_Ghost_Procedure_Call
(N
: Node_Id
) return Boolean is
1255 -- A procedure call is Ghost when it invokes a Ghost procedure
1257 if Nkind
(N
) = N_Procedure_Call_Statement
then
1258 Id
:= Ghost_Entity
(Name
(N
));
1260 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
1264 end Is_Ghost_Procedure_Call
;
1266 ---------------------------
1267 -- Is_Ignored_Ghost_Unit --
1268 ---------------------------
1270 function Is_Ignored_Ghost_Unit
(N
: Node_Id
) return Boolean is
1271 function Ultimate_Original_Node
(Nod
: Node_Id
) return Node_Id
;
1272 -- Obtain the original node of arbitrary node Nod following a potential
1273 -- chain of rewritings.
1275 ----------------------------
1276 -- Ultimate_Original_Node --
1277 ----------------------------
1279 function Ultimate_Original_Node
(Nod
: Node_Id
) return Node_Id
is
1280 Res
: Node_Id
:= Nod
;
1282 while Is_Rewrite_Substitution
(Res
) loop
1283 Res
:= Original_Node
(Res
);
1287 end Ultimate_Original_Node
;
1289 -- Start of processing for Is_Ignored_Ghost_Unit
1292 -- Inspect the original node of the unit in case removal of ignored
1293 -- Ghost code has already taken place.
1296 Nkind
(N
) = N_Compilation_Unit
1297 and then Is_Ignored_Ghost_Entity
1298 (Defining_Entity
(Ultimate_Original_Node
(Unit
(N
))));
1299 end Is_Ignored_Ghost_Unit
;
1301 -------------------------
1302 -- Is_Subject_To_Ghost --
1303 -------------------------
1305 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean is
1306 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean;
1307 -- Determine whether aspect or pragma argument Arg enables "ghostness"
1309 -----------------------
1310 -- Enables_Ghostness --
1311 -----------------------
1313 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean is
1319 if Nkind
(Expr
) = N_Pragma_Argument_Association
then
1320 Expr
:= Get_Pragma_Arg
(Expr
);
1323 -- Determine whether the expression of the aspect or pragma is static
1324 -- and denotes True.
1326 if Present
(Expr
) then
1327 Preanalyze_And_Resolve
(Expr
);
1330 Is_OK_Static_Expression
(Expr
)
1331 and then Is_True
(Expr_Value
(Expr
));
1333 -- Otherwise Ghost defaults to True
1338 end Enables_Ghostness
;
1342 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1345 Prev_Id
: Entity_Id
;
1347 -- Start of processing for Is_Subject_To_Ghost
1350 -- The related entity of the declaration has not been analyzed yet, do
1351 -- not inspect its attributes.
1353 if Ekind
(Id
) = E_Void
then
1356 elsif Is_Ghost_Entity
(Id
) then
1359 -- The completion of a type or a constant is not fully analyzed when the
1360 -- reference to the Ghost entity is resolved. Because the completion is
1361 -- not marked as Ghost yet, inspect the partial view.
1363 elsif Is_Record_Type
(Id
)
1364 or else Ekind
(Id
) = E_Constant
1365 or else (Nkind
(N
) = N_Object_Declaration
1366 and then Constant_Present
(N
))
1368 Prev_Id
:= Incomplete_Or_Partial_View
(Id
);
1370 if Present
(Prev_Id
) and then Is_Ghost_Entity
(Prev_Id
) then
1375 -- Examine the aspect specifications (if any) looking for aspect Ghost
1377 if Permits_Aspect_Specifications
(N
) then
1378 Asp
:= First
(Aspect_Specifications
(N
));
1379 while Present
(Asp
) loop
1380 if Chars
(Identifier
(Asp
)) = Name_Ghost
then
1381 return Enables_Ghostness
(Expression
(Asp
));
1390 -- When the context is a [generic] package declaration, pragma Ghost
1391 -- resides in the visible declarations.
1393 if Nkind
(N
) in N_Generic_Package_Declaration | N_Package_Declaration
1395 Decl
:= First
(Visible_Declarations
(Specification
(N
)));
1397 -- When the context is a package or a subprogram body, pragma Ghost
1398 -- resides in the declarative part.
1400 elsif Nkind
(N
) in N_Package_Body | N_Subprogram_Body
then
1401 Decl
:= First
(Declarations
(N
));
1403 -- Otherwise pragma Ghost appears in the declarations following N
1405 elsif Is_List_Member
(N
) then
1409 while Present
(Decl
) loop
1410 if Nkind
(Decl
) = N_Pragma
1411 and then Pragma_Name
(Decl
) = Name_Ghost
1414 Enables_Ghostness
(First
(Pragma_Argument_Associations
(Decl
)));
1416 -- A source construct ends the region where pragma Ghost may appear,
1417 -- stop the traversal. Check the original node as source constructs
1418 -- may be rewritten into something else by expansion.
1420 elsif Comes_From_Source
(Original_Node
(Decl
)) then
1428 end Is_Subject_To_Ghost
;
1436 Ignored_Ghost_Nodes
.Release
;
1437 Ignored_Ghost_Nodes
.Locked
:= True;
1440 -----------------------------------
1441 -- Mark_And_Set_Ghost_Assignment --
1442 -----------------------------------
1444 procedure Mark_And_Set_Ghost_Assignment
(N
: Node_Id
) is
1445 -- A ghost assignment is an assignment whose left-hand side denotes a
1446 -- ghost object. Subcomponents are not marked "ghost", so we need to
1447 -- find the containing "whole" object. So, for "P.X.Comp (J) := ...",
1448 -- where P is a package, X is a record, and Comp is an array, we need
1449 -- to check the ghost flags of X.
1451 Orig_Lhs
: constant Node_Id
:= Name
(N
);
1453 -- Ghost assignments are irrelevant when the expander is inactive, and
1454 -- processing them in that mode can lead to spurious errors.
1456 if Expander_Active
then
1457 -- Cases where full analysis is needed, involving array indexing
1458 -- which would otherwise be missing array-bounds checks:
1460 if not Analyzed
(Orig_Lhs
)
1462 ((Nkind
(Orig_Lhs
) = N_Indexed_Component
1463 and then Nkind
(Prefix
(Orig_Lhs
)) = N_Selected_Component
1464 and then Nkind
(Prefix
(Prefix
(Orig_Lhs
))) =
1465 N_Indexed_Component
)
1467 (Nkind
(Orig_Lhs
) = N_Selected_Component
1468 and then Nkind
(Prefix
(Orig_Lhs
)) = N_Indexed_Component
1469 and then Nkind
(Prefix
(Prefix
(Orig_Lhs
))) =
1470 N_Selected_Component
1471 and then Nkind
(Parent
(N
)) /= N_Loop_Statement
))
1476 -- Make sure Lhs is at least preanalyzed, so we can tell whether
1477 -- it denotes a ghost variable. In some cases we need to do a full
1478 -- analysis, or else the back end gets confused. Note that in the
1479 -- preanalysis case, we are preanalyzing a copy of the left-hand
1480 -- side name, temporarily attached to the tree.
1483 Lhs
: constant Node_Id
:=
1484 (if Analyzed
(Orig_Lhs
) then Orig_Lhs
1485 else New_Copy_Tree
(Orig_Lhs
));
1487 if not Analyzed
(Lhs
) then
1489 Set_Parent
(Lhs
, N
);
1490 Preanalyze_Without_Errors
(Lhs
);
1491 Set_Name
(N
, Orig_Lhs
);
1495 Whole
: constant Node_Id
:= Whole_Object_Ref
(Lhs
);
1498 if Is_Entity_Name
(Whole
) then
1499 Id
:= Entity
(Whole
);
1501 if Present
(Id
) then
1502 -- Left-hand side denotes a Checked ghost entity, so
1503 -- install the region.
1505 if Is_Checked_Ghost_Entity
(Id
) then
1506 Install_Ghost_Region
(Check
, N
);
1508 -- Left-hand side denotes an Ignored ghost entity, so
1509 -- install the region, and mark the assignment statement
1510 -- as an ignored ghost assignment, so it will be removed
1513 elsif Is_Ignored_Ghost_Entity
(Id
) then
1514 Install_Ghost_Region
(Ignore
, N
);
1515 Set_Is_Ignored_Ghost_Node
(N
);
1516 Record_Ignored_Ghost_Node
(N
);
1523 end Mark_And_Set_Ghost_Assignment
;
1525 -----------------------------
1526 -- Mark_And_Set_Ghost_Body --
1527 -----------------------------
1529 procedure Mark_And_Set_Ghost_Body
1531 Spec_Id
: Entity_Id
)
1533 Body_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1534 Policy
: Name_Id
:= No_Name
;
1537 -- A body becomes Ghost when it is subject to aspect or pragma Ghost
1539 if Is_Subject_To_Ghost
(N
) then
1540 Policy
:= Policy_In_Effect
(Name_Ghost
);
1542 -- A body declared within a Ghost region is automatically Ghost
1543 -- (SPARK RM 6.9(2)).
1545 elsif Ghost_Mode
= Check
then
1546 Policy
:= Name_Check
;
1548 elsif Ghost_Mode
= Ignore
then
1549 Policy
:= Name_Ignore
;
1551 -- Inherit the "ghostness" of the previous declaration when the body
1552 -- acts as a completion.
1554 elsif Present
(Spec_Id
) then
1555 if Is_Checked_Ghost_Entity
(Spec_Id
) then
1556 Policy
:= Name_Check
;
1558 elsif Is_Ignored_Ghost_Entity
(Spec_Id
) then
1559 Policy
:= Name_Ignore
;
1563 -- The Ghost policy in effect at the point of declaration and at the
1564 -- point of completion must match (SPARK RM 6.9(16)).
1566 Check_Ghost_Completion
1567 (Prev_Id
=> Spec_Id
,
1568 Compl_Id
=> Body_Id
);
1570 -- Mark the body as its formals as Ghost
1572 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1574 -- Install the appropriate Ghost region
1576 Install_Ghost_Region
(Policy
, N
);
1577 end Mark_And_Set_Ghost_Body
;
1579 -----------------------------------
1580 -- Mark_And_Set_Ghost_Completion --
1581 -----------------------------------
1583 procedure Mark_And_Set_Ghost_Completion
1585 Prev_Id
: Entity_Id
)
1587 Compl_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1588 Policy
: Name_Id
:= No_Name
;
1591 -- A completion elaborated in a Ghost region is automatically Ghost
1592 -- (SPARK RM 6.9(2)).
1594 if Ghost_Mode
= Check
then
1595 Policy
:= Name_Check
;
1597 elsif Ghost_Mode
= Ignore
then
1598 Policy
:= Name_Ignore
;
1600 -- The completion becomes Ghost when its initial declaration is also
1603 elsif Is_Checked_Ghost_Entity
(Prev_Id
) then
1604 Policy
:= Name_Check
;
1606 elsif Is_Ignored_Ghost_Entity
(Prev_Id
) then
1607 Policy
:= Name_Ignore
;
1610 -- The Ghost policy in effect at the point of declaration and at the
1611 -- point of completion must match (SPARK RM 6.9(16)).
1613 Check_Ghost_Completion
1614 (Prev_Id
=> Prev_Id
,
1615 Compl_Id
=> Compl_Id
);
1617 -- Mark the completion as Ghost
1619 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1621 -- Install the appropriate Ghost region
1623 Install_Ghost_Region
(Policy
, N
);
1624 end Mark_And_Set_Ghost_Completion
;
1626 ------------------------------------
1627 -- Mark_And_Set_Ghost_Declaration --
1628 ------------------------------------
1630 procedure Mark_And_Set_Ghost_Declaration
(N
: Node_Id
) is
1632 Policy
: Name_Id
:= No_Name
;
1635 -- A declaration becomes Ghost when it is subject to aspect or pragma
1638 if Is_Subject_To_Ghost
(N
) then
1639 Policy
:= Policy_In_Effect
(Name_Ghost
);
1641 -- A declaration elaborated in a Ghost region is automatically Ghost
1642 -- (SPARK RM 6.9(2)).
1644 elsif Ghost_Mode
= Check
then
1645 Policy
:= Name_Check
;
1647 elsif Ghost_Mode
= Ignore
then
1648 Policy
:= Name_Ignore
;
1650 -- A child package or subprogram declaration becomes Ghost when its
1651 -- parent is Ghost (SPARK RM 6.9(2)).
1653 elsif Nkind
(N
) in N_Generic_Function_Renaming_Declaration
1654 | N_Generic_Package_Declaration
1655 | N_Generic_Package_Renaming_Declaration
1656 | N_Generic_Procedure_Renaming_Declaration
1657 | N_Generic_Subprogram_Declaration
1658 | N_Package_Declaration
1659 | N_Package_Renaming_Declaration
1660 | N_Subprogram_Declaration
1661 | N_Subprogram_Renaming_Declaration
1662 and then Present
(Parent_Spec
(N
))
1664 Par_Id
:= Defining_Entity
(Unit
(Parent_Spec
(N
)));
1666 if Is_Checked_Ghost_Entity
(Par_Id
) then
1667 Policy
:= Name_Check
;
1669 elsif Is_Ignored_Ghost_Entity
(Par_Id
) then
1670 Policy
:= Name_Ignore
;
1674 -- Mark the declaration and its formals as Ghost
1676 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1678 -- Install the appropriate Ghost region
1680 Install_Ghost_Region
(Policy
, N
);
1681 end Mark_And_Set_Ghost_Declaration
;
1683 --------------------------------------
1684 -- Mark_And_Set_Ghost_Instantiation --
1685 --------------------------------------
1687 procedure Mark_And_Set_Ghost_Instantiation
1691 procedure Check_Ghost_Actuals
;
1692 -- Check the context of ghost actuals
1694 -------------------------
1695 -- Check_Ghost_Actuals --
1696 -------------------------
1698 procedure Check_Ghost_Actuals
is
1699 Assoc
: Node_Id
:= First
(Generic_Associations
(N
));
1703 while Present
(Assoc
) loop
1704 if Nkind
(Assoc
) /= N_Others_Choice
then
1705 Act
:= Explicit_Generic_Actual_Parameter
(Assoc
);
1707 -- Within a nested instantiation, a defaulted actual is an
1708 -- empty association, so nothing to check.
1713 elsif Comes_From_Source
(Act
)
1714 and then Nkind
(Act
) in N_Has_Etype
1715 and then Present
(Etype
(Act
))
1716 and then Is_Ghost_Entity
(Etype
(Act
))
1718 Check_Ghost_Context
(Etype
(Act
), Act
);
1724 end Check_Ghost_Actuals
;
1728 Policy
: Name_Id
:= No_Name
;
1731 -- An instantiation becomes Ghost when it is subject to pragma Ghost
1733 if Is_Subject_To_Ghost
(N
) then
1734 Policy
:= Policy_In_Effect
(Name_Ghost
);
1736 -- An instantiation declaration within a Ghost region is automatically
1737 -- Ghost (SPARK RM 6.9(2)).
1739 elsif Ghost_Mode
= Check
then
1740 Policy
:= Name_Check
;
1742 elsif Ghost_Mode
= Ignore
then
1743 Policy
:= Name_Ignore
;
1745 -- Inherit the "ghostness" of the generic unit, but the current Ghost
1746 -- policy is the relevant one for the instantiation.
1748 elsif Is_Checked_Ghost_Entity
(Gen_Id
)
1749 or else Is_Ignored_Ghost_Entity
(Gen_Id
)
1751 Policy
:= Policy_In_Effect
(Name_Ghost
);
1753 if Policy
= No_Name
then
1754 Policy
:= Name_Ignore
;
1758 -- Mark the instantiation as Ghost
1760 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1762 -- Install the appropriate Ghost region
1764 Install_Ghost_Region
(Policy
, N
);
1766 -- Check Ghost actuals. Given that this routine is unconditionally
1767 -- invoked with subprogram and package instantiations, this check
1768 -- verifies the context of all the ghost entities passed in generic
1771 Check_Ghost_Actuals
;
1772 end Mark_And_Set_Ghost_Instantiation
;
1774 ---------------------------------------
1775 -- Mark_And_Set_Ghost_Procedure_Call --
1776 ---------------------------------------
1778 procedure Mark_And_Set_Ghost_Procedure_Call
(N
: Node_Id
) is
1782 -- A procedure call becomes Ghost when the procedure being invoked is
1783 -- Ghost. Install the Ghost mode of the procedure.
1785 Id
:= Ghost_Entity
(Name
(N
));
1787 if Present
(Id
) then
1788 if Is_Checked_Ghost_Entity
(Id
) then
1789 Install_Ghost_Region
(Check
, N
);
1791 elsif Is_Ignored_Ghost_Entity
(Id
) then
1792 Install_Ghost_Region
(Ignore
, N
);
1794 Set_Is_Ignored_Ghost_Node
(N
);
1795 Record_Ignored_Ghost_Node
(N
);
1798 end Mark_And_Set_Ghost_Procedure_Call
;
1800 -----------------------
1801 -- Mark_Ghost_Clause --
1802 -----------------------
1804 procedure Mark_Ghost_Clause
(N
: Node_Id
) is
1805 Nam
: Node_Id
:= Empty
;
1808 if Nkind
(N
) = N_Use_Package_Clause
then
1811 elsif Nkind
(N
) = N_Use_Type_Clause
then
1812 Nam
:= Subtype_Mark
(N
);
1814 elsif Nkind
(N
) = N_With_Clause
then
1819 and then Is_Entity_Name
(Nam
)
1820 and then Present
(Entity
(Nam
))
1821 and then Is_Ignored_Ghost_Entity
(Entity
(Nam
))
1823 Set_Is_Ignored_Ghost_Node
(N
);
1824 Record_Ignored_Ghost_Node
(N
);
1826 end Mark_Ghost_Clause
;
1828 ------------------------------------
1829 -- Mark_Ghost_Declaration_Or_Body --
1830 ------------------------------------
1832 procedure Mark_Ghost_Declaration_Or_Body
1836 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1838 Mark_Formals
: Boolean := False;
1840 Param_Id
: Entity_Id
;
1843 -- Mark the related node and its entity
1845 if Mode
= Name_Check
then
1846 Mark_Formals
:= True;
1847 Set_Is_Checked_Ghost_Entity
(Id
);
1849 elsif Mode
= Name_Ignore
then
1850 Mark_Formals
:= True;
1851 Set_Is_Ignored_Ghost_Entity
(Id
);
1852 Set_Is_Ignored_Ghost_Node
(N
);
1853 Record_Ignored_Ghost_Node
(N
);
1856 -- Mark all formal parameters when the related node denotes a subprogram
1857 -- or a body. The traversal is performed via the specification because
1858 -- the related subprogram or body may be unanalyzed.
1860 -- ??? could extra formal parameters cause a Ghost leak?
1863 and then Nkind
(N
) in N_Abstract_Subprogram_Declaration
1864 | N_Formal_Abstract_Subprogram_Declaration
1865 | N_Formal_Concrete_Subprogram_Declaration
1866 | N_Generic_Subprogram_Declaration
1868 | N_Subprogram_Body_Stub
1869 | N_Subprogram_Declaration
1870 | N_Subprogram_Renaming_Declaration
1872 Param
:= First
(Parameter_Specifications
(Specification
(N
)));
1873 while Present
(Param
) loop
1874 Param_Id
:= Defining_Entity
(Param
);
1876 if Mode
= Name_Check
then
1877 Set_Is_Checked_Ghost_Entity
(Param_Id
);
1879 elsif Mode
= Name_Ignore
then
1880 Set_Is_Ignored_Ghost_Entity
(Param_Id
);
1886 end Mark_Ghost_Declaration_Or_Body
;
1888 -----------------------
1889 -- Mark_Ghost_Pragma --
1890 -----------------------
1892 procedure Mark_Ghost_Pragma
1897 -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
1900 if Is_Checked_Ghost_Entity
(Id
) then
1901 Mark_Ghost_Pragma
(N
, Check
);
1903 elsif Is_Ignored_Ghost_Entity
(Id
) then
1904 Mark_Ghost_Pragma
(N
, Ignore
);
1906 end Mark_Ghost_Pragma
;
1908 procedure Mark_Ghost_Pragma
1910 Mode
: Ghost_Mode_Type
)
1913 if Mode
= Check
then
1914 Set_Is_Checked_Ghost_Pragma
(N
);
1917 Set_Is_Ignored_Ghost_Pragma
(N
);
1918 Set_Is_Ignored_Ghost_Node
(N
);
1919 Record_Ignored_Ghost_Node
(N
);
1921 end Mark_Ghost_Pragma
;
1923 -------------------------
1924 -- Mark_Ghost_Renaming --
1925 -------------------------
1927 procedure Mark_Ghost_Renaming
1931 Policy
: Name_Id
:= No_Name
;
1934 -- A renaming becomes Ghost when it renames a Ghost entity
1936 if Is_Checked_Ghost_Entity
(Id
) then
1937 Policy
:= Name_Check
;
1939 elsif Is_Ignored_Ghost_Entity
(Id
) then
1940 Policy
:= Name_Ignore
;
1943 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1944 end Mark_Ghost_Renaming
;
1946 ------------------------
1947 -- Name_To_Ghost_Mode --
1948 ------------------------
1950 function Name_To_Ghost_Mode
(Mode
: Name_Id
) return Ghost_Mode_Type
is
1952 if Mode
= Name_Check
then
1955 elsif Mode
= Name_Ignore
then
1958 -- Otherwise the mode must denote one of the following:
1960 -- * Disable indicates that the Ghost policy in effect is Disable
1962 -- * None or No_Name indicates that the associated construct is not
1963 -- subject to any Ghost annotation.
1966 pragma Assert
(Mode
in Name_Disable | Name_None | No_Name
);
1969 end Name_To_Ghost_Mode
;
1971 -------------------------------
1972 -- Record_Ignored_Ghost_Node --
1973 -------------------------------
1975 procedure Record_Ignored_Ghost_Node
(N
: Node_Or_Entity_Id
) is
1977 -- Save all "top level" ignored Ghost nodes which can be safely replaced
1978 -- with a null statement. Note that there is need to save other kinds of
1979 -- nodes because those will always be enclosed by some top level ignored
1983 or else Is_Declaration
(N
)
1984 or else Nkind
(N
) in N_Generic_Instantiation
1985 | N_Push_Pop_xxx_Label
1987 | N_Representation_Clause
1988 | N_Statement_Other_Than_Procedure_Call
1991 | N_Freeze_Generic_Entity
1994 | N_Procedure_Call_Statement
1995 | N_Use_Package_Clause
1997 | N_Variable_Reference_Marker
2000 -- Only ignored Ghost nodes must be recorded in the table
2002 pragma Assert
(Is_Ignored_Ghost_Node
(N
));
2003 Ignored_Ghost_Nodes
.Append
(N
);
2005 end Record_Ignored_Ghost_Node
;
2007 -------------------------------
2008 -- Remove_Ignored_Ghost_Code --
2009 -------------------------------
2011 procedure Remove_Ignored_Ghost_Code
is
2012 procedure Remove_Ignored_Ghost_Node
(N
: Node_Id
);
2013 -- Eliminate ignored Ghost node N from the tree
2015 -------------------------------
2016 -- Remove_Ignored_Ghost_Node --
2017 -------------------------------
2019 procedure Remove_Ignored_Ghost_Node
(N
: Node_Id
) is
2021 -- The generation and processing of ignored Ghost nodes may cause the
2022 -- same node to be saved multiple times. Reducing the number of saves
2023 -- to one involves costly solutions such as a hash table or the use
2024 -- of a flag shared by all nodes. To solve this problem, the removal
2025 -- machinery allows for multiple saves, but does not eliminate a node
2026 -- which has already been eliminated.
2028 if Nkind
(N
) = N_Null_Statement
then
2031 -- Otherwise the ignored Ghost node must be eliminated
2034 -- Only ignored Ghost nodes must be eliminated from the tree
2036 pragma Assert
(Is_Ignored_Ghost_Node
(N
));
2038 -- Eliminate the node by rewriting it into null. Another option
2039 -- is to remove it from the tree, however multiple corner cases
2040 -- emerge which have be dealt individually.
2042 Rewrite
(N
, Make_Null_Statement
(Sloc
(N
)));
2045 end Remove_Ignored_Ghost_Node
;
2047 -- Start of processing for Remove_Ignored_Ghost_Code
2050 for Index
in Ignored_Ghost_Nodes
.First
.. Ignored_Ghost_Nodes
.Last
loop
2051 Remove_Ignored_Ghost_Node
(Ignored_Ghost_Nodes
.Table
(Index
));
2053 end Remove_Ignored_Ghost_Code
;
2055 --------------------------
2056 -- Restore_Ghost_Region --
2057 --------------------------
2059 procedure Restore_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
2062 Ignored_Ghost_Region
:= N
;
2063 end Restore_Ghost_Region
;
2065 --------------------
2066 -- Set_Ghost_Mode --
2067 --------------------
2069 procedure Set_Ghost_Mode
(N
: Node_Or_Entity_Id
) is
2070 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
);
2071 -- Install the Ghost mode of entity Id
2073 --------------------------------
2074 -- Set_Ghost_Mode_From_Entity --
2075 --------------------------------
2077 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
) is
2079 if Is_Checked_Ghost_Entity
(Id
) then
2080 Install_Ghost_Mode
(Check
);
2081 elsif Is_Ignored_Ghost_Entity
(Id
) then
2082 Install_Ghost_Mode
(Ignore
);
2084 Install_Ghost_Mode
(None
);
2086 end Set_Ghost_Mode_From_Entity
;
2092 -- Start of processing for Set_Ghost_Mode
2095 -- The Ghost mode of an assignment statement depends on the Ghost mode
2098 if Nkind
(N
) = N_Assignment_Statement
then
2099 Id
:= Ghost_Entity
(Name
(N
));
2101 if Present
(Id
) then
2102 Set_Ghost_Mode_From_Entity
(Id
);
2105 -- The Ghost mode of a body or a declaration depends on the Ghost mode
2106 -- of its defining entity.
2108 elsif Is_Body
(N
) or else Is_Declaration
(N
) then
2109 Set_Ghost_Mode_From_Entity
(Defining_Entity
(N
));
2111 -- The Ghost mode of an entity depends on the entity itself
2113 elsif Nkind
(N
) in N_Entity
then
2114 Set_Ghost_Mode_From_Entity
(N
);
2116 -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
2117 -- of the entity being frozen.
2119 elsif Nkind
(N
) in N_Freeze_Entity | N_Freeze_Generic_Entity
then
2120 Set_Ghost_Mode_From_Entity
(Entity
(N
));
2122 -- The Ghost mode of a pragma depends on the associated entity. The
2123 -- property is encoded in the pragma itself.
2125 elsif Nkind
(N
) = N_Pragma
then
2126 if Is_Checked_Ghost_Pragma
(N
) then
2127 Install_Ghost_Mode
(Check
);
2128 elsif Is_Ignored_Ghost_Pragma
(N
) then
2129 Install_Ghost_Mode
(Ignore
);
2131 Install_Ghost_Mode
(None
);
2134 -- The Ghost mode of a procedure call depends on the Ghost mode of the
2135 -- procedure being invoked.
2137 elsif Nkind
(N
) = N_Procedure_Call_Statement
then
2138 Id
:= Ghost_Entity
(Name
(N
));
2140 if Present
(Id
) then
2141 Set_Ghost_Mode_From_Entity
(Id
);
2146 -------------------------
2147 -- Set_Is_Ghost_Entity --
2148 -------------------------
2150 procedure Set_Is_Ghost_Entity
(Id
: Entity_Id
) is
2151 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
2153 if Policy
= Name_Check
then
2154 Set_Is_Checked_Ghost_Entity
(Id
);
2155 elsif Policy
= Name_Ignore
then
2156 Set_Is_Ignored_Ghost_Entity
(Id
);
2158 end Set_Is_Ghost_Entity
;
2160 ----------------------
2161 -- Whole_Object_Ref --
2162 ----------------------
2164 function Whole_Object_Ref
(Ref
: Node_Id
) return Node_Id
is
2166 if Nkind
(Ref
) in N_Indexed_Component | N_Slice
2167 or else (Nkind
(Ref
) = N_Selected_Component
2168 and then Is_Object_Reference
(Prefix
(Ref
)))
2170 if Is_Access_Type
(Etype
(Prefix
(Ref
))) then
2173 return Whole_Object_Ref
(Prefix
(Ref
));
2178 end Whole_Object_Ref
;