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
;
33 with Namet
; use Namet
;
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 Snames
; use Snames
;
49 -- The following table contains the N_Compilation_Unit node for a unit that
50 -- is either subject to pragma Ghost with policy Ignore or contains ignored
51 -- Ghost code. The table is used in the removal of ignored Ghost code from
54 package Ignored_Ghost_Units
is new Table
.Table
(
55 Table_Component_Type
=> Node_Id
,
56 Table_Index_Type
=> Int
,
58 Table_Initial
=> Alloc
.Ignored_Ghost_Units_Initial
,
59 Table_Increment
=> Alloc
.Ignored_Ghost_Units_Increment
,
60 Table_Name
=> "Ignored_Ghost_Units");
62 -----------------------
63 -- Local Subprograms --
64 -----------------------
66 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
;
67 -- Find the entity of a reference to a Ghost entity. Return Empty if there
70 procedure Install_Ghost_Mode
(Mode
: Name_Id
);
71 -- Install a specific Ghost mode denoted by Mode by setting global variable
74 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean;
75 -- Determine whether declaration or body N is subject to aspect or pragma
76 -- Ghost. This routine must be used in cases where pragma Ghost has not
77 -- been analyzed yet, but the context needs to establish the "ghostness"
80 procedure Mark_Ghost_Declaration_Or_Body
83 -- Mark the defining entity of declaration or body N as Ghost depending on
84 -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
87 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
);
88 -- Signal all enclosing scopes that they now contain at least one ignored
89 -- Ghost node denoted by N. Add the compilation unit containing N to table
90 -- Ignored_Ghost_Units for post processing.
92 ----------------------------
93 -- Add_Ignored_Ghost_Unit --
94 ----------------------------
96 procedure Add_Ignored_Ghost_Unit
(Unit
: Node_Id
) is
98 pragma Assert
(Nkind
(Unit
) = N_Compilation_Unit
);
100 -- Avoid duplicates in the table as pruning the same unit more than once
101 -- is wasteful. Since ignored Ghost code tends to be grouped up, check
102 -- the contents of the table in reverse.
104 for Index
in reverse Ignored_Ghost_Units
.First
..
105 Ignored_Ghost_Units
.Last
107 -- If the unit is already present in the table, do not add it again
109 if Unit
= Ignored_Ghost_Units
.Table
(Index
) then
114 -- If we get here, then this is the first time the unit is being added
116 Ignored_Ghost_Units
.Append
(Unit
);
117 end Add_Ignored_Ghost_Unit
;
119 ----------------------------
120 -- Check_Ghost_Completion --
121 ----------------------------
123 procedure Check_Ghost_Completion
124 (Prev_Id
: Entity_Id
;
125 Compl_Id
: Entity_Id
)
127 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
130 -- Nothing to do if one of the views is missing
132 if No
(Prev_Id
) or else No
(Compl_Id
) then
135 -- The Ghost policy in effect at the point of declaration and at the
136 -- point of completion must match (SPARK RM 6.9(14)).
138 elsif Is_Checked_Ghost_Entity
(Prev_Id
)
139 and then Policy
= Name_Ignore
141 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
143 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
144 Error_Msg_N
("\& declared with ghost policy `Check`", Prev_Id
);
145 Error_Msg_N
("\& completed # with ghost policy `Ignore`", Prev_Id
);
147 elsif Is_Ignored_Ghost_Entity
(Prev_Id
)
148 and then Policy
= Name_Check
150 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
152 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
153 Error_Msg_N
("\& declared with ghost policy `Ignore`", Prev_Id
);
154 Error_Msg_N
("\& completed # with ghost policy `Check`", Prev_Id
);
156 end Check_Ghost_Completion
;
158 -------------------------
159 -- Check_Ghost_Context --
160 -------------------------
162 procedure Check_Ghost_Context
(Ghost_Id
: Entity_Id
; Ghost_Ref
: Node_Id
) is
163 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
);
164 -- Verify that the Ghost policy at the point of declaration of entity Id
165 -- matches the policy at the point of reference Ref. If this is not the
166 -- case emit an error at Ref.
168 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean;
169 -- Determine whether node Context denotes a Ghost-friendly context where
170 -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
172 -------------------------
173 -- Is_OK_Ghost_Context --
174 -------------------------
176 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean is
177 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean;
178 -- Determine whether node Decl is a suitable context for a reference
179 -- to a Ghost entity. To qualify as such, Decl must either
181 -- * Define a Ghost entity
183 -- * Be subject to pragma Ghost
185 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean;
186 -- Determine whether node Prag is a suitable context for a reference
187 -- to a Ghost entity. To qualify as such, Prag must either
189 -- * Be an assertion expression pragma
191 -- * Denote pragma Global, Depends, Initializes, Refined_Global,
192 -- Refined_Depends or Refined_State.
194 -- * Specify an aspect of a Ghost entity
196 -- * Contain a reference to a Ghost entity
198 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean;
199 -- Determine whether node Stmt is a suitable context for a reference
200 -- to a Ghost entity. To qualify as such, Stmt must either
202 -- * Denote a procedure call to a Ghost procedure
204 -- * Denote an assignment statement whose target is Ghost
206 -----------------------
207 -- Is_OK_Declaration --
208 -----------------------
210 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean is
211 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean;
212 -- Determine whether node N appears in the profile of a subprogram
215 --------------------------------
216 -- In_Subprogram_Body_Profile --
217 --------------------------------
219 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean is
220 Spec
: constant Node_Id
:= Parent
(N
);
223 -- The node appears in a parameter specification in which case
224 -- it is either the parameter type or the default expression or
225 -- the node appears as the result definition of a function.
228 (Nkind
(N
) = N_Parameter_Specification
230 (Nkind
(Spec
) = N_Function_Specification
231 and then N
= Result_Definition
(Spec
)))
232 and then Nkind
(Parent
(Spec
)) = N_Subprogram_Body
;
233 end In_Subprogram_Body_Profile
;
240 -- Start of processing for Is_OK_Declaration
243 if Is_Ghost_Declaration
(Decl
) then
248 -- A reference to a Ghost entity may appear within the profile of
249 -- a subprogram body. This context is treated as suitable because
250 -- it duplicates the context of the corresponding spec. The real
251 -- check was already performed during the analysis of the spec.
253 elsif In_Subprogram_Body_Profile
(Decl
) then
256 -- A reference to a Ghost entity may appear within an expression
257 -- function which is still being analyzed. This context is treated
258 -- as suitable because it is not yet known whether the expression
259 -- function is an initial declaration or a completion. The real
260 -- check is performed when the expression function is expanded.
262 elsif Nkind
(Decl
) = N_Expression_Function
263 and then not Analyzed
(Decl
)
267 -- References to Ghost entities may be relocated in internally
270 elsif Nkind
(Decl
) = N_Subprogram_Body
271 and then not Comes_From_Source
(Decl
)
273 Subp_Id
:= Corresponding_Spec
(Decl
);
275 if Present
(Subp_Id
) then
277 -- The context is the internally built _Postconditions
278 -- procedure, which is OK because the real check was done
279 -- before expansion activities.
281 if Chars
(Subp_Id
) = Name_uPostconditions
then
284 -- The context is the internally built predicate function,
285 -- which is OK because the real check was done before the
286 -- predicate function was generated.
288 elsif Is_Predicate_Function
(Subp_Id
) then
293 Original_Node
(Unit_Declaration_Node
(Subp_Id
));
295 -- The original context is an expression function that
296 -- has been split into a spec and a body. The context is
297 -- OK as long as the initial declaration is Ghost.
299 if Nkind
(Subp_Decl
) = N_Expression_Function
then
300 return Is_Ghost_Declaration
(Subp_Decl
);
304 -- Otherwise this is either an internal body or an internal
305 -- completion. Both are OK because the real check was done
306 -- before expansion activities.
314 end Is_OK_Declaration
;
320 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean is
321 procedure Check_Policies
(Prag_Nam
: Name_Id
);
322 -- Verify that the Ghost policy in effect is the same as the
323 -- assertion policy for pragma name Prag_Nam. Emit an error if
324 -- this is not the case.
330 procedure Check_Policies
(Prag_Nam
: Name_Id
) is
331 AP
: constant Name_Id
:= Check_Kind
(Prag_Nam
);
332 GP
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
335 -- If the Ghost policy in effect at the point of a Ghost entity
336 -- reference is Ignore, then the assertion policy of the pragma
337 -- must be Ignore (SPARK RM 6.9(18)).
339 if GP
= Name_Ignore
and then AP
/= Name_Ignore
then
341 ("incompatible ghost policies in effect",
344 ("\ghost entity & has policy `Ignore`",
345 Ghost_Ref
, Ghost_Id
);
347 Error_Msg_Name_1
:= AP
;
349 ("\assertion expression has policy %", Ghost_Ref
);
358 -- Start of processing for Is_OK_Pragma
361 if Nkind
(Prag
) = N_Pragma
then
362 Prag_Id
:= Get_Pragma_Id
(Prag
);
363 Prag_Nam
:= Original_Aspect_Pragma_Name
(Prag
);
365 -- A pragma that applies to a Ghost construct or specifies an
366 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
368 if Is_Ghost_Pragma
(Prag
) then
371 -- An assertion expression pragma is Ghost when it contains a
372 -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
373 -- predicate pragmas (SPARK RM 6.9(11)).
375 elsif Assertion_Expression_Pragma
(Prag_Id
)
376 and then Prag_Id
/= Pragma_Predicate
378 -- Ensure that the assertion policy and the Ghost policy are
379 -- compatible (SPARK RM 6.9(18)).
381 Check_Policies
(Prag_Nam
);
384 -- Several pragmas that may apply to a non-Ghost entity are
385 -- treated as Ghost when they contain a reference to a Ghost
386 -- entity (SPARK RM 6.9(11)).
388 elsif Nam_In
(Prag_Nam
, Name_Global
,
392 Name_Refined_Depends
,
402 ---------------------
403 -- Is_OK_Statement --
404 ---------------------
406 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean is
408 -- An assignment statement is Ghost when the target is a Ghost
411 if Nkind
(Stmt
) = N_Assignment_Statement
then
412 return Is_Ghost_Assignment
(Stmt
);
414 -- A procedure call is Ghost when it calls a Ghost procedure
416 elsif Nkind
(Stmt
) = N_Procedure_Call_Statement
then
417 return Is_Ghost_Procedure_Call
(Stmt
);
421 -- An if statement is a suitable context for a Ghost entity if it
422 -- is the byproduct of assertion expression expansion. Note that
423 -- the assertion expression may not be related to a Ghost entity,
424 -- but it may still contain references to Ghost entities.
426 elsif Nkind
(Stmt
) = N_If_Statement
427 and then Nkind
(Original_Node
(Stmt
)) = N_Pragma
428 and then Assertion_Expression_Pragma
429 (Get_Pragma_Id
(Original_Node
(Stmt
)))
441 -- Start of processing for Is_OK_Ghost_Context
444 -- The context is Ghost when it appears within a Ghost package or
447 if Ghost_Mode
> None
then
450 -- A Ghost type may be referenced in a use_type clause
451 -- (SPARK RM 6.9.10).
453 elsif Present
(Parent
(Context
))
454 and then Nkind
(Parent
(Context
)) = N_Use_Type_Clause
458 -- Routine Expand_Record_Extension creates a parent subtype without
459 -- inserting it into the tree. There is no good way of recognizing
460 -- this special case as there is no parent. Try to approximate the
463 elsif No
(Parent
(Context
)) and then Is_Tagged_Type
(Ghost_Id
) then
466 -- Otherwise climb the parent chain looking for a suitable Ghost
471 while Present
(Par
) loop
472 if Is_Ignored_Ghost_Node
(Par
) then
475 -- A reference to a Ghost entity can appear within an aspect
476 -- specification (SPARK RM 6.9(10)). The precise checking will
477 -- occur when analyzing the corresponding pragma. We make an
478 -- exception for predicate aspects that only allow referencing
479 -- a Ghost entity when the corresponding type declaration is
480 -- Ghost (SPARK RM 6.9(11)).
482 elsif Nkind
(Par
) = N_Aspect_Specification
483 and then not Same_Aspect
484 (Get_Aspect_Id
(Par
), Aspect_Predicate
)
488 elsif Is_OK_Declaration
(Par
) then
491 elsif Is_OK_Pragma
(Par
) then
494 elsif Is_OK_Statement
(Par
) then
497 -- Prevent the search from going too far
499 elsif Is_Body_Or_Package_Declaration
(Par
) then
506 -- The expansion of assertion expression pragmas and attribute Old
507 -- may cause a legal Ghost entity reference to become illegal due
508 -- to node relocation. Check the In_Assertion_Expr counter as last
509 -- resort to try and infer the original legal context.
511 if In_Assertion_Expr
> 0 then
514 -- Otherwise the context is not suitable for a reference to a
521 end Is_OK_Ghost_Context
;
523 ------------------------
524 -- Check_Ghost_Policy --
525 ------------------------
527 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
) is
528 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
531 -- The Ghost policy in effect a the point of declaration and at the
532 -- point of use must match (SPARK RM 6.9(13)).
534 if Is_Checked_Ghost_Entity
(Id
)
535 and then Policy
= Name_Ignore
536 and then May_Be_Lvalue
(Ref
)
538 Error_Msg_Sloc
:= Sloc
(Ref
);
540 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
541 Error_Msg_NE
("\& declared with ghost policy `Check`", Ref
, Id
);
542 Error_Msg_NE
("\& used # with ghost policy `Ignore`", Ref
, Id
);
544 elsif Is_Ignored_Ghost_Entity
(Id
) and then Policy
= Name_Check
then
545 Error_Msg_Sloc
:= Sloc
(Ref
);
547 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
548 Error_Msg_NE
("\& declared with ghost policy `Ignore`", Ref
, Id
);
549 Error_Msg_NE
("\& used # with ghost policy `Check`", Ref
, Id
);
551 end Check_Ghost_Policy
;
553 -- Start of processing for Check_Ghost_Context
556 -- Once it has been established that the reference to the Ghost entity
557 -- is within a suitable context, ensure that the policy at the point of
558 -- declaration and at the point of use match.
560 if Is_OK_Ghost_Context
(Ghost_Ref
) then
561 Check_Ghost_Policy
(Ghost_Id
, Ghost_Ref
);
563 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
564 -- its behavior or value (SPARK RM 6.9(10,11)).
567 Error_Msg_N
("ghost entity cannot appear in this context", Ghost_Ref
);
569 end Check_Ghost_Context
;
571 ----------------------------
572 -- Check_Ghost_Overriding --
573 ----------------------------
575 procedure Check_Ghost_Overriding
577 Overridden_Subp
: Entity_Id
)
579 Deriv_Typ
: Entity_Id
;
580 Over_Subp
: Entity_Id
;
583 if Present
(Subp
) and then Present
(Overridden_Subp
) then
584 Over_Subp
:= Ultimate_Alias
(Overridden_Subp
);
585 Deriv_Typ
:= Find_Dispatching_Type
(Subp
);
587 -- A Ghost primitive of a non-Ghost type extension cannot override an
588 -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
590 if Is_Ghost_Entity
(Subp
)
591 and then Present
(Deriv_Typ
)
592 and then not Is_Ghost_Entity
(Deriv_Typ
)
593 and then not Is_Ghost_Entity
(Over_Subp
)
594 and then not Is_Abstract_Subprogram
(Over_Subp
)
596 Error_Msg_N
("incompatible overriding in effect", Subp
);
598 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
599 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
601 Error_Msg_Sloc
:= Sloc
(Subp
);
602 Error_Msg_N
("\overridden # with ghost subprogram", Subp
);
605 -- A non-Ghost primitive of a type extension cannot override an
606 -- inherited Ghost primitive (SPARK RM 6.9(8)).
608 if Is_Ghost_Entity
(Over_Subp
)
609 and then not Is_Ghost_Entity
(Subp
)
610 and then not Is_Abstract_Subprogram
(Subp
)
612 Error_Msg_N
("incompatible overriding in effect", Subp
);
614 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
615 Error_Msg_N
("\& declared # as ghost subprogram", Subp
);
617 Error_Msg_Sloc
:= Sloc
(Subp
);
618 Error_Msg_N
("\overridden # with non-ghost subprogram", Subp
);
621 if Present
(Deriv_Typ
)
622 and then not Is_Ignored_Ghost_Entity
(Deriv_Typ
)
624 -- When a tagged type is either non-Ghost or checked Ghost and
625 -- one of its primitives overrides an inherited operation, the
626 -- overridden operation of the ancestor type must be ignored Ghost
627 -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
629 if Is_Ignored_Ghost_Entity
(Subp
) then
631 -- Both the parent subprogram and overriding subprogram are
634 if Is_Ignored_Ghost_Entity
(Over_Subp
) then
637 -- The parent subprogram carries policy Check
639 elsif Is_Checked_Ghost_Entity
(Over_Subp
) then
641 ("incompatible ghost policies in effect", Subp
);
643 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
645 ("\& declared # with ghost policy `Check`", Subp
);
647 Error_Msg_Sloc
:= Sloc
(Subp
);
649 ("\overridden # with ghost policy `Ignore`", Subp
);
651 -- The parent subprogram is non-Ghost
655 ("incompatible ghost policies in effect", Subp
);
657 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
658 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
660 Error_Msg_Sloc
:= Sloc
(Subp
);
662 ("\overridden # with ghost policy `Ignore`", Subp
);
665 -- When a tagged type is either non-Ghost or checked Ghost and
666 -- one of its primitives overrides an inherited operation, the
667 -- the primitive of the tagged type must be ignored Ghost if the
668 -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
670 elsif Is_Ignored_Ghost_Entity
(Over_Subp
) then
672 -- Both the parent subprogram and the overriding subprogram are
675 if Is_Ignored_Ghost_Entity
(Subp
) then
678 -- The overriding subprogram carries policy Check
680 elsif Is_Checked_Ghost_Entity
(Subp
) then
682 ("incompatible ghost policies in effect", Subp
);
684 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
686 ("\& declared # with ghost policy `Ignore`", Subp
);
688 Error_Msg_Sloc
:= Sloc
(Subp
);
690 ("\overridden # with Ghost policy `Check`", Subp
);
692 -- The overriding subprogram is non-Ghost
696 ("incompatible ghost policies in effect", Subp
);
698 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
700 ("\& declared # with ghost policy `Ignore`", Subp
);
702 Error_Msg_Sloc
:= Sloc
(Subp
);
704 ("\overridden # with non-ghost subprogram", Subp
);
709 end Check_Ghost_Overriding
;
711 ---------------------------
712 -- Check_Ghost_Primitive --
713 ---------------------------
715 procedure Check_Ghost_Primitive
(Prim
: Entity_Id
; Typ
: Entity_Id
) is
717 -- The Ghost policy in effect at the point of declaration of a primitive
718 -- operation and a tagged type must match (SPARK RM 6.9(16)).
720 if Is_Tagged_Type
(Typ
) then
721 if Is_Checked_Ghost_Entity
(Prim
)
722 and then Is_Ignored_Ghost_Entity
(Typ
)
724 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
726 Error_Msg_Sloc
:= Sloc
(Typ
);
728 ("\tagged type & declared # with ghost policy `Ignore`",
731 Error_Msg_Sloc
:= Sloc
(Prim
);
733 ("\primitive subprogram & declared # with ghost policy `Check`",
736 elsif Is_Ignored_Ghost_Entity
(Prim
)
737 and then Is_Checked_Ghost_Entity
(Typ
)
739 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
741 Error_Msg_Sloc
:= Sloc
(Typ
);
743 ("\tagged type & declared # with ghost policy `Check`",
746 Error_Msg_Sloc
:= Sloc
(Prim
);
748 ("\primitive subprogram & declared # with ghost policy `Ignore`",
752 end Check_Ghost_Primitive
;
754 ----------------------------
755 -- Check_Ghost_Refinement --
756 ----------------------------
758 procedure Check_Ghost_Refinement
760 State_Id
: Entity_Id
;
762 Constit_Id
: Entity_Id
)
765 if Is_Ghost_Entity
(State_Id
) then
766 if Is_Ghost_Entity
(Constit_Id
) then
768 -- The Ghost policy in effect at the point of abstract state
769 -- declaration and constituent must match (SPARK RM 6.9(15)).
771 if Is_Checked_Ghost_Entity
(State_Id
)
772 and then Is_Ignored_Ghost_Entity
(Constit_Id
)
774 Error_Msg_Sloc
:= Sloc
(Constit
);
775 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
778 ("\abstract state & declared with ghost policy `Check`",
781 ("\constituent & declared # with ghost policy `Ignore`",
784 elsif Is_Ignored_Ghost_Entity
(State_Id
)
785 and then Is_Checked_Ghost_Entity
(Constit_Id
)
787 Error_Msg_Sloc
:= Sloc
(Constit
);
788 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
791 ("\abstract state & declared with ghost policy `Ignore`",
794 ("\constituent & declared # with ghost policy `Check`",
798 -- A constituent of a Ghost abstract state must be a Ghost entity
799 -- (SPARK RM 7.2.2(12)).
803 ("constituent of ghost state & must be ghost",
807 end Check_Ghost_Refinement
;
809 ----------------------
810 -- Check_Ghost_Type --
811 ----------------------
813 procedure Check_Ghost_Type
(Typ
: Entity_Id
) is
814 Conc_Typ
: Entity_Id
;
815 Full_Typ
: Entity_Id
;
818 if Is_Ghost_Entity
(Typ
) then
822 if Is_Single_Concurrent_Type
(Typ
) then
823 Conc_Typ
:= Anonymous_Object
(Typ
);
824 Full_Typ
:= Conc_Typ
;
826 elsif Is_Concurrent_Type
(Typ
) then
830 -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
831 -- legality rule first to give a finer-grained diagnostic.
833 if Present
(Conc_Typ
) then
834 Error_Msg_N
("ghost type & cannot be concurrent", Conc_Typ
);
837 -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
839 if Is_Effectively_Volatile
(Full_Typ
) then
840 Error_Msg_N
("ghost type & cannot be volatile", Full_Typ
);
843 end Check_Ghost_Type
;
849 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
is
853 -- When the reference denotes a subcomponent, recover the related
854 -- object (SPARK RM 6.9(1)).
857 while Nkind_In
(Ref
, N_Explicit_Dereference
,
859 N_Selected_Component
,
865 if Is_Entity_Name
(Ref
) then
872 --------------------------------
873 -- Implements_Ghost_Interface --
874 --------------------------------
876 function Implements_Ghost_Interface
(Typ
: Entity_Id
) return Boolean is
877 Iface_Elmt
: Elmt_Id
;
880 -- Traverse the list of interfaces looking for a Ghost interface
882 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
883 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
884 while Present
(Iface_Elmt
) loop
885 if Is_Ghost_Entity
(Node
(Iface_Elmt
)) then
889 Next_Elmt
(Iface_Elmt
);
894 end Implements_Ghost_Interface
;
900 procedure Initialize
is
902 Ignored_Ghost_Units
.Init
;
905 ------------------------
906 -- Install_Ghost_Mode --
907 ------------------------
909 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
) is
912 end Install_Ghost_Mode
;
914 procedure Install_Ghost_Mode
(Mode
: Name_Id
) is
916 if Mode
= Name_Check
then
919 elsif Mode
= Name_Ignore
then
920 Ghost_Mode
:= Ignore
;
922 elsif Mode
= Name_None
then
925 end Install_Ghost_Mode
;
927 -------------------------
928 -- Is_Ghost_Assignment --
929 -------------------------
931 function Is_Ghost_Assignment
(N
: Node_Id
) return Boolean is
935 -- An assignment statement is Ghost when its target denotes a Ghost
938 if Nkind
(N
) = N_Assignment_Statement
then
939 Id
:= Ghost_Entity
(Name
(N
));
941 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
945 end Is_Ghost_Assignment
;
947 --------------------------
948 -- Is_Ghost_Declaration --
949 --------------------------
951 function Is_Ghost_Declaration
(N
: Node_Id
) return Boolean is
955 -- A declaration is Ghost when it elaborates a Ghost entity or is
956 -- subject to pragma Ghost.
958 if Is_Declaration
(N
) then
959 Id
:= Defining_Entity
(N
);
961 return Is_Ghost_Entity
(Id
) or else Is_Subject_To_Ghost
(N
);
965 end Is_Ghost_Declaration
;
967 ---------------------
968 -- Is_Ghost_Pragma --
969 ---------------------
971 function Is_Ghost_Pragma
(N
: Node_Id
) return Boolean is
973 return Is_Checked_Ghost_Pragma
(N
) or else Is_Ignored_Ghost_Pragma
(N
);
976 -----------------------------
977 -- Is_Ghost_Procedure_Call --
978 -----------------------------
980 function Is_Ghost_Procedure_Call
(N
: Node_Id
) return Boolean is
984 -- A procedure call is Ghost when it invokes a Ghost procedure
986 if Nkind
(N
) = N_Procedure_Call_Statement
then
987 Id
:= Ghost_Entity
(Name
(N
));
989 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
993 end Is_Ghost_Procedure_Call
;
995 ---------------------------
996 -- Is_Ignored_Ghost_Unit --
997 ---------------------------
999 function Is_Ignored_Ghost_Unit
(N
: Node_Id
) return Boolean is
1001 -- Inspect the original node of the unit in case removal of ignored
1002 -- Ghost code has already taken place.
1005 Nkind
(N
) = N_Compilation_Unit
1006 and then Is_Ignored_Ghost_Entity
1007 (Defining_Entity
(Original_Node
(Unit
(N
))));
1008 end Is_Ignored_Ghost_Unit
;
1010 -------------------------
1011 -- Is_Subject_To_Ghost --
1012 -------------------------
1014 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean is
1015 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean;
1016 -- Determine whether aspect or pragma argument Arg enables "ghostness"
1018 -----------------------
1019 -- Enables_Ghostness --
1020 -----------------------
1022 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean is
1028 if Nkind
(Expr
) = N_Pragma_Argument_Association
then
1029 Expr
:= Get_Pragma_Arg
(Expr
);
1032 -- Determine whether the expression of the aspect or pragma is static
1033 -- and denotes True.
1035 if Present
(Expr
) then
1036 Preanalyze_And_Resolve
(Expr
);
1039 Is_OK_Static_Expression
(Expr
)
1040 and then Is_True
(Expr_Value
(Expr
));
1042 -- Otherwise Ghost defaults to True
1047 end Enables_Ghostness
;
1051 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1054 Prev_Id
: Entity_Id
;
1056 -- Start of processing for Is_Subject_To_Ghost
1059 -- The related entity of the declaration has not been analyzed yet, do
1060 -- not inspect its attributes.
1062 if Ekind
(Id
) = E_Void
then
1065 elsif Is_Ghost_Entity
(Id
) then
1068 -- The completion of a type or a constant is not fully analyzed when the
1069 -- reference to the Ghost entity is resolved. Because the completion is
1070 -- not marked as Ghost yet, inspect the partial view.
1072 elsif Is_Record_Type
(Id
)
1073 or else Ekind
(Id
) = E_Constant
1074 or else (Nkind
(N
) = N_Object_Declaration
1075 and then Constant_Present
(N
))
1077 Prev_Id
:= Incomplete_Or_Partial_View
(Id
);
1079 if Present
(Prev_Id
) and then Is_Ghost_Entity
(Prev_Id
) then
1084 -- Examine the aspect specifications (if any) looking for aspect Ghost
1086 if Permits_Aspect_Specifications
(N
) then
1087 Asp
:= First
(Aspect_Specifications
(N
));
1088 while Present
(Asp
) loop
1089 if Chars
(Identifier
(Asp
)) = Name_Ghost
then
1090 return Enables_Ghostness
(Expression
(Asp
));
1099 -- When the context is a [generic] package declaration, pragma Ghost
1100 -- resides in the visible declarations.
1102 if Nkind_In
(N
, N_Generic_Package_Declaration
,
1103 N_Package_Declaration
)
1105 Decl
:= First
(Visible_Declarations
(Specification
(N
)));
1107 -- When the context is a package or a subprogram body, pragma Ghost
1108 -- resides in the declarative part.
1110 elsif Nkind_In
(N
, N_Package_Body
, N_Subprogram_Body
) then
1111 Decl
:= First
(Declarations
(N
));
1113 -- Otherwise pragma Ghost appears in the declarations following N
1115 elsif Is_List_Member
(N
) then
1119 while Present
(Decl
) loop
1120 if Nkind
(Decl
) = N_Pragma
1121 and then Pragma_Name
(Decl
) = Name_Ghost
1124 Enables_Ghostness
(First
(Pragma_Argument_Associations
(Decl
)));
1126 -- A source construct ends the region where pragma Ghost may appear,
1127 -- stop the traversal. Check the original node as source constructs
1128 -- may be rewritten into something else by expansion.
1130 elsif Comes_From_Source
(Original_Node
(Decl
)) then
1138 end Is_Subject_To_Ghost
;
1146 Ignored_Ghost_Units
.Release
;
1147 Ignored_Ghost_Units
.Locked
:= True;
1150 -----------------------------------
1151 -- Mark_And_Set_Ghost_Assignment --
1152 -----------------------------------
1154 procedure Mark_And_Set_Ghost_Assignment
(N
: Node_Id
) is
1158 -- An assignment statement becomes Ghost when its target denotes a Ghost
1159 -- object. Install the Ghost mode of the target.
1161 Id
:= Ghost_Entity
(Name
(N
));
1163 if Present
(Id
) then
1164 if Is_Checked_Ghost_Entity
(Id
) then
1165 Install_Ghost_Mode
(Check
);
1167 elsif Is_Ignored_Ghost_Entity
(Id
) then
1168 Install_Ghost_Mode
(Ignore
);
1170 Set_Is_Ignored_Ghost_Node
(N
);
1171 Propagate_Ignored_Ghost_Code
(N
);
1174 end Mark_And_Set_Ghost_Assignment
;
1176 -----------------------------
1177 -- Mark_And_Set_Ghost_Body --
1178 -----------------------------
1180 procedure Mark_And_Set_Ghost_Body
1182 Spec_Id
: Entity_Id
)
1184 Body_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1185 Policy
: Name_Id
:= No_Name
;
1188 -- A body becomes Ghost when it is subject to aspect or pragma Ghost
1190 if Is_Subject_To_Ghost
(N
) then
1191 Policy
:= Policy_In_Effect
(Name_Ghost
);
1193 -- A body declared within a Ghost region is automatically Ghost
1194 -- (SPARK RM 6.9(2)).
1196 elsif Ghost_Mode
= Check
then
1197 Policy
:= Name_Check
;
1199 elsif Ghost_Mode
= Ignore
then
1200 Policy
:= Name_Ignore
;
1202 -- Inherit the "ghostness" of the previous declaration when the body
1203 -- acts as a completion.
1205 elsif Present
(Spec_Id
) then
1206 if Is_Checked_Ghost_Entity
(Spec_Id
) then
1207 Policy
:= Name_Check
;
1209 elsif Is_Ignored_Ghost_Entity
(Spec_Id
) then
1210 Policy
:= Name_Ignore
;
1214 -- The Ghost policy in effect at the point of declaration and at the
1215 -- point of completion must match (SPARK RM 6.9(14)).
1217 Check_Ghost_Completion
1218 (Prev_Id
=> Spec_Id
,
1219 Compl_Id
=> Body_Id
);
1221 -- Mark the body as its formals as Ghost
1223 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1225 -- Install the appropriate Ghost mode
1227 Install_Ghost_Mode
(Policy
);
1228 end Mark_And_Set_Ghost_Body
;
1230 -----------------------------------
1231 -- Mark_And_Set_Ghost_Completion --
1232 -----------------------------------
1234 procedure Mark_And_Set_Ghost_Completion
1236 Prev_Id
: Entity_Id
)
1238 Compl_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1239 Policy
: Name_Id
:= No_Name
;
1242 -- A completion elaborated in a Ghost region is automatically Ghost
1243 -- (SPARK RM 6.9(2)).
1245 if Ghost_Mode
= Check
then
1246 Policy
:= Name_Check
;
1248 elsif Ghost_Mode
= Ignore
then
1249 Policy
:= Name_Ignore
;
1251 -- The completion becomes Ghost when its initial declaration is also
1254 elsif Is_Checked_Ghost_Entity
(Prev_Id
) then
1255 Policy
:= Name_Check
;
1257 elsif Is_Ignored_Ghost_Entity
(Prev_Id
) then
1258 Policy
:= Name_Ignore
;
1261 -- The Ghost policy in effect at the point of declaration and at the
1262 -- point of completion must match (SPARK RM 6.9(14)).
1264 Check_Ghost_Completion
1265 (Prev_Id
=> Prev_Id
,
1266 Compl_Id
=> Compl_Id
);
1268 -- Mark the completion as Ghost
1270 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1272 -- Install the appropriate Ghost mode
1274 Install_Ghost_Mode
(Policy
);
1275 end Mark_And_Set_Ghost_Completion
;
1277 ------------------------------------
1278 -- Mark_And_Set_Ghost_Declaration --
1279 ------------------------------------
1281 procedure Mark_And_Set_Ghost_Declaration
(N
: Node_Id
) is
1283 Policy
: Name_Id
:= No_Name
;
1286 -- A declaration becomes Ghost when it is subject to aspect or pragma
1289 if Is_Subject_To_Ghost
(N
) then
1290 Policy
:= Policy_In_Effect
(Name_Ghost
);
1292 -- A declaration elaborated in a Ghost region is automatically Ghost
1293 -- (SPARK RM 6.9(2)).
1295 elsif Ghost_Mode
= Check
then
1296 Policy
:= Name_Check
;
1298 elsif Ghost_Mode
= Ignore
then
1299 Policy
:= Name_Ignore
;
1301 -- A child package or subprogram declaration becomes Ghost when its
1302 -- parent is Ghost (SPARK RM 6.9(2)).
1304 elsif Nkind_In
(N
, N_Generic_Function_Renaming_Declaration
,
1305 N_Generic_Package_Declaration
,
1306 N_Generic_Package_Renaming_Declaration
,
1307 N_Generic_Procedure_Renaming_Declaration
,
1308 N_Generic_Subprogram_Declaration
,
1309 N_Package_Declaration
,
1310 N_Package_Renaming_Declaration
,
1311 N_Subprogram_Declaration
,
1312 N_Subprogram_Renaming_Declaration
)
1313 and then Present
(Parent_Spec
(N
))
1315 Par_Id
:= Defining_Entity
(Unit
(Parent_Spec
(N
)));
1317 if Is_Checked_Ghost_Entity
(Par_Id
) then
1318 Policy
:= Name_Check
;
1320 elsif Is_Ignored_Ghost_Entity
(Par_Id
) then
1321 Policy
:= Name_Ignore
;
1325 -- Mark the declaration and its formals as Ghost
1327 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1329 -- Install the appropriate Ghost mode
1331 Install_Ghost_Mode
(Policy
);
1332 end Mark_And_Set_Ghost_Declaration
;
1334 --------------------------------------
1335 -- Mark_And_Set_Ghost_Instantiation --
1336 --------------------------------------
1338 procedure Mark_And_Set_Ghost_Instantiation
1342 procedure Check_Ghost_Actuals
;
1343 -- Check the context of ghost actuals
1345 -------------------------
1346 -- Check_Ghost_Actuals --
1347 -------------------------
1349 procedure Check_Ghost_Actuals
is
1350 Assoc
: Node_Id
:= First
(Generic_Associations
(N
));
1354 while Present
(Assoc
) loop
1355 if Nkind
(Assoc
) /= N_Others_Choice
then
1356 Act
:= Explicit_Generic_Actual_Parameter
(Assoc
);
1358 -- Within a nested instantiation, a defaulted actual is an
1359 -- empty association, so nothing to check.
1364 elsif Comes_From_Source
(Act
)
1365 and then Nkind
(Act
) in N_Has_Etype
1366 and then Present
(Etype
(Act
))
1367 and then Is_Ghost_Entity
(Etype
(Act
))
1369 Check_Ghost_Context
(Etype
(Act
), Act
);
1375 end Check_Ghost_Actuals
;
1379 Policy
: Name_Id
:= No_Name
;
1382 -- An instantiation becomes Ghost when it is subject to pragma Ghost
1384 if Is_Subject_To_Ghost
(N
) then
1385 Policy
:= Policy_In_Effect
(Name_Ghost
);
1387 -- An instantiation declaration within a Ghost region is automatically
1388 -- Ghost (SPARK RM 6.9(2)).
1390 elsif Ghost_Mode
= Check
then
1391 Policy
:= Name_Check
;
1393 elsif Ghost_Mode
= Ignore
then
1394 Policy
:= Name_Ignore
;
1396 -- Inherit the "ghostness" of the generic unit
1398 elsif Is_Checked_Ghost_Entity
(Gen_Id
) then
1399 Policy
:= Name_Check
;
1401 elsif Is_Ignored_Ghost_Entity
(Gen_Id
) then
1402 Policy
:= Name_Ignore
;
1405 -- Mark the instantiation as Ghost
1407 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1409 -- Install the appropriate Ghost mode
1411 Install_Ghost_Mode
(Policy
);
1413 -- Check ghost actuals. Given that this routine is unconditionally
1414 -- invoked with subprogram and package instantiations, this check
1415 -- verifies the context of all the ghost entities passed in generic
1418 Check_Ghost_Actuals
;
1419 end Mark_And_Set_Ghost_Instantiation
;
1421 ---------------------------------------
1422 -- Mark_And_Set_Ghost_Procedure_Call --
1423 ---------------------------------------
1425 procedure Mark_And_Set_Ghost_Procedure_Call
(N
: Node_Id
) is
1429 -- A procedure call becomes Ghost when the procedure being invoked is
1430 -- Ghost. Install the Ghost mode of the procedure.
1432 Id
:= Ghost_Entity
(Name
(N
));
1434 if Present
(Id
) then
1435 if Is_Checked_Ghost_Entity
(Id
) then
1436 Install_Ghost_Mode
(Check
);
1438 elsif Is_Ignored_Ghost_Entity
(Id
) then
1439 Install_Ghost_Mode
(Ignore
);
1441 Set_Is_Ignored_Ghost_Node
(N
);
1442 Propagate_Ignored_Ghost_Code
(N
);
1445 end Mark_And_Set_Ghost_Procedure_Call
;
1447 ------------------------------------
1448 -- Mark_Ghost_Declaration_Or_Body --
1449 ------------------------------------
1451 procedure Mark_Ghost_Declaration_Or_Body
1455 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1457 Mark_Formals
: Boolean := False;
1459 Param_Id
: Entity_Id
;
1462 -- Mark the related node and its entity
1464 if Mode
= Name_Check
then
1465 Mark_Formals
:= True;
1466 Set_Is_Checked_Ghost_Entity
(Id
);
1468 elsif Mode
= Name_Ignore
then
1469 Mark_Formals
:= True;
1470 Set_Is_Ignored_Ghost_Entity
(Id
);
1471 Set_Is_Ignored_Ghost_Node
(N
);
1472 Propagate_Ignored_Ghost_Code
(N
);
1475 -- Mark all formal parameters when the related node denotes a subprogram
1476 -- or a body. The traversal is performed via the specification because
1477 -- the related subprogram or body may be unanalyzed.
1479 -- ??? could extra formal parameters cause a Ghost leak?
1482 and then Nkind_In
(N
, N_Abstract_Subprogram_Declaration
,
1483 N_Formal_Abstract_Subprogram_Declaration
,
1484 N_Formal_Concrete_Subprogram_Declaration
,
1485 N_Generic_Subprogram_Declaration
,
1487 N_Subprogram_Body_Stub
,
1488 N_Subprogram_Declaration
,
1489 N_Subprogram_Renaming_Declaration
)
1491 Param
:= First
(Parameter_Specifications
(Specification
(N
)));
1492 while Present
(Param
) loop
1493 Param_Id
:= Defining_Entity
(Param
);
1495 if Mode
= Name_Check
then
1496 Set_Is_Checked_Ghost_Entity
(Param_Id
);
1498 elsif Mode
= Name_Ignore
then
1499 Set_Is_Ignored_Ghost_Entity
(Param_Id
);
1505 end Mark_Ghost_Declaration_Or_Body
;
1507 -----------------------
1508 -- Mark_Ghost_Clause --
1509 -----------------------
1511 procedure Mark_Ghost_Clause
(N
: Node_Id
) is
1512 Nam
: Node_Id
:= Empty
;
1515 if Nkind
(N
) = N_Use_Package_Clause
then
1518 elsif Nkind
(N
) = N_Use_Type_Clause
then
1519 Nam
:= Subtype_Mark
(N
);
1521 elsif Nkind
(N
) = N_With_Clause
then
1526 and then Is_Entity_Name
(Nam
)
1527 and then Present
(Entity
(Nam
))
1528 and then Is_Ignored_Ghost_Entity
(Entity
(Nam
))
1530 Set_Is_Ignored_Ghost_Node
(N
);
1531 Propagate_Ignored_Ghost_Code
(N
);
1533 end Mark_Ghost_Clause
;
1535 -----------------------
1536 -- Mark_Ghost_Pragma --
1537 -----------------------
1539 procedure Mark_Ghost_Pragma
1544 -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
1547 if Is_Checked_Ghost_Entity
(Id
) then
1548 Set_Is_Checked_Ghost_Pragma
(N
);
1550 elsif Is_Ignored_Ghost_Entity
(Id
) then
1551 Set_Is_Ignored_Ghost_Pragma
(N
);
1552 Set_Is_Ignored_Ghost_Node
(N
);
1553 Propagate_Ignored_Ghost_Code
(N
);
1555 end Mark_Ghost_Pragma
;
1557 -------------------------
1558 -- Mark_Ghost_Renaming --
1559 -------------------------
1561 procedure Mark_Ghost_Renaming
1565 Policy
: Name_Id
:= No_Name
;
1568 -- A renaming becomes Ghost when it renames a Ghost entity
1570 if Is_Checked_Ghost_Entity
(Id
) then
1571 Policy
:= Name_Check
;
1573 elsif Is_Ignored_Ghost_Entity
(Id
) then
1574 Policy
:= Name_Ignore
;
1577 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1578 end Mark_Ghost_Renaming
;
1580 ----------------------------------
1581 -- Propagate_Ignored_Ghost_Code --
1582 ----------------------------------
1584 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
) is
1589 -- Traverse the parent chain looking for blocks, packages, and
1590 -- subprograms or their respective bodies.
1593 while Present
(Nod
) loop
1596 if Nkind
(Nod
) = N_Block_Statement
1597 and then Present
(Identifier
(Nod
))
1599 Scop
:= Entity
(Identifier
(Nod
));
1601 elsif Nkind_In
(Nod
, N_Package_Body
,
1602 N_Package_Declaration
,
1604 N_Subprogram_Declaration
)
1606 Scop
:= Defining_Entity
(Nod
);
1609 -- The current node denotes a scoping construct
1611 if Present
(Scop
) then
1613 -- Stop the traversal when the scope already contains ignored
1614 -- Ghost code as all enclosing scopes have already been marked.
1616 if Contains_Ignored_Ghost_Code
(Scop
) then
1619 -- Otherwise mark this scope and keep climbing
1622 Set_Contains_Ignored_Ghost_Code
(Scop
);
1626 Nod
:= Parent
(Nod
);
1629 -- The unit containing the ignored Ghost code must be post processed
1630 -- before invoking the back end.
1632 Add_Ignored_Ghost_Unit
(Cunit
(Get_Code_Unit
(N
)));
1633 end Propagate_Ignored_Ghost_Code
;
1635 -------------------------------
1636 -- Remove_Ignored_Ghost_Code --
1637 -------------------------------
1639 procedure Remove_Ignored_Ghost_Code
is
1640 procedure Prune_Tree
(Root
: Node_Id
);
1641 -- Remove all code marked as ignored Ghost from the tree of denoted by
1648 procedure Prune_Tree
(Root
: Node_Id
) is
1649 procedure Prune
(N
: Node_Id
);
1650 -- Remove a given node from the tree by rewriting it into null
1652 function Prune_Node
(N
: Node_Id
) return Traverse_Result
;
1653 -- Determine whether node N denotes an ignored Ghost construct. If
1654 -- this is the case, rewrite N as a null statement. See the body for
1661 procedure Prune
(N
: Node_Id
) is
1663 -- Destroy any aspects that may be associated with the node
1665 if Permits_Aspect_Specifications
(N
) and then Has_Aspects
(N
) then
1669 Rewrite
(N
, Make_Null_Statement
(Sloc
(N
)));
1676 function Prune_Node
(N
: Node_Id
) return Traverse_Result
is
1680 -- Do not prune compilation unit nodes because many mechanisms
1681 -- depend on their presence. Note that context items are still
1684 if Nkind
(N
) = N_Compilation_Unit
then
1687 -- The node is either declared as ignored Ghost or is a byproduct
1688 -- of expansion. Destroy it and stop the traversal on this branch.
1690 elsif Is_Ignored_Ghost_Node
(N
) then
1694 -- Scoping constructs such as blocks, packages, subprograms and
1695 -- bodies offer some flexibility with respect to pruning.
1697 elsif Nkind_In
(N
, N_Block_Statement
,
1699 N_Package_Declaration
,
1701 N_Subprogram_Declaration
)
1703 if Nkind
(N
) = N_Block_Statement
then
1704 Id
:= Entity
(Identifier
(N
));
1706 Id
:= Defining_Entity
(N
);
1709 -- The scoping construct contains both living and ignored Ghost
1710 -- code, let the traversal prune all relevant nodes.
1712 if Contains_Ignored_Ghost_Code
(Id
) then
1715 -- Otherwise the construct contains only living code and should
1722 -- Otherwise keep searching for ignored Ghost nodes
1729 procedure Prune_Nodes
is new Traverse_Proc
(Prune_Node
);
1731 -- Start of processing for Prune_Tree
1737 -- Start of processing for Remove_Ignored_Ghost_Code
1740 for Index
in Ignored_Ghost_Units
.First
.. Ignored_Ghost_Units
.Last
loop
1741 Prune_Tree
(Ignored_Ghost_Units
.Table
(Index
));
1743 end Remove_Ignored_Ghost_Code
;
1745 ------------------------
1746 -- Restore_Ghost_Mode --
1747 ------------------------
1749 procedure Restore_Ghost_Mode
(Mode
: Ghost_Mode_Type
) is
1752 end Restore_Ghost_Mode
;
1754 --------------------
1755 -- Set_Ghost_Mode --
1756 --------------------
1758 procedure Set_Ghost_Mode
(N
: Node_Or_Entity_Id
) is
1759 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
);
1760 -- Install the Ghost mode of entity Id
1762 --------------------------------
1763 -- Set_Ghost_Mode_From_Entity --
1764 --------------------------------
1766 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
) is
1768 if Is_Checked_Ghost_Entity
(Id
) then
1769 Install_Ghost_Mode
(Check
);
1770 elsif Is_Ignored_Ghost_Entity
(Id
) then
1771 Install_Ghost_Mode
(Ignore
);
1773 Install_Ghost_Mode
(None
);
1775 end Set_Ghost_Mode_From_Entity
;
1781 -- Start of processing for Set_Ghost_Mode
1784 -- The Ghost mode of an assignment statement depends on the Ghost mode
1787 if Nkind
(N
) = N_Assignment_Statement
then
1788 Id
:= Ghost_Entity
(Name
(N
));
1790 if Present
(Id
) then
1791 Set_Ghost_Mode_From_Entity
(Id
);
1794 -- The Ghost mode of a body or a declaration depends on the Ghost mode
1795 -- of its defining entity.
1797 elsif Is_Body
(N
) or else Is_Declaration
(N
) then
1798 Set_Ghost_Mode_From_Entity
(Defining_Entity
(N
));
1800 -- The Ghost mode of an entity depends on the entity itself
1802 elsif Nkind
(N
) in N_Entity
then
1803 Set_Ghost_Mode_From_Entity
(N
);
1805 -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
1806 -- of the entity being frozen.
1808 elsif Nkind_In
(N
, N_Freeze_Entity
, N_Freeze_Generic_Entity
) then
1809 Set_Ghost_Mode_From_Entity
(Entity
(N
));
1811 -- The Ghost mode of a pragma depends on the associated entity. The
1812 -- property is encoded in the pragma itself.
1814 elsif Nkind
(N
) = N_Pragma
then
1815 if Is_Checked_Ghost_Pragma
(N
) then
1816 Install_Ghost_Mode
(Check
);
1817 elsif Is_Ignored_Ghost_Pragma
(N
) then
1818 Install_Ghost_Mode
(Ignore
);
1820 Install_Ghost_Mode
(None
);
1823 -- The Ghost mode of a procedure call depends on the Ghost mode of the
1824 -- procedure being invoked.
1826 elsif Nkind
(N
) = N_Procedure_Call_Statement
then
1827 Id
:= Ghost_Entity
(Name
(N
));
1829 if Present
(Id
) then
1830 Set_Ghost_Mode_From_Entity
(Id
);
1835 -------------------------
1836 -- Set_Is_Ghost_Entity --
1837 -------------------------
1839 procedure Set_Is_Ghost_Entity
(Id
: Entity_Id
) is
1840 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
1842 if Policy
= Name_Check
then
1843 Set_Is_Checked_Ghost_Entity
(Id
);
1844 elsif Policy
= Name_Ignore
then
1845 Set_Is_Ignored_Ghost_Entity
(Id
);
1847 end Set_Is_Ghost_Entity
;