1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
9 -- Copyright (C) 2014-2018, 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 Elists
; use Elists
;
31 with Errout
; use Errout
;
32 with Namet
; use Namet
;
33 with Nlists
; use Nlists
;
34 with Nmake
; use Nmake
;
36 with Sem_Aux
; use Sem_Aux
;
37 with Sem_Disp
; use Sem_Disp
;
38 with Sem_Eval
; use Sem_Eval
;
39 with Sem_Prag
; use Sem_Prag
;
40 with Sem_Res
; use Sem_Res
;
41 with Sem_Util
; use Sem_Util
;
42 with Sinfo
; use Sinfo
;
43 with Snames
; use Snames
;
52 -- The following table contains all ignored Ghost nodes that must be
53 -- eliminated from the tree by routine Remove_Ignored_Ghost_Code.
55 package Ignored_Ghost_Nodes
is new Table
.Table
(
56 Table_Component_Type
=> Node_Id
,
57 Table_Index_Type
=> Int
,
59 Table_Initial
=> Alloc
.Ignored_Ghost_Nodes_Initial
,
60 Table_Increment
=> Alloc
.Ignored_Ghost_Nodes_Increment
,
61 Table_Name
=> "Ignored_Ghost_Nodes");
63 -----------------------
64 -- Local subprograms --
65 -----------------------
67 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
;
68 -- Find the entity of a reference to a Ghost entity. Return Empty if there
71 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
);
72 pragma Inline
(Install_Ghost_Mode
);
73 -- Install Ghost mode Mode as the Ghost mode in effect
75 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
);
76 pragma Inline
(Install_Ghost_Region
);
77 -- Install a Ghost region comprised of mode Mode and ignored region start
80 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean;
81 -- Determine whether declaration or body N is subject to aspect or pragma
82 -- Ghost. This routine must be used in cases where pragma Ghost has not
83 -- been analyzed yet, but the context needs to establish the "ghostness"
86 procedure Mark_Ghost_Declaration_Or_Body
89 -- Mark the defining entity of declaration or body N as Ghost depending on
90 -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
93 function Name_To_Ghost_Mode
(Mode
: Name_Id
) return Ghost_Mode_Type
;
94 pragma Inline
(Name_To_Ghost_Mode
);
95 -- Convert a Ghost mode denoted by name Mode into its respective enumerated
98 procedure Record_Ignored_Ghost_Node
(N
: Node_Or_Entity_Id
);
99 -- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
100 -- later elimination.
102 ----------------------------
103 -- Check_Ghost_Completion --
104 ----------------------------
106 procedure Check_Ghost_Completion
107 (Prev_Id
: Entity_Id
;
108 Compl_Id
: Entity_Id
)
110 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
113 -- Nothing to do if one of the views is missing
115 if No
(Prev_Id
) or else No
(Compl_Id
) then
118 -- The Ghost policy in effect at the point of declaration and at the
119 -- point of completion must match (SPARK RM 6.9(14)).
121 elsif Is_Checked_Ghost_Entity
(Prev_Id
)
122 and then Policy
= Name_Ignore
124 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
126 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
127 Error_Msg_N
("\& declared with ghost policy `Check`", Prev_Id
);
128 Error_Msg_N
("\& completed # with ghost policy `Ignore`", Prev_Id
);
130 elsif Is_Ignored_Ghost_Entity
(Prev_Id
)
131 and then Policy
= Name_Check
133 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
135 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
136 Error_Msg_N
("\& declared with ghost policy `Ignore`", Prev_Id
);
137 Error_Msg_N
("\& completed # with ghost policy `Check`", Prev_Id
);
139 end Check_Ghost_Completion
;
141 -------------------------
142 -- Check_Ghost_Context --
143 -------------------------
145 procedure Check_Ghost_Context
(Ghost_Id
: Entity_Id
; Ghost_Ref
: Node_Id
) is
146 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
);
147 -- Verify that the Ghost policy at the point of declaration of entity Id
148 -- matches the policy at the point of reference Ref. If this is not the
149 -- case emit an error at Ref.
151 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean;
152 -- Determine whether node Context denotes a Ghost-friendly context where
153 -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
155 -------------------------
156 -- Is_OK_Ghost_Context --
157 -------------------------
159 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean is
160 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean;
161 -- Determine whether node Decl is a suitable context for a reference
162 -- to a Ghost entity. To qualify as such, Decl must either
164 -- * Define a Ghost entity
166 -- * Be subject to pragma Ghost
168 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean;
169 -- Determine whether node Prag is a suitable context for a reference
170 -- to a Ghost entity. To qualify as such, Prag must either
172 -- * Be an assertion expression pragma
174 -- * Denote pragma Global, Depends, Initializes, Refined_Global,
175 -- Refined_Depends or Refined_State.
177 -- * Specify an aspect of a Ghost entity
179 -- * Contain a reference to a Ghost entity
181 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean;
182 -- Determine whether node Stmt is a suitable context for a reference
183 -- to a Ghost entity. To qualify as such, Stmt must either
185 -- * Denote a procedure call to a Ghost procedure
187 -- * Denote an assignment statement whose target is Ghost
189 -----------------------
190 -- Is_OK_Declaration --
191 -----------------------
193 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean is
194 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean;
195 -- Determine whether node N appears in the profile of a subprogram
198 --------------------------------
199 -- In_Subprogram_Body_Profile --
200 --------------------------------
202 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean is
203 Spec
: constant Node_Id
:= Parent
(N
);
206 -- The node appears in a parameter specification in which case
207 -- it is either the parameter type or the default expression or
208 -- the node appears as the result definition of a function.
211 (Nkind
(N
) = N_Parameter_Specification
213 (Nkind
(Spec
) = N_Function_Specification
214 and then N
= Result_Definition
(Spec
)))
215 and then Nkind
(Parent
(Spec
)) = N_Subprogram_Body
;
216 end In_Subprogram_Body_Profile
;
223 -- Start of processing for Is_OK_Declaration
226 if Is_Ghost_Declaration
(Decl
) then
231 -- A reference to a Ghost entity may appear within the profile of
232 -- a subprogram body. This context is treated as suitable because
233 -- it duplicates the context of the corresponding spec. The real
234 -- check was already performed during the analysis of the spec.
236 elsif In_Subprogram_Body_Profile
(Decl
) then
239 -- A reference to a Ghost entity may appear within an expression
240 -- function which is still being analyzed. This context is treated
241 -- as suitable because it is not yet known whether the expression
242 -- function is an initial declaration or a completion. The real
243 -- check is performed when the expression function is expanded.
245 elsif Nkind
(Decl
) = N_Expression_Function
246 and then not Analyzed
(Decl
)
250 -- References to Ghost entities may be relocated in internally
253 elsif Nkind
(Decl
) = N_Subprogram_Body
254 and then not Comes_From_Source
(Decl
)
256 Subp_Id
:= Corresponding_Spec
(Decl
);
258 if Present
(Subp_Id
) then
260 -- The context is the internally built _Postconditions
261 -- procedure, which is OK because the real check was done
262 -- before expansion activities.
264 if Chars
(Subp_Id
) = Name_uPostconditions
then
267 -- The context is the internally built predicate function,
268 -- which is OK because the real check was done before the
269 -- predicate function was generated.
271 elsif Is_Predicate_Function
(Subp_Id
) then
276 Original_Node
(Unit_Declaration_Node
(Subp_Id
));
278 -- The original context is an expression function that
279 -- has been split into a spec and a body. The context is
280 -- OK as long as the initial declaration is Ghost.
282 if Nkind
(Subp_Decl
) = N_Expression_Function
then
283 return Is_Ghost_Declaration
(Subp_Decl
);
287 -- Otherwise this is either an internal body or an internal
288 -- completion. Both are OK because the real check was done
289 -- before expansion activities.
297 end Is_OK_Declaration
;
303 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean is
304 procedure Check_Policies
(Prag_Nam
: Name_Id
);
305 -- Verify that the Ghost policy in effect is the same as the
306 -- assertion policy for pragma name Prag_Nam. Emit an error if
307 -- this is not the case.
313 procedure Check_Policies
(Prag_Nam
: Name_Id
) is
314 AP
: constant Name_Id
:= Check_Kind
(Prag_Nam
);
315 GP
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
318 -- If the Ghost policy in effect at the point of a Ghost entity
319 -- reference is Ignore, then the assertion policy of the pragma
320 -- must be Ignore (SPARK RM 6.9(18)).
322 if GP
= Name_Ignore
and then AP
/= Name_Ignore
then
324 ("incompatible ghost policies in effect",
327 ("\ghost entity & has policy `Ignore`",
328 Ghost_Ref
, Ghost_Id
);
330 Error_Msg_Name_1
:= AP
;
332 ("\assertion expression has policy %", Ghost_Ref
);
341 -- Start of processing for Is_OK_Pragma
344 if Nkind
(Prag
) = N_Pragma
then
345 Prag_Id
:= Get_Pragma_Id
(Prag
);
346 Prag_Nam
:= Original_Aspect_Pragma_Name
(Prag
);
348 -- A pragma that applies to a Ghost construct or specifies an
349 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
351 if Is_Ghost_Pragma
(Prag
) then
354 -- An assertion expression pragma is Ghost when it contains a
355 -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
356 -- predicate pragmas (SPARK RM 6.9(11)).
358 elsif Assertion_Expression_Pragma
(Prag_Id
)
359 and then Prag_Id
/= Pragma_Predicate
361 -- Ensure that the assertion policy and the Ghost policy are
362 -- compatible (SPARK RM 6.9(18)).
364 Check_Policies
(Prag_Nam
);
367 -- Several pragmas that may apply to a non-Ghost entity are
368 -- treated as Ghost when they contain a reference to a Ghost
369 -- entity (SPARK RM 6.9(11)).
371 elsif Nam_In
(Prag_Nam
, Name_Global
,
375 Name_Refined_Depends
,
385 ---------------------
386 -- Is_OK_Statement --
387 ---------------------
389 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean is
391 -- An assignment statement is Ghost when the target is a Ghost
394 if Nkind
(Stmt
) = N_Assignment_Statement
then
395 return Is_Ghost_Assignment
(Stmt
);
397 -- A procedure call is Ghost when it calls a Ghost procedure
399 elsif Nkind
(Stmt
) = N_Procedure_Call_Statement
then
400 return Is_Ghost_Procedure_Call
(Stmt
);
404 -- An if statement is a suitable context for a Ghost entity if it
405 -- is the byproduct of assertion expression expansion. Note that
406 -- the assertion expression may not be related to a Ghost entity,
407 -- but it may still contain references to Ghost entities.
409 elsif Nkind
(Stmt
) = N_If_Statement
410 and then Nkind
(Original_Node
(Stmt
)) = N_Pragma
411 and then Assertion_Expression_Pragma
412 (Get_Pragma_Id
(Original_Node
(Stmt
)))
424 -- Start of processing for Is_OK_Ghost_Context
427 -- The context is Ghost when it appears within a Ghost package or
430 if Ghost_Mode
> None
then
433 -- A Ghost type may be referenced in a use_type clause
434 -- (SPARK RM 6.9.10).
436 elsif Present
(Parent
(Context
))
437 and then Nkind
(Parent
(Context
)) = N_Use_Type_Clause
441 -- Routine Expand_Record_Extension creates a parent subtype without
442 -- inserting it into the tree. There is no good way of recognizing
443 -- this special case as there is no parent. Try to approximate the
446 elsif No
(Parent
(Context
)) and then Is_Tagged_Type
(Ghost_Id
) then
449 -- Otherwise climb the parent chain looking for a suitable Ghost
454 while Present
(Par
) loop
455 if Is_Ignored_Ghost_Node
(Par
) then
458 -- A reference to a Ghost entity can appear within an aspect
459 -- specification (SPARK RM 6.9(10)). The precise checking will
460 -- occur when analyzing the corresponding pragma. We make an
461 -- exception for predicate aspects that only allow referencing
462 -- a Ghost entity when the corresponding type declaration is
463 -- Ghost (SPARK RM 6.9(11)).
465 elsif Nkind
(Par
) = N_Aspect_Specification
466 and then not Same_Aspect
467 (Get_Aspect_Id
(Par
), Aspect_Predicate
)
471 elsif Is_OK_Declaration
(Par
) then
474 elsif Is_OK_Pragma
(Par
) then
477 elsif Is_OK_Statement
(Par
) then
480 -- Prevent the search from going too far
482 elsif Is_Body_Or_Package_Declaration
(Par
) then
489 -- The expansion of assertion expression pragmas and attribute Old
490 -- may cause a legal Ghost entity reference to become illegal due
491 -- to node relocation. Check the In_Assertion_Expr counter as last
492 -- resort to try and infer the original legal context.
494 if In_Assertion_Expr
> 0 then
497 -- Otherwise the context is not suitable for a reference to a
504 end Is_OK_Ghost_Context
;
506 ------------------------
507 -- Check_Ghost_Policy --
508 ------------------------
510 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
) is
511 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
514 -- The Ghost policy in effect a the point of declaration and at the
515 -- point of use must match (SPARK RM 6.9(13)).
517 if Is_Checked_Ghost_Entity
(Id
)
518 and then Policy
= Name_Ignore
519 and then May_Be_Lvalue
(Ref
)
521 Error_Msg_Sloc
:= Sloc
(Ref
);
523 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
524 Error_Msg_NE
("\& declared with ghost policy `Check`", Ref
, Id
);
525 Error_Msg_NE
("\& used # with ghost policy `Ignore`", Ref
, Id
);
527 elsif Is_Ignored_Ghost_Entity
(Id
) and then Policy
= Name_Check
then
528 Error_Msg_Sloc
:= Sloc
(Ref
);
530 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
531 Error_Msg_NE
("\& declared with ghost policy `Ignore`", Ref
, Id
);
532 Error_Msg_NE
("\& used # with ghost policy `Check`", Ref
, Id
);
534 end Check_Ghost_Policy
;
536 -- Start of processing for Check_Ghost_Context
539 -- Once it has been established that the reference to the Ghost entity
540 -- is within a suitable context, ensure that the policy at the point of
541 -- declaration and at the point of use match.
543 if Is_OK_Ghost_Context
(Ghost_Ref
) then
544 Check_Ghost_Policy
(Ghost_Id
, Ghost_Ref
);
546 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
547 -- its behavior or value (SPARK RM 6.9(10,11)).
550 Error_Msg_N
("ghost entity cannot appear in this context", Ghost_Ref
);
552 end Check_Ghost_Context
;
554 ----------------------------
555 -- Check_Ghost_Overriding --
556 ----------------------------
558 procedure Check_Ghost_Overriding
560 Overridden_Subp
: Entity_Id
)
562 Deriv_Typ
: Entity_Id
;
563 Over_Subp
: Entity_Id
;
566 if Present
(Subp
) and then Present
(Overridden_Subp
) then
567 Over_Subp
:= Ultimate_Alias
(Overridden_Subp
);
568 Deriv_Typ
:= Find_Dispatching_Type
(Subp
);
570 -- A Ghost primitive of a non-Ghost type extension cannot override an
571 -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
573 if Is_Ghost_Entity
(Subp
)
574 and then Present
(Deriv_Typ
)
575 and then not Is_Ghost_Entity
(Deriv_Typ
)
576 and then not Is_Ghost_Entity
(Over_Subp
)
577 and then not Is_Abstract_Subprogram
(Over_Subp
)
579 Error_Msg_N
("incompatible overriding in effect", Subp
);
581 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
582 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
584 Error_Msg_Sloc
:= Sloc
(Subp
);
585 Error_Msg_N
("\overridden # with ghost subprogram", Subp
);
588 -- A non-Ghost primitive of a type extension cannot override an
589 -- inherited Ghost primitive (SPARK RM 6.9(8)).
591 if Is_Ghost_Entity
(Over_Subp
)
592 and then not Is_Ghost_Entity
(Subp
)
593 and then not Is_Abstract_Subprogram
(Subp
)
595 Error_Msg_N
("incompatible overriding in effect", Subp
);
597 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
598 Error_Msg_N
("\& declared # as ghost subprogram", Subp
);
600 Error_Msg_Sloc
:= Sloc
(Subp
);
601 Error_Msg_N
("\overridden # with non-ghost subprogram", Subp
);
604 if Present
(Deriv_Typ
)
605 and then not Is_Ignored_Ghost_Entity
(Deriv_Typ
)
607 -- When a tagged type is either non-Ghost or checked Ghost and
608 -- one of its primitives overrides an inherited operation, the
609 -- overridden operation of the ancestor type must be ignored Ghost
610 -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
612 if Is_Ignored_Ghost_Entity
(Subp
) then
614 -- Both the parent subprogram and overriding subprogram are
617 if Is_Ignored_Ghost_Entity
(Over_Subp
) then
620 -- The parent subprogram carries policy Check
622 elsif Is_Checked_Ghost_Entity
(Over_Subp
) then
624 ("incompatible ghost policies in effect", Subp
);
626 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
628 ("\& declared # with ghost policy `Check`", Subp
);
630 Error_Msg_Sloc
:= Sloc
(Subp
);
632 ("\overridden # with ghost policy `Ignore`", Subp
);
634 -- The parent subprogram is non-Ghost
638 ("incompatible ghost policies in effect", Subp
);
640 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
641 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
643 Error_Msg_Sloc
:= Sloc
(Subp
);
645 ("\overridden # with ghost policy `Ignore`", Subp
);
648 -- When a tagged type is either non-Ghost or checked Ghost and
649 -- one of its primitives overrides an inherited operation, the
650 -- the primitive of the tagged type must be ignored Ghost if the
651 -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
653 elsif Is_Ignored_Ghost_Entity
(Over_Subp
) then
655 -- Both the parent subprogram and the overriding subprogram are
658 if Is_Ignored_Ghost_Entity
(Subp
) then
661 -- The overriding subprogram carries policy Check
663 elsif Is_Checked_Ghost_Entity
(Subp
) then
665 ("incompatible ghost policies in effect", Subp
);
667 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
669 ("\& declared # with ghost policy `Ignore`", Subp
);
671 Error_Msg_Sloc
:= Sloc
(Subp
);
673 ("\overridden # with Ghost policy `Check`", Subp
);
675 -- The overriding subprogram is non-Ghost
679 ("incompatible ghost policies in effect", Subp
);
681 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
683 ("\& declared # with ghost policy `Ignore`", Subp
);
685 Error_Msg_Sloc
:= Sloc
(Subp
);
687 ("\overridden # with non-ghost subprogram", Subp
);
692 end Check_Ghost_Overriding
;
694 ---------------------------
695 -- Check_Ghost_Primitive --
696 ---------------------------
698 procedure Check_Ghost_Primitive
(Prim
: Entity_Id
; Typ
: Entity_Id
) is
700 -- The Ghost policy in effect at the point of declaration of a primitive
701 -- operation and a tagged type must match (SPARK RM 6.9(16)).
703 if Is_Tagged_Type
(Typ
) then
704 if Is_Checked_Ghost_Entity
(Prim
)
705 and then Is_Ignored_Ghost_Entity
(Typ
)
707 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
709 Error_Msg_Sloc
:= Sloc
(Typ
);
711 ("\tagged type & declared # with ghost policy `Ignore`",
714 Error_Msg_Sloc
:= Sloc
(Prim
);
716 ("\primitive subprogram & declared # with ghost policy `Check`",
719 elsif Is_Ignored_Ghost_Entity
(Prim
)
720 and then Is_Checked_Ghost_Entity
(Typ
)
722 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
724 Error_Msg_Sloc
:= Sloc
(Typ
);
726 ("\tagged type & declared # with ghost policy `Check`",
729 Error_Msg_Sloc
:= Sloc
(Prim
);
731 ("\primitive subprogram & declared # with ghost policy `Ignore`",
735 end Check_Ghost_Primitive
;
737 ----------------------------
738 -- Check_Ghost_Refinement --
739 ----------------------------
741 procedure Check_Ghost_Refinement
743 State_Id
: Entity_Id
;
745 Constit_Id
: Entity_Id
)
748 if Is_Ghost_Entity
(State_Id
) then
749 if Is_Ghost_Entity
(Constit_Id
) then
751 -- The Ghost policy in effect at the point of abstract state
752 -- declaration and constituent must match (SPARK RM 6.9(15)).
754 if Is_Checked_Ghost_Entity
(State_Id
)
755 and then Is_Ignored_Ghost_Entity
(Constit_Id
)
757 Error_Msg_Sloc
:= Sloc
(Constit
);
758 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
761 ("\abstract state & declared with ghost policy `Check`",
764 ("\constituent & declared # with ghost policy `Ignore`",
767 elsif Is_Ignored_Ghost_Entity
(State_Id
)
768 and then Is_Checked_Ghost_Entity
(Constit_Id
)
770 Error_Msg_Sloc
:= Sloc
(Constit
);
771 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
774 ("\abstract state & declared with ghost policy `Ignore`",
777 ("\constituent & declared # with ghost policy `Check`",
781 -- A constituent of a Ghost abstract state must be a Ghost entity
782 -- (SPARK RM 7.2.2(12)).
786 ("constituent of ghost state & must be ghost",
790 end Check_Ghost_Refinement
;
792 ----------------------
793 -- Check_Ghost_Type --
794 ----------------------
796 procedure Check_Ghost_Type
(Typ
: Entity_Id
) is
797 Conc_Typ
: Entity_Id
;
798 Full_Typ
: Entity_Id
;
801 if Is_Ghost_Entity
(Typ
) then
805 if Is_Single_Concurrent_Type
(Typ
) then
806 Conc_Typ
:= Anonymous_Object
(Typ
);
807 Full_Typ
:= Conc_Typ
;
809 elsif Is_Concurrent_Type
(Typ
) then
813 -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
814 -- legality rule first to give a finer-grained diagnostic.
816 if Present
(Conc_Typ
) then
817 Error_Msg_N
("ghost type & cannot be concurrent", Conc_Typ
);
820 -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
822 if Is_Effectively_Volatile
(Full_Typ
) then
823 Error_Msg_N
("ghost type & cannot be volatile", Full_Typ
);
826 end Check_Ghost_Type
;
832 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
is
836 -- When the reference denotes a subcomponent, recover the related
837 -- object (SPARK RM 6.9(1)).
840 while Nkind_In
(Ref
, N_Explicit_Dereference
,
842 N_Selected_Component
,
848 if Is_Entity_Name
(Ref
) then
855 --------------------------------
856 -- Implements_Ghost_Interface --
857 --------------------------------
859 function Implements_Ghost_Interface
(Typ
: Entity_Id
) return Boolean is
860 Iface_Elmt
: Elmt_Id
;
863 -- Traverse the list of interfaces looking for a Ghost interface
865 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
866 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
867 while Present
(Iface_Elmt
) loop
868 if Is_Ghost_Entity
(Node
(Iface_Elmt
)) then
872 Next_Elmt
(Iface_Elmt
);
877 end Implements_Ghost_Interface
;
883 procedure Initialize
is
885 Ignored_Ghost_Nodes
.Init
;
887 -- Set the soft link which enables Atree.Mark_New_Ghost_Node to record
888 -- an ignored Ghost node or entity.
890 Set_Ignored_Ghost_Recording_Proc
(Record_Ignored_Ghost_Node
'Access);
893 ------------------------
894 -- Install_Ghost_Mode --
895 ------------------------
897 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
) is
899 Install_Ghost_Region
(Mode
, Empty
);
900 end Install_Ghost_Mode
;
902 --------------------------
903 -- Install_Ghost_Region --
904 --------------------------
906 procedure Install_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
908 -- The context is already within an ignored Ghost region. Maintain the
909 -- start of the outermost ignored Ghost region.
911 if Present
(Ignored_Ghost_Region
) then
914 -- The current region is the outermost ignored Ghost region. Save its
917 elsif Present
(N
) and then Mode
= Ignore
then
918 Ignored_Ghost_Region
:= N
;
920 -- Otherwise the current region is not ignored, nothing to save
923 Ignored_Ghost_Region
:= Empty
;
927 end Install_Ghost_Region
;
929 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
) is
931 Install_Ghost_Region
(Name_To_Ghost_Mode
(Mode
), N
);
932 end Install_Ghost_Region
;
934 -------------------------
935 -- Is_Ghost_Assignment --
936 -------------------------
938 function Is_Ghost_Assignment
(N
: Node_Id
) return Boolean is
942 -- An assignment statement is Ghost when its target denotes a Ghost
945 if Nkind
(N
) = N_Assignment_Statement
then
946 Id
:= Ghost_Entity
(Name
(N
));
948 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
952 end Is_Ghost_Assignment
;
954 --------------------------
955 -- Is_Ghost_Declaration --
956 --------------------------
958 function Is_Ghost_Declaration
(N
: Node_Id
) return Boolean is
962 -- A declaration is Ghost when it elaborates a Ghost entity or is
963 -- subject to pragma Ghost.
965 if Is_Declaration
(N
) then
966 Id
:= Defining_Entity
(N
);
968 return Is_Ghost_Entity
(Id
) or else Is_Subject_To_Ghost
(N
);
972 end Is_Ghost_Declaration
;
974 ---------------------
975 -- Is_Ghost_Pragma --
976 ---------------------
978 function Is_Ghost_Pragma
(N
: Node_Id
) return Boolean is
980 return Is_Checked_Ghost_Pragma
(N
) or else Is_Ignored_Ghost_Pragma
(N
);
983 -----------------------------
984 -- Is_Ghost_Procedure_Call --
985 -----------------------------
987 function Is_Ghost_Procedure_Call
(N
: Node_Id
) return Boolean is
991 -- A procedure call is Ghost when it invokes a Ghost procedure
993 if Nkind
(N
) = N_Procedure_Call_Statement
then
994 Id
:= Ghost_Entity
(Name
(N
));
996 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
1000 end Is_Ghost_Procedure_Call
;
1002 ---------------------------
1003 -- Is_Ignored_Ghost_Unit --
1004 ---------------------------
1006 function Is_Ignored_Ghost_Unit
(N
: Node_Id
) return Boolean is
1007 function Ultimate_Original_Node
(Nod
: Node_Id
) return Node_Id
;
1008 -- Obtain the original node of arbitrary node Nod following a potential
1009 -- chain of rewritings.
1011 ----------------------------
1012 -- Ultimate_Original_Node --
1013 ----------------------------
1015 function Ultimate_Original_Node
(Nod
: Node_Id
) return Node_Id
is
1020 while Original_Node
(Res
) /= Res
loop
1021 Res
:= Original_Node
(Res
);
1025 end Ultimate_Original_Node
;
1027 -- Start of processing for Is_Ignored_Ghost_Unit
1030 -- Inspect the original node of the unit in case removal of ignored
1031 -- Ghost code has already taken place.
1034 Nkind
(N
) = N_Compilation_Unit
1035 and then Is_Ignored_Ghost_Entity
1036 (Defining_Entity
(Ultimate_Original_Node
(Unit
(N
))));
1037 end Is_Ignored_Ghost_Unit
;
1039 -------------------------
1040 -- Is_Subject_To_Ghost --
1041 -------------------------
1043 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean is
1044 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean;
1045 -- Determine whether aspect or pragma argument Arg enables "ghostness"
1047 -----------------------
1048 -- Enables_Ghostness --
1049 -----------------------
1051 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean is
1057 if Nkind
(Expr
) = N_Pragma_Argument_Association
then
1058 Expr
:= Get_Pragma_Arg
(Expr
);
1061 -- Determine whether the expression of the aspect or pragma is static
1062 -- and denotes True.
1064 if Present
(Expr
) then
1065 Preanalyze_And_Resolve
(Expr
);
1068 Is_OK_Static_Expression
(Expr
)
1069 and then Is_True
(Expr_Value
(Expr
));
1071 -- Otherwise Ghost defaults to True
1076 end Enables_Ghostness
;
1080 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1083 Prev_Id
: Entity_Id
;
1085 -- Start of processing for Is_Subject_To_Ghost
1088 -- The related entity of the declaration has not been analyzed yet, do
1089 -- not inspect its attributes.
1091 if Ekind
(Id
) = E_Void
then
1094 elsif Is_Ghost_Entity
(Id
) then
1097 -- The completion of a type or a constant is not fully analyzed when the
1098 -- reference to the Ghost entity is resolved. Because the completion is
1099 -- not marked as Ghost yet, inspect the partial view.
1101 elsif Is_Record_Type
(Id
)
1102 or else Ekind
(Id
) = E_Constant
1103 or else (Nkind
(N
) = N_Object_Declaration
1104 and then Constant_Present
(N
))
1106 Prev_Id
:= Incomplete_Or_Partial_View
(Id
);
1108 if Present
(Prev_Id
) and then Is_Ghost_Entity
(Prev_Id
) then
1113 -- Examine the aspect specifications (if any) looking for aspect Ghost
1115 if Permits_Aspect_Specifications
(N
) then
1116 Asp
:= First
(Aspect_Specifications
(N
));
1117 while Present
(Asp
) loop
1118 if Chars
(Identifier
(Asp
)) = Name_Ghost
then
1119 return Enables_Ghostness
(Expression
(Asp
));
1128 -- When the context is a [generic] package declaration, pragma Ghost
1129 -- resides in the visible declarations.
1131 if Nkind_In
(N
, N_Generic_Package_Declaration
,
1132 N_Package_Declaration
)
1134 Decl
:= First
(Visible_Declarations
(Specification
(N
)));
1136 -- When the context is a package or a subprogram body, pragma Ghost
1137 -- resides in the declarative part.
1139 elsif Nkind_In
(N
, N_Package_Body
, N_Subprogram_Body
) then
1140 Decl
:= First
(Declarations
(N
));
1142 -- Otherwise pragma Ghost appears in the declarations following N
1144 elsif Is_List_Member
(N
) then
1148 while Present
(Decl
) loop
1149 if Nkind
(Decl
) = N_Pragma
1150 and then Pragma_Name
(Decl
) = Name_Ghost
1153 Enables_Ghostness
(First
(Pragma_Argument_Associations
(Decl
)));
1155 -- A source construct ends the region where pragma Ghost may appear,
1156 -- stop the traversal. Check the original node as source constructs
1157 -- may be rewritten into something else by expansion.
1159 elsif Comes_From_Source
(Original_Node
(Decl
)) then
1167 end Is_Subject_To_Ghost
;
1175 Ignored_Ghost_Nodes
.Release
;
1176 Ignored_Ghost_Nodes
.Locked
:= True;
1179 -----------------------------------
1180 -- Mark_And_Set_Ghost_Assignment --
1181 -----------------------------------
1183 procedure Mark_And_Set_Ghost_Assignment
(N
: Node_Id
) is
1187 -- An assignment statement becomes Ghost when its target denotes a Ghost
1188 -- object. Install the Ghost mode of the target.
1190 Id
:= Ghost_Entity
(Name
(N
));
1192 if Present
(Id
) then
1193 if Is_Checked_Ghost_Entity
(Id
) then
1194 Install_Ghost_Region
(Check
, N
);
1196 elsif Is_Ignored_Ghost_Entity
(Id
) then
1197 Install_Ghost_Region
(Ignore
, N
);
1199 Set_Is_Ignored_Ghost_Node
(N
);
1200 Record_Ignored_Ghost_Node
(N
);
1203 end Mark_And_Set_Ghost_Assignment
;
1205 -----------------------------
1206 -- Mark_And_Set_Ghost_Body --
1207 -----------------------------
1209 procedure Mark_And_Set_Ghost_Body
1211 Spec_Id
: Entity_Id
)
1213 Body_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1214 Policy
: Name_Id
:= No_Name
;
1217 -- A body becomes Ghost when it is subject to aspect or pragma Ghost
1219 if Is_Subject_To_Ghost
(N
) then
1220 Policy
:= Policy_In_Effect
(Name_Ghost
);
1222 -- A body declared within a Ghost region is automatically Ghost
1223 -- (SPARK RM 6.9(2)).
1225 elsif Ghost_Mode
= Check
then
1226 Policy
:= Name_Check
;
1228 elsif Ghost_Mode
= Ignore
then
1229 Policy
:= Name_Ignore
;
1231 -- Inherit the "ghostness" of the previous declaration when the body
1232 -- acts as a completion.
1234 elsif Present
(Spec_Id
) then
1235 if Is_Checked_Ghost_Entity
(Spec_Id
) then
1236 Policy
:= Name_Check
;
1238 elsif Is_Ignored_Ghost_Entity
(Spec_Id
) then
1239 Policy
:= Name_Ignore
;
1243 -- The Ghost policy in effect at the point of declaration and at the
1244 -- point of completion must match (SPARK RM 6.9(14)).
1246 Check_Ghost_Completion
1247 (Prev_Id
=> Spec_Id
,
1248 Compl_Id
=> Body_Id
);
1250 -- Mark the body as its formals as Ghost
1252 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1254 -- Install the appropriate Ghost region
1256 Install_Ghost_Region
(Policy
, N
);
1257 end Mark_And_Set_Ghost_Body
;
1259 -----------------------------------
1260 -- Mark_And_Set_Ghost_Completion --
1261 -----------------------------------
1263 procedure Mark_And_Set_Ghost_Completion
1265 Prev_Id
: Entity_Id
)
1267 Compl_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1268 Policy
: Name_Id
:= No_Name
;
1271 -- A completion elaborated in a Ghost region is automatically Ghost
1272 -- (SPARK RM 6.9(2)).
1274 if Ghost_Mode
= Check
then
1275 Policy
:= Name_Check
;
1277 elsif Ghost_Mode
= Ignore
then
1278 Policy
:= Name_Ignore
;
1280 -- The completion becomes Ghost when its initial declaration is also
1283 elsif Is_Checked_Ghost_Entity
(Prev_Id
) then
1284 Policy
:= Name_Check
;
1286 elsif Is_Ignored_Ghost_Entity
(Prev_Id
) then
1287 Policy
:= Name_Ignore
;
1290 -- The Ghost policy in effect at the point of declaration and at the
1291 -- point of completion must match (SPARK RM 6.9(14)).
1293 Check_Ghost_Completion
1294 (Prev_Id
=> Prev_Id
,
1295 Compl_Id
=> Compl_Id
);
1297 -- Mark the completion as Ghost
1299 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1301 -- Install the appropriate Ghost region
1303 Install_Ghost_Region
(Policy
, N
);
1304 end Mark_And_Set_Ghost_Completion
;
1306 ------------------------------------
1307 -- Mark_And_Set_Ghost_Declaration --
1308 ------------------------------------
1310 procedure Mark_And_Set_Ghost_Declaration
(N
: Node_Id
) is
1312 Policy
: Name_Id
:= No_Name
;
1315 -- A declaration becomes Ghost when it is subject to aspect or pragma
1318 if Is_Subject_To_Ghost
(N
) then
1319 Policy
:= Policy_In_Effect
(Name_Ghost
);
1321 -- A declaration elaborated in a Ghost region is automatically Ghost
1322 -- (SPARK RM 6.9(2)).
1324 elsif Ghost_Mode
= Check
then
1325 Policy
:= Name_Check
;
1327 elsif Ghost_Mode
= Ignore
then
1328 Policy
:= Name_Ignore
;
1330 -- A child package or subprogram declaration becomes Ghost when its
1331 -- parent is Ghost (SPARK RM 6.9(2)).
1333 elsif Nkind_In
(N
, N_Generic_Function_Renaming_Declaration
,
1334 N_Generic_Package_Declaration
,
1335 N_Generic_Package_Renaming_Declaration
,
1336 N_Generic_Procedure_Renaming_Declaration
,
1337 N_Generic_Subprogram_Declaration
,
1338 N_Package_Declaration
,
1339 N_Package_Renaming_Declaration
,
1340 N_Subprogram_Declaration
,
1341 N_Subprogram_Renaming_Declaration
)
1342 and then Present
(Parent_Spec
(N
))
1344 Par_Id
:= Defining_Entity
(Unit
(Parent_Spec
(N
)));
1346 if Is_Checked_Ghost_Entity
(Par_Id
) then
1347 Policy
:= Name_Check
;
1349 elsif Is_Ignored_Ghost_Entity
(Par_Id
) then
1350 Policy
:= Name_Ignore
;
1354 -- Mark the declaration and its formals as Ghost
1356 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1358 -- Install the appropriate Ghost region
1360 Install_Ghost_Region
(Policy
, N
);
1361 end Mark_And_Set_Ghost_Declaration
;
1363 --------------------------------------
1364 -- Mark_And_Set_Ghost_Instantiation --
1365 --------------------------------------
1367 procedure Mark_And_Set_Ghost_Instantiation
1371 procedure Check_Ghost_Actuals
;
1372 -- Check the context of ghost actuals
1374 -------------------------
1375 -- Check_Ghost_Actuals --
1376 -------------------------
1378 procedure Check_Ghost_Actuals
is
1379 Assoc
: Node_Id
:= First
(Generic_Associations
(N
));
1383 while Present
(Assoc
) loop
1384 if Nkind
(Assoc
) /= N_Others_Choice
then
1385 Act
:= Explicit_Generic_Actual_Parameter
(Assoc
);
1387 -- Within a nested instantiation, a defaulted actual is an
1388 -- empty association, so nothing to check.
1393 elsif Comes_From_Source
(Act
)
1394 and then Nkind
(Act
) in N_Has_Etype
1395 and then Present
(Etype
(Act
))
1396 and then Is_Ghost_Entity
(Etype
(Act
))
1398 Check_Ghost_Context
(Etype
(Act
), Act
);
1404 end Check_Ghost_Actuals
;
1408 Policy
: Name_Id
:= No_Name
;
1411 -- An instantiation becomes Ghost when it is subject to pragma Ghost
1413 if Is_Subject_To_Ghost
(N
) then
1414 Policy
:= Policy_In_Effect
(Name_Ghost
);
1416 -- An instantiation declaration within a Ghost region is automatically
1417 -- Ghost (SPARK RM 6.9(2)).
1419 elsif Ghost_Mode
= Check
then
1420 Policy
:= Name_Check
;
1422 elsif Ghost_Mode
= Ignore
then
1423 Policy
:= Name_Ignore
;
1425 -- Inherit the "ghostness" of the generic unit
1427 elsif Is_Checked_Ghost_Entity
(Gen_Id
) then
1428 Policy
:= Name_Check
;
1430 elsif Is_Ignored_Ghost_Entity
(Gen_Id
) then
1431 Policy
:= Name_Ignore
;
1434 -- Mark the instantiation as Ghost
1436 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1438 -- Install the appropriate Ghost region
1440 Install_Ghost_Region
(Policy
, N
);
1442 -- Check Ghost actuals. Given that this routine is unconditionally
1443 -- invoked with subprogram and package instantiations, this check
1444 -- verifies the context of all the ghost entities passed in generic
1447 Check_Ghost_Actuals
;
1448 end Mark_And_Set_Ghost_Instantiation
;
1450 ---------------------------------------
1451 -- Mark_And_Set_Ghost_Procedure_Call --
1452 ---------------------------------------
1454 procedure Mark_And_Set_Ghost_Procedure_Call
(N
: Node_Id
) is
1458 -- A procedure call becomes Ghost when the procedure being invoked is
1459 -- Ghost. Install the Ghost mode of the procedure.
1461 Id
:= Ghost_Entity
(Name
(N
));
1463 if Present
(Id
) then
1464 if Is_Checked_Ghost_Entity
(Id
) then
1465 Install_Ghost_Region
(Check
, N
);
1467 elsif Is_Ignored_Ghost_Entity
(Id
) then
1468 Install_Ghost_Region
(Ignore
, N
);
1470 Set_Is_Ignored_Ghost_Node
(N
);
1471 Record_Ignored_Ghost_Node
(N
);
1474 end Mark_And_Set_Ghost_Procedure_Call
;
1476 -----------------------
1477 -- Mark_Ghost_Clause --
1478 -----------------------
1480 procedure Mark_Ghost_Clause
(N
: Node_Id
) is
1481 Nam
: Node_Id
:= Empty
;
1484 if Nkind
(N
) = N_Use_Package_Clause
then
1487 elsif Nkind
(N
) = N_Use_Type_Clause
then
1488 Nam
:= Subtype_Mark
(N
);
1490 elsif Nkind
(N
) = N_With_Clause
then
1495 and then Is_Entity_Name
(Nam
)
1496 and then Present
(Entity
(Nam
))
1497 and then Is_Ignored_Ghost_Entity
(Entity
(Nam
))
1499 Set_Is_Ignored_Ghost_Node
(N
);
1500 Record_Ignored_Ghost_Node
(N
);
1502 end Mark_Ghost_Clause
;
1504 ------------------------------------
1505 -- Mark_Ghost_Declaration_Or_Body --
1506 ------------------------------------
1508 procedure Mark_Ghost_Declaration_Or_Body
1512 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1514 Mark_Formals
: Boolean := False;
1516 Param_Id
: Entity_Id
;
1519 -- Mark the related node and its entity
1521 if Mode
= Name_Check
then
1522 Mark_Formals
:= True;
1523 Set_Is_Checked_Ghost_Entity
(Id
);
1525 elsif Mode
= Name_Ignore
then
1526 Mark_Formals
:= True;
1527 Set_Is_Ignored_Ghost_Entity
(Id
);
1528 Set_Is_Ignored_Ghost_Node
(N
);
1529 Record_Ignored_Ghost_Node
(N
);
1532 -- Mark all formal parameters when the related node denotes a subprogram
1533 -- or a body. The traversal is performed via the specification because
1534 -- the related subprogram or body may be unanalyzed.
1536 -- ??? could extra formal parameters cause a Ghost leak?
1539 and then Nkind_In
(N
, N_Abstract_Subprogram_Declaration
,
1540 N_Formal_Abstract_Subprogram_Declaration
,
1541 N_Formal_Concrete_Subprogram_Declaration
,
1542 N_Generic_Subprogram_Declaration
,
1544 N_Subprogram_Body_Stub
,
1545 N_Subprogram_Declaration
,
1546 N_Subprogram_Renaming_Declaration
)
1548 Param
:= First
(Parameter_Specifications
(Specification
(N
)));
1549 while Present
(Param
) loop
1550 Param_Id
:= Defining_Entity
(Param
);
1552 if Mode
= Name_Check
then
1553 Set_Is_Checked_Ghost_Entity
(Param_Id
);
1555 elsif Mode
= Name_Ignore
then
1556 Set_Is_Ignored_Ghost_Entity
(Param_Id
);
1562 end Mark_Ghost_Declaration_Or_Body
;
1564 -----------------------
1565 -- Mark_Ghost_Pragma --
1566 -----------------------
1568 procedure Mark_Ghost_Pragma
1573 -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
1576 if Is_Checked_Ghost_Entity
(Id
) then
1577 Set_Is_Checked_Ghost_Pragma
(N
);
1579 elsif Is_Ignored_Ghost_Entity
(Id
) then
1580 Set_Is_Ignored_Ghost_Pragma
(N
);
1581 Set_Is_Ignored_Ghost_Node
(N
);
1582 Record_Ignored_Ghost_Node
(N
);
1584 end Mark_Ghost_Pragma
;
1586 -------------------------
1587 -- Mark_Ghost_Renaming --
1588 -------------------------
1590 procedure Mark_Ghost_Renaming
1594 Policy
: Name_Id
:= No_Name
;
1597 -- A renaming becomes Ghost when it renames a Ghost entity
1599 if Is_Checked_Ghost_Entity
(Id
) then
1600 Policy
:= Name_Check
;
1602 elsif Is_Ignored_Ghost_Entity
(Id
) then
1603 Policy
:= Name_Ignore
;
1606 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1607 end Mark_Ghost_Renaming
;
1609 ------------------------
1610 -- Name_To_Ghost_Mode --
1611 ------------------------
1613 function Name_To_Ghost_Mode
(Mode
: Name_Id
) return Ghost_Mode_Type
is
1615 if Mode
= Name_Check
then
1618 elsif Mode
= Name_Ignore
then
1621 -- Otherwise the mode must denote one of the following:
1623 -- * Disable indicates that the Ghost policy in effect is Disable
1625 -- * None or No_Name indicates that the associated construct is not
1626 -- subject to any Ghost annotation.
1629 pragma Assert
(Nam_In
(Mode
, Name_Disable
, Name_None
, No_Name
));
1632 end Name_To_Ghost_Mode
;
1634 -------------------------------
1635 -- Record_Ignored_Ghost_Node --
1636 -------------------------------
1638 procedure Record_Ignored_Ghost_Node
(N
: Node_Or_Entity_Id
) is
1640 -- Save all "top level" ignored Ghost nodes which can be safely replaced
1641 -- with a null statement. Note that there is need to save other kinds of
1642 -- nodes because those will always be enclosed by some top level ignored
1646 or else Is_Declaration
(N
)
1647 or else Nkind
(N
) in N_Generic_Instantiation
1648 or else Nkind
(N
) in N_Push_Pop_xxx_Label
1649 or else Nkind
(N
) in N_Raise_xxx_Error
1650 or else Nkind
(N
) in N_Representation_Clause
1651 or else Nkind_In
(N
, N_Assignment_Statement
,
1654 N_Freeze_Generic_Entity
,
1657 N_Procedure_Call_Statement
,
1658 N_Use_Package_Clause
,
1660 N_Variable_Reference_Marker
,
1663 -- Only ignored Ghost nodes must be recorded in the table
1665 pragma Assert
(Is_Ignored_Ghost_Node
(N
));
1666 Ignored_Ghost_Nodes
.Append
(N
);
1668 end Record_Ignored_Ghost_Node
;
1670 -------------------------------
1671 -- Remove_Ignored_Ghost_Code --
1672 -------------------------------
1674 procedure Remove_Ignored_Ghost_Code
is
1675 procedure Remove_Ignored_Ghost_Node
(N
: Node_Id
);
1676 -- Eliminate ignored Ghost node N from the tree
1678 -------------------------------
1679 -- Remove_Ignored_Ghost_Node --
1680 -------------------------------
1682 procedure Remove_Ignored_Ghost_Node
(N
: Node_Id
) is
1684 -- The generation and processing of ignored Ghost nodes may cause the
1685 -- same node to be saved multiple times. Reducing the number of saves
1686 -- to one involves costly solutions such as a hash table or the use
1687 -- of a flag shared by all nodes. To solve this problem, the removal
1688 -- machinery allows for multiple saves, but does not eliminate a node
1689 -- which has already been eliminated.
1691 if Nkind
(N
) = N_Null_Statement
then
1694 -- Otherwise the ignored Ghost node must be eliminated
1697 -- Only ignored Ghost nodes must be eliminated from the tree
1699 pragma Assert
(Is_Ignored_Ghost_Node
(N
));
1701 -- Eliminate the node by rewriting it into null. Another option
1702 -- is to remove it from the tree, however multiple corner cases
1703 -- emerge which have be dealt individually.
1705 Rewrite
(N
, Make_Null_Statement
(Sloc
(N
)));
1707 -- Eliminate any aspects hanging off the ignored Ghost node
1711 end Remove_Ignored_Ghost_Node
;
1713 -- Start of processing for Remove_Ignored_Ghost_Code
1716 for Index
in Ignored_Ghost_Nodes
.First
.. Ignored_Ghost_Nodes
.Last
loop
1717 Remove_Ignored_Ghost_Node
(Ignored_Ghost_Nodes
.Table
(Index
));
1719 end Remove_Ignored_Ghost_Code
;
1721 --------------------------
1722 -- Restore_Ghost_Region --
1723 --------------------------
1725 procedure Restore_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
1728 Ignored_Ghost_Region
:= N
;
1729 end Restore_Ghost_Region
;
1731 --------------------
1732 -- Set_Ghost_Mode --
1733 --------------------
1735 procedure Set_Ghost_Mode
(N
: Node_Or_Entity_Id
) is
1736 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
);
1737 -- Install the Ghost mode of entity Id
1739 --------------------------------
1740 -- Set_Ghost_Mode_From_Entity --
1741 --------------------------------
1743 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
) is
1745 if Is_Checked_Ghost_Entity
(Id
) then
1746 Install_Ghost_Mode
(Check
);
1747 elsif Is_Ignored_Ghost_Entity
(Id
) then
1748 Install_Ghost_Mode
(Ignore
);
1750 Install_Ghost_Mode
(None
);
1752 end Set_Ghost_Mode_From_Entity
;
1758 -- Start of processing for Set_Ghost_Mode
1761 -- The Ghost mode of an assignment statement depends on the Ghost mode
1764 if Nkind
(N
) = N_Assignment_Statement
then
1765 Id
:= Ghost_Entity
(Name
(N
));
1767 if Present
(Id
) then
1768 Set_Ghost_Mode_From_Entity
(Id
);
1771 -- The Ghost mode of a body or a declaration depends on the Ghost mode
1772 -- of its defining entity.
1774 elsif Is_Body
(N
) or else Is_Declaration
(N
) then
1775 Set_Ghost_Mode_From_Entity
(Defining_Entity
(N
));
1777 -- The Ghost mode of an entity depends on the entity itself
1779 elsif Nkind
(N
) in N_Entity
then
1780 Set_Ghost_Mode_From_Entity
(N
);
1782 -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
1783 -- of the entity being frozen.
1785 elsif Nkind_In
(N
, N_Freeze_Entity
, N_Freeze_Generic_Entity
) then
1786 Set_Ghost_Mode_From_Entity
(Entity
(N
));
1788 -- The Ghost mode of a pragma depends on the associated entity. The
1789 -- property is encoded in the pragma itself.
1791 elsif Nkind
(N
) = N_Pragma
then
1792 if Is_Checked_Ghost_Pragma
(N
) then
1793 Install_Ghost_Mode
(Check
);
1794 elsif Is_Ignored_Ghost_Pragma
(N
) then
1795 Install_Ghost_Mode
(Ignore
);
1797 Install_Ghost_Mode
(None
);
1800 -- The Ghost mode of a procedure call depends on the Ghost mode of the
1801 -- procedure being invoked.
1803 elsif Nkind
(N
) = N_Procedure_Call_Statement
then
1804 Id
:= Ghost_Entity
(Name
(N
));
1806 if Present
(Id
) then
1807 Set_Ghost_Mode_From_Entity
(Id
);
1812 -------------------------
1813 -- Set_Is_Ghost_Entity --
1814 -------------------------
1816 procedure Set_Is_Ghost_Entity
(Id
: Entity_Id
) is
1817 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
1819 if Policy
= Name_Check
then
1820 Set_Is_Checked_Ghost_Entity
(Id
);
1821 elsif Policy
= Name_Ignore
then
1822 Set_Is_Ignored_Ghost_Entity
(Id
);
1824 end Set_Is_Ghost_Entity
;