1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
9 -- Copyright (C) 2014-2015, 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 ------------------------------------------------------------------------------
26 with Alloc
; use Alloc
;
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
;
38 with Sem_Aux
; use Sem_Aux
;
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 -- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
68 -- a reference to a Ghost entity. Return Empty if there is no such entity.
70 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
);
71 -- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
72 -- Signal all enclosing scopes that they now contain ignored Ghost code.
73 -- Add the compilation unit containing N to table Ignored_Ghost_Units for
76 ----------------------------
77 -- Add_Ignored_Ghost_Unit --
78 ----------------------------
80 procedure Add_Ignored_Ghost_Unit
(Unit
: Node_Id
) is
82 pragma Assert
(Nkind
(Unit
) = N_Compilation_Unit
);
84 -- Avoid duplicates in the table as pruning the same unit more than once
85 -- is wasteful. Since ignored Ghost code tends to be grouped up, check
86 -- the contents of the table in reverse.
88 for Index
in reverse Ignored_Ghost_Units
.First
..
89 Ignored_Ghost_Units
.Last
91 -- If the unit is already present in the table, do not add it again
93 if Unit
= Ignored_Ghost_Units
.Table
(Index
) then
98 -- If we get here, then this is the first time the unit is being added
100 Ignored_Ghost_Units
.Append
(Unit
);
101 end Add_Ignored_Ghost_Unit
;
103 ----------------------------
104 -- Check_Ghost_Completion --
105 ----------------------------
107 procedure Check_Ghost_Completion
108 (Partial_View
: Entity_Id
;
109 Full_View
: Entity_Id
)
111 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
114 -- The Ghost policy in effect at the point of declaration and at the
115 -- point of completion must match (SPARK RM 6.9(14)).
117 if Is_Checked_Ghost_Entity
(Partial_View
)
118 and then Policy
= Name_Ignore
120 Error_Msg_Sloc
:= Sloc
(Full_View
);
122 Error_Msg_N
("incompatible ghost policies in effect", Partial_View
);
123 Error_Msg_N
("\& declared with ghost policy `Check`", Partial_View
);
124 Error_Msg_N
("\& completed # with ghost policy `Ignore`",
127 elsif Is_Ignored_Ghost_Entity
(Partial_View
)
128 and then Policy
= Name_Check
130 Error_Msg_Sloc
:= Sloc
(Full_View
);
132 Error_Msg_N
("incompatible ghost policies in effect", Partial_View
);
133 Error_Msg_N
("\& declared with ghost policy `Ignore`", Partial_View
);
134 Error_Msg_N
("\& completed # with ghost policy `Check`",
137 end Check_Ghost_Completion
;
139 -------------------------
140 -- Check_Ghost_Context --
141 -------------------------
143 procedure Check_Ghost_Context
(Ghost_Id
: Entity_Id
; Ghost_Ref
: Node_Id
) is
144 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Err_N
: Node_Id
);
145 -- Verify that the Ghost policy at the point of declaration of entity Id
146 -- matches the policy at the point of reference. If this is not the case
147 -- emit an error at Err_N.
149 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean;
150 -- Determine whether node Context denotes a Ghost-friendly context where
151 -- a Ghost entity can safely reside.
153 -------------------------
154 -- Is_OK_Ghost_Context --
155 -------------------------
157 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean is
158 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean;
159 -- Determine whether node Decl is a suitable context for a reference
160 -- to a Ghost entity. To qualify as such, Decl must either
161 -- 1) Be subject to pragma Ghost
162 -- 2) Rename a Ghost entity
164 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean;
165 -- Determine whether node Prag is a suitable context for a reference
166 -- to a Ghost entity. To qualify as such, Prag must either
167 -- 1) Be an assertion expression pragma
168 -- 2) Denote pragma Global, Depends, Initializes, Refined_Global,
169 -- Refined_Depends or Refined_State
170 -- 3) Specify an aspect of a Ghost entity
171 -- 4) Contain a reference to a Ghost entity
173 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean;
174 -- Determine whether node Stmt is a suitable context for a reference
175 -- to a Ghost entity. To qualify as such, Stmt must either
176 -- 1) Denote a call to a Ghost procedure
177 -- 2) Denote an assignment statement whose target is Ghost
179 -----------------------
180 -- Is_OK_Declaration --
181 -----------------------
183 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean is
184 function Is_Ghost_Renaming
(Ren_Decl
: Node_Id
) return Boolean;
185 -- Determine whether node Ren_Decl denotes a renaming declaration
186 -- with a Ghost name.
188 -----------------------
189 -- Is_Ghost_Renaming --
190 -----------------------
192 function Is_Ghost_Renaming
(Ren_Decl
: Node_Id
) return Boolean is
196 if Is_Renaming_Declaration
(Ren_Decl
) then
197 Nam_Id
:= Ghost_Entity
(Name
(Ren_Decl
));
199 return Present
(Nam_Id
) and then Is_Ghost_Entity
(Nam_Id
);
203 end Is_Ghost_Renaming
;
210 -- Start of processing for Is_OK_Declaration
213 if Is_Declaration
(Decl
) then
215 -- A renaming declaration is Ghost when it renames a Ghost
218 if Is_Ghost_Renaming
(Decl
) then
221 -- The declaration may not have been analyzed yet, determine
222 -- whether it is subject to pragma Ghost.
224 elsif Is_Subject_To_Ghost
(Decl
) then
227 -- The declaration appears within an assertion expression
229 elsif In_Assertion_Expr
> 0 then
235 -- A reference to a Ghost entity may appear as the default
236 -- expression of a formal parameter of a subprogram body. This
237 -- context must be treated as suitable because the relation
238 -- between the spec and the body has not been established and
239 -- the body is not marked as Ghost yet. The real check was
240 -- performed on the spec.
242 elsif Nkind
(Decl
) = N_Parameter_Specification
243 and then Nkind
(Parent
(Parent
(Decl
))) = N_Subprogram_Body
247 -- References to Ghost entities may be relocated in internally
250 elsif Nkind
(Decl
) = N_Subprogram_Body
251 and then not Comes_From_Source
(Decl
)
253 Subp_Id
:= Corresponding_Spec
(Decl
);
255 -- The original context is an expression function that has
256 -- been split into a spec and a body. The context is OK as
257 -- long as the initial declaration is Ghost.
259 if Present
(Subp_Id
) then
260 Subp_Decl
:= Original_Node
(Unit_Declaration_Node
(Subp_Id
));
262 if Nkind
(Subp_Decl
) = N_Expression_Function
then
263 return Is_Subject_To_Ghost
(Subp_Decl
);
266 -- Otherwise this is either an internal body or an internal
267 -- completion. Both are OK because the real check was done
268 -- before expansion activities.
276 end Is_OK_Declaration
;
282 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean is
283 procedure Check_Policies
(Prag_Nam
: Name_Id
);
284 -- Verify that the Ghost policy in effect is the same as the
285 -- assertion policy for pragma name Prag_Nam. Emit an error if
286 -- this is not the case.
292 procedure Check_Policies
(Prag_Nam
: Name_Id
) is
293 AP
: constant Name_Id
:= Check_Kind
(Prag_Nam
);
294 GP
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
297 -- If the Ghost policy in effect at the point of a Ghost entity
298 -- reference is Ignore, then the assertion policy of the pragma
299 -- must be Ignore (SPARK RM 6.9(18)).
301 if GP
= Name_Ignore
and then AP
/= Name_Ignore
then
303 ("incompatible ghost policies in effect",
306 ("\ghost entity & has policy `Ignore`",
307 Ghost_Ref
, Ghost_Id
);
309 Error_Msg_Name_1
:= AP
;
311 ("\assertion expression has policy %", Ghost_Ref
);
322 -- Start of processing for Is_OK_Pragma
325 if Nkind
(Prag
) = N_Pragma
then
326 Prag_Id
:= Get_Pragma_Id
(Prag
);
327 Prag_Nam
:= Original_Aspect_Pragma_Name
(Prag
);
329 -- A pragma that applies to a Ghost construct or specifies an
330 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
332 if Is_Ghost_Pragma
(Prag
) then
335 -- An assertion expression is a Ghost pragma when it contains a
336 -- reference to a Ghost entity (SPARK RM 6.9(11)).
338 elsif Assertion_Expression_Pragma
(Prag_Id
) then
340 -- Predicates are excluded from this category when they do
341 -- not apply to a Ghost subtype (SPARK RM 6.9(12)).
343 if Nam_In
(Prag_Nam
, Name_Dynamic_Predicate
,
345 Name_Static_Predicate
)
349 -- Otherwise ensure that the assertion policy and the Ghost
350 -- policy are compatible (SPARK RM 6.9(18)).
353 Check_Policies
(Prag_Nam
);
357 -- Several pragmas that may apply to a non-Ghost entity are
358 -- treated as Ghost when they contain a reference to a Ghost
359 -- entity (SPARK RM 6.9(12)).
361 elsif Nam_In
(Prag_Nam
, Name_Global
,
365 Name_Refined_Depends
,
370 -- Otherwise a normal pragma is Ghost when it encloses a Ghost
371 -- name (SPARK RM 6.9(3)).
374 Arg
:= First
(Pragma_Argument_Associations
(Prag
));
375 while Present
(Arg
) loop
376 Arg_Id
:= Ghost_Entity
(Get_Pragma_Arg
(Arg
));
378 if Present
(Arg_Id
) and then Is_Ghost_Entity
(Arg_Id
) then
390 ---------------------
391 -- Is_OK_Statement --
392 ---------------------
394 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean is
398 -- An assignment statement or a procedure call is Ghost when the
399 -- name denotes a Ghost entity.
401 if Nkind_In
(Stmt
, N_Assignment_Statement
,
402 N_Procedure_Call_Statement
)
404 Nam_Id
:= Ghost_Entity
(Name
(Stmt
));
406 return Present
(Nam_Id
) and then Is_Ghost_Entity
(Nam_Id
);
410 -- An if statement is a suitable context for a Ghost entity if it
411 -- is the byproduct of assertion expression expansion.
413 elsif Nkind
(Stmt
) = N_If_Statement
414 and then Nkind
(Original_Node
(Stmt
)) = N_Pragma
415 and then Assertion_Expression_Pragma
416 (Get_Pragma_Id
(Original_Node
(Stmt
)))
428 -- Start of processing for Is_OK_Ghost_Context
431 -- The context is Ghost when it appears within a Ghost package or
434 if Ghost_Mode
> None
then
437 -- Routine Expand_Record_Extension creates a parent subtype without
438 -- inserting it into the tree. There is no good way of recognizing
439 -- this special case as there is no parent. Try to approximate the
442 elsif No
(Parent
(Context
)) and then Is_Tagged_Type
(Ghost_Id
) then
445 -- Otherwise climb the parent chain looking for a suitable Ghost
450 while Present
(Par
) loop
451 if Is_Ignored_Ghost_Node
(Par
) then
454 -- A reference to a Ghost entity can appear within an aspect
455 -- specification (SPARK RM 6.9(11)).
457 elsif Nkind
(Par
) = N_Aspect_Specification
then
460 elsif Is_OK_Declaration
(Par
) then
463 elsif Is_OK_Pragma
(Par
) then
466 elsif Is_OK_Statement
(Par
) then
469 -- Prevent the search from going too far
471 elsif Is_Body_Or_Package_Declaration
(Par
) then
480 end Is_OK_Ghost_Context
;
482 ------------------------
483 -- Check_Ghost_Policy --
484 ------------------------
486 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Err_N
: Node_Id
) is
487 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
490 -- The Ghost policy in effect a the point of declaration and at the
491 -- point of use must match (SPARK RM 6.9(14)).
493 if Is_Checked_Ghost_Entity
(Id
) and then Policy
= Name_Ignore
then
494 Error_Msg_Sloc
:= Sloc
(Err_N
);
496 Error_Msg_N
("incompatible ghost policies in effect", Err_N
);
497 Error_Msg_NE
("\& declared with ghost policy `Check`", Err_N
, Id
);
498 Error_Msg_NE
("\& used # with ghost policy `Ignore`", Err_N
, Id
);
500 elsif Is_Ignored_Ghost_Entity
(Id
) and then Policy
= Name_Check
then
501 Error_Msg_Sloc
:= Sloc
(Err_N
);
503 Error_Msg_N
("incompatible ghost policies in effect", Err_N
);
504 Error_Msg_NE
("\& declared with ghost policy `Ignore`", Err_N
, Id
);
505 Error_Msg_NE
("\& used # with ghost policy `Check`", Err_N
, Id
);
507 end Check_Ghost_Policy
;
509 -- Start of processing for Check_Ghost_Context
512 -- Once it has been established that the reference to the Ghost entity
513 -- is within a suitable context, ensure that the policy at the point of
514 -- declaration and at the point of use match.
516 if Is_OK_Ghost_Context
(Ghost_Ref
) then
517 Check_Ghost_Policy
(Ghost_Id
, Ghost_Ref
);
519 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
520 -- its behavior or value.
524 ("ghost entity cannot appear in this context (SPARK RM 6.9(11))",
527 end Check_Ghost_Context
;
529 ----------------------------
530 -- Check_Ghost_Derivation --
531 ----------------------------
533 procedure Check_Ghost_Derivation
(Typ
: Entity_Id
) is
534 Parent_Typ
: constant Entity_Id
:= Etype
(Typ
);
536 Iface_Elmt
: Elmt_Id
;
539 -- Allow untagged derivations from predefined types such as Integer as
540 -- those are not Ghost by definition.
542 if Is_Scalar_Type
(Typ
) and then Parent_Typ
= Base_Type
(Typ
) then
545 -- The parent type of a Ghost type extension must be Ghost
547 elsif not Is_Ghost_Entity
(Parent_Typ
) then
548 Error_Msg_N
("type extension & cannot be ghost", Typ
);
549 Error_Msg_NE
("\parent type & is not ghost", Typ
, Parent_Typ
);
553 -- All progenitors (if any) must be Ghost as well
555 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
556 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
557 while Present
(Iface_Elmt
) loop
558 Iface
:= Node
(Iface_Elmt
);
560 if not Is_Ghost_Entity
(Iface
) then
561 Error_Msg_N
("type extension & cannot be ghost", Typ
);
562 Error_Msg_NE
("\interface type & is not ghost", Typ
, Iface
);
566 Next_Elmt
(Iface_Elmt
);
569 end Check_Ghost_Derivation
;
571 ----------------------------
572 -- Check_Ghost_Overriding --
573 ----------------------------
575 procedure Check_Ghost_Overriding
577 Overridden_Subp
: Entity_Id
)
579 Par_Subp
: Entity_Id
;
582 if Present
(Subp
) and then Present
(Overridden_Subp
) then
583 Par_Subp
:= Ultimate_Alias
(Overridden_Subp
);
585 -- The Ghost policy in effect at the point of declaration of a parent
586 -- and an overriding subprogram must match (SPARK RM 6.9(17)).
588 if Is_Checked_Ghost_Entity
(Par_Subp
)
589 and then Is_Ignored_Ghost_Entity
(Subp
)
591 Error_Msg_N
("incompatible ghost policies in effect", Subp
);
593 Error_Msg_Sloc
:= Sloc
(Par_Subp
);
594 Error_Msg_N
("\& declared # with ghost policy `Check`", Subp
);
596 Error_Msg_Sloc
:= Sloc
(Subp
);
597 Error_Msg_N
("\overridden # with ghost policy `Ignore`", Subp
);
599 elsif Is_Ignored_Ghost_Entity
(Par_Subp
)
600 and then Is_Checked_Ghost_Entity
(Subp
)
602 Error_Msg_N
("incompatible ghost policies in effect", Subp
);
604 Error_Msg_Sloc
:= Sloc
(Par_Subp
);
605 Error_Msg_N
("\& declared # with ghost policy `Ignore`", Subp
);
607 Error_Msg_Sloc
:= Sloc
(Subp
);
608 Error_Msg_N
("\overridden # with ghost policy `Check`", Subp
);
611 end Check_Ghost_Overriding
;
617 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
is
621 -- When the reference extracts a subcomponent, recover the related
622 -- object (SPARK RM 6.9(1)).
625 while Nkind_In
(Ref
, N_Explicit_Dereference
,
627 N_Selected_Component
,
633 if Is_Entity_Name
(Ref
) then
640 --------------------------------
641 -- Implements_Ghost_Interface --
642 --------------------------------
644 function Implements_Ghost_Interface
(Typ
: Entity_Id
) return Boolean is
645 Iface_Elmt
: Elmt_Id
;
648 -- Traverse the list of interfaces looking for a Ghost interface
650 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
651 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
652 while Present
(Iface_Elmt
) loop
653 if Is_Ghost_Entity
(Node
(Iface_Elmt
)) then
657 Next_Elmt
(Iface_Elmt
);
662 end Implements_Ghost_Interface
;
668 procedure Initialize
is
670 Ignored_Ghost_Units
.Init
;
673 ---------------------
674 -- Is_Ghost_Entity --
675 ---------------------
677 function Is_Ghost_Entity
(Id
: Entity_Id
) return Boolean is
679 return Is_Checked_Ghost_Entity
(Id
) or else Is_Ignored_Ghost_Entity
(Id
);
682 -------------------------
683 -- Is_Subject_To_Ghost --
684 -------------------------
686 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean is
687 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean;
688 -- Determine whether aspect or pragma argument Arg enables "ghostness"
690 -----------------------
691 -- Enables_Ghostness --
692 -----------------------
694 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean is
700 if Nkind
(Expr
) = N_Pragma_Argument_Association
then
701 Expr
:= Get_Pragma_Arg
(Expr
);
704 -- Determine whether the expression of the aspect is static and
707 if Present
(Expr
) then
708 Preanalyze_And_Resolve
(Expr
);
711 Is_OK_Static_Expression
(Expr
)
712 and then Is_True
(Expr_Value
(Expr
));
714 -- Otherwise Ghost defaults to True
719 end Enables_Ghostness
;
723 Id
: constant Entity_Id
:= Defining_Entity
(N
);
728 -- Start of processing for Is_Subject_To_Ghost
731 -- The related entity of the declaration has not been analyzed yet, do
732 -- not inspect its attributes.
734 if Ekind
(Id
) = E_Void
then
737 elsif Is_Ghost_Entity
(Id
) then
740 -- The completion of a type or a constant is not fully analyzed when the
741 -- reference to the Ghost entity is resolved. Because the completion is
742 -- not marked as Ghost yet, inspect the partial view.
744 elsif Is_Record_Type
(Id
)
745 or else Ekind
(Id
) = E_Constant
746 or else (Nkind
(N
) = N_Object_Declaration
747 and then Constant_Present
(N
))
749 Prev_Id
:= Incomplete_Or_Partial_View
(Id
);
751 if Present
(Prev_Id
) and then Is_Ghost_Entity
(Prev_Id
) then
756 -- Examine the aspect specifications (if any) looking for aspect Ghost
758 if Permits_Aspect_Specifications
(N
) then
759 Asp
:= First
(Aspect_Specifications
(N
));
760 while Present
(Asp
) loop
761 if Chars
(Identifier
(Asp
)) = Name_Ghost
then
762 return Enables_Ghostness
(Expression
(Asp
));
771 -- When the context is a [generic] package declaration, pragma Ghost
772 -- resides in the visible declarations.
774 if Nkind_In
(N
, N_Generic_Package_Declaration
,
775 N_Package_Declaration
)
777 Decl
:= First
(Visible_Declarations
(Specification
(N
)));
779 -- When the context is a package or a subprogram body, pragma Ghost
780 -- resides in the declarative part.
782 elsif Nkind_In
(N
, N_Package_Body
, N_Subprogram_Body
) then
783 Decl
:= First
(Declarations
(N
));
785 -- Otherwise pragma Ghost appears in the declarations following N
787 elsif Is_List_Member
(N
) then
791 while Present
(Decl
) loop
792 if Nkind
(Decl
) = N_Pragma
793 and then Pragma_Name
(Decl
) = Name_Ghost
796 Enables_Ghostness
(First
(Pragma_Argument_Associations
(Decl
)));
798 -- A source construct ends the region where pragma Ghost may appear,
799 -- stop the traversal.
801 elsif Comes_From_Source
(Decl
) then
809 end Is_Subject_To_Ghost
;
817 Ignored_Ghost_Units
.Locked
:= True;
818 Ignored_Ghost_Units
.Release
;
821 -----------------------------
822 -- Mark_Full_View_As_Ghost --
823 -----------------------------
825 procedure Mark_Full_View_As_Ghost
826 (Priv_Typ
: Entity_Id
;
827 Full_Typ
: Entity_Id
)
829 Full_Decl
: constant Node_Id
:= Declaration_Node
(Full_Typ
);
832 if Is_Checked_Ghost_Entity
(Priv_Typ
) then
833 Set_Is_Checked_Ghost_Entity
(Full_Typ
);
835 elsif Is_Ignored_Ghost_Entity
(Priv_Typ
) then
836 Set_Is_Ignored_Ghost_Entity
(Full_Typ
);
837 Set_Is_Ignored_Ghost_Node
(Full_Decl
);
838 Propagate_Ignored_Ghost_Code
(Full_Decl
);
840 end Mark_Full_View_As_Ghost
;
842 --------------------------
843 -- Mark_Pragma_As_Ghost --
844 --------------------------
846 procedure Mark_Pragma_As_Ghost
848 Context_Id
: Entity_Id
)
851 if Is_Checked_Ghost_Entity
(Context_Id
) then
852 Set_Is_Ghost_Pragma
(Prag
);
854 elsif Is_Ignored_Ghost_Entity
(Context_Id
) then
855 Set_Is_Ghost_Pragma
(Prag
);
856 Set_Is_Ignored_Ghost_Node
(Prag
);
857 Propagate_Ignored_Ghost_Code
(Prag
);
859 end Mark_Pragma_As_Ghost
;
861 ----------------------------
862 -- Mark_Renaming_As_Ghost --
863 ----------------------------
865 procedure Mark_Renaming_As_Ghost
869 Ren_Id
: constant Entity_Id
:= Defining_Entity
(Ren_Decl
);
872 if Is_Checked_Ghost_Entity
(Nam_Id
) then
873 Set_Is_Checked_Ghost_Entity
(Ren_Id
);
875 elsif Is_Ignored_Ghost_Entity
(Nam_Id
) then
876 Set_Is_Ignored_Ghost_Entity
(Ren_Id
);
877 Set_Is_Ignored_Ghost_Node
(Ren_Decl
);
878 Propagate_Ignored_Ghost_Code
(Ren_Decl
);
880 end Mark_Renaming_As_Ghost
;
882 ----------------------------------
883 -- Propagate_Ignored_Ghost_Code --
884 ----------------------------------
886 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
) is
891 -- Traverse the parent chain looking for blocks, packages and
892 -- subprograms or their respective bodies.
895 while Present
(Nod
) loop
898 if Nkind
(Nod
) = N_Block_Statement
then
899 Scop
:= Entity
(Identifier
(Nod
));
901 elsif Nkind_In
(Nod
, N_Package_Body
,
902 N_Package_Declaration
,
904 N_Subprogram_Declaration
)
906 Scop
:= Defining_Entity
(Nod
);
909 -- The current node denotes a scoping construct
911 if Present
(Scop
) then
913 -- Stop the traversal when the scope already contains ignored
914 -- Ghost code as all enclosing scopes have already been marked.
916 if Contains_Ignored_Ghost_Code
(Scop
) then
919 -- Otherwise mark this scope and keep climbing
922 Set_Contains_Ignored_Ghost_Code
(Scop
);
929 -- The unit containing the ignored Ghost code must be post processed
930 -- before invoking the back end.
932 Add_Ignored_Ghost_Unit
(Cunit
(Get_Code_Unit
(N
)));
933 end Propagate_Ignored_Ghost_Code
;
935 -------------------------------
936 -- Remove_Ignored_Ghost_Code --
937 -------------------------------
939 procedure Remove_Ignored_Ghost_Code
is
940 procedure Prune_Tree
(Root
: Node_Id
);
941 -- Remove all code marked as ignored Ghost from the tree of denoted by
948 procedure Prune_Tree
(Root
: Node_Id
) is
949 procedure Prune
(N
: Node_Id
);
950 -- Remove a given node from the tree by rewriting it into null
952 function Prune_Node
(N
: Node_Id
) return Traverse_Result
;
953 -- Determine whether node N denotes an ignored Ghost construct. If
954 -- this is the case, rewrite N as a null statement. See the body for
961 procedure Prune
(N
: Node_Id
) is
963 -- Destroy any aspects that may be associated with the node
965 if Permits_Aspect_Specifications
(N
) and then Has_Aspects
(N
) then
969 Rewrite
(N
, Make_Null_Statement
(Sloc
(N
)));
976 function Prune_Node
(N
: Node_Id
) return Traverse_Result
is
980 -- The node is either declared as ignored Ghost or is a byproduct
981 -- of expansion. Destroy it and stop the traversal on this branch.
983 if Is_Ignored_Ghost_Node
(N
) then
987 -- Scoping constructs such as blocks, packages, subprograms and
988 -- bodies offer some flexibility with respect to pruning.
990 elsif Nkind_In
(N
, N_Block_Statement
,
992 N_Package_Declaration
,
994 N_Subprogram_Declaration
)
996 if Nkind
(N
) = N_Block_Statement
then
997 Id
:= Entity
(Identifier
(N
));
999 Id
:= Defining_Entity
(N
);
1002 -- The scoping construct contains both living and ignored Ghost
1003 -- code, let the traversal prune all relevant nodes.
1005 if Contains_Ignored_Ghost_Code
(Id
) then
1008 -- Otherwise the construct contains only living code and should
1015 -- Otherwise keep searching for ignored Ghost nodes
1022 procedure Prune_Nodes
is new Traverse_Proc
(Prune_Node
);
1024 -- Start of processing for Prune_Tree
1030 -- Start of processing for Remove_Ignored_Ghost_Code
1033 for Index
in Ignored_Ghost_Units
.First
.. Ignored_Ghost_Units
.Last
loop
1034 Prune_Tree
(Unit
(Ignored_Ghost_Units
.Table
(Index
)));
1036 end Remove_Ignored_Ghost_Code
;
1038 --------------------
1039 -- Set_Ghost_Mode --
1040 --------------------
1042 procedure Set_Ghost_Mode
(N
: Node_Id
; Id
: Entity_Id
:= Empty
) is
1043 procedure Set_From_Entity
(Ent_Id
: Entity_Id
);
1044 -- Set the value of global variable Ghost_Mode depending on the mode of
1047 procedure Set_From_Policy
;
1048 -- Set the value of global variable Ghost_Mode depending on the current
1049 -- Ghost policy in effect.
1051 ---------------------
1052 -- Set_From_Entity --
1053 ---------------------
1055 procedure Set_From_Entity
(Ent_Id
: Entity_Id
) is
1057 Set_Ghost_Mode_From_Entity
(Ent_Id
);
1059 if Is_Ignored_Ghost_Entity
(Ent_Id
) then
1060 Set_Is_Ignored_Ghost_Node
(N
);
1061 Propagate_Ignored_Ghost_Code
(N
);
1063 end Set_From_Entity
;
1065 ---------------------
1066 -- Set_From_Policy --
1067 ---------------------
1069 procedure Set_From_Policy
is
1070 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
1073 if Policy
= Name_Check
then
1074 Ghost_Mode
:= Check
;
1076 elsif Policy
= Name_Ignore
then
1077 Ghost_Mode
:= Ignore
;
1079 Set_Is_Ignored_Ghost_Node
(N
);
1080 Propagate_Ignored_Ghost_Code
(N
);
1082 end Set_From_Policy
;
1088 -- Start of processing for Set_Ghost_Mode
1091 -- The input node denotes one of the many declaration kinds that may be
1092 -- subject to pragma Ghost.
1094 if Is_Declaration
(N
) then
1095 if Is_Subject_To_Ghost
(N
) then
1098 -- The declaration denotes the completion of a deferred constant,
1099 -- pragma Ghost appears on the partial declaration.
1101 elsif Nkind
(N
) = N_Object_Declaration
1102 and then Constant_Present
(N
)
1103 and then Present
(Id
)
1105 Set_From_Entity
(Id
);
1107 -- The declaration denotes the full view of a private type, pragma
1108 -- Ghost appears on the partial declaration.
1110 elsif Nkind
(N
) = N_Full_Type_Declaration
1111 and then Is_Private_Type
(Defining_Entity
(N
))
1112 and then Present
(Id
)
1114 Set_From_Entity
(Id
);
1117 -- The input denotes an assignment or a procedure call. In this case
1118 -- the Ghost mode is dictated by the name of the construct.
1120 elsif Nkind_In
(N
, N_Assignment_Statement
,
1121 N_Procedure_Call_Statement
)
1123 Nam_Id
:= Ghost_Entity
(Name
(N
));
1125 if Present
(Nam_Id
) then
1126 Set_From_Entity
(Nam_Id
);
1129 -- The input denotes a package or subprogram body
1131 elsif Nkind_In
(N
, N_Package_Body
, N_Subprogram_Body
) then
1132 if (Present
(Id
) and then Is_Ghost_Entity
(Id
))
1133 or else Is_Subject_To_Ghost
(N
)
1138 -- The input denotes a pragma
1140 elsif Nkind
(N
) = N_Pragma
and then Is_Ghost_Pragma
(N
) then
1141 if Is_Ignored_Ghost_Node
(N
) then
1142 Ghost_Mode
:= Ignore
;
1144 Ghost_Mode
:= Check
;
1147 -- The input denotes a freeze node
1149 elsif Nkind
(N
) = N_Freeze_Entity
and then Present
(Id
) then
1150 Set_From_Entity
(Id
);
1154 --------------------------------
1155 -- Set_Ghost_Mode_From_Entity --
1156 --------------------------------
1158 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
) is
1160 if Is_Checked_Ghost_Entity
(Id
) then
1161 Ghost_Mode
:= Check
;
1162 elsif Is_Ignored_Ghost_Entity
(Id
) then
1163 Ghost_Mode
:= Ignore
;
1165 end Set_Ghost_Mode_From_Entity
;
1167 -------------------------
1168 -- Set_Is_Ghost_Entity --
1169 -------------------------
1171 procedure Set_Is_Ghost_Entity
(Id
: Entity_Id
) is
1172 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
1174 if Policy
= Name_Check
then
1175 Set_Is_Checked_Ghost_Entity
(Id
);
1176 elsif Policy
= Name_Ignore
then
1177 Set_Is_Ignored_Ghost_Entity
(Id
);
1179 end Set_Is_Ghost_Entity
;