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
;
53 -- The following table contains the N_Compilation_Unit node for a unit that
54 -- is either subject to pragma Ghost with policy Ignore or contains ignored
55 -- Ghost code. The table is used in the removal of ignored Ghost code from
58 package Ignored_Ghost_Units
is new Table
.Table
(
59 Table_Component_Type
=> Node_Id
,
60 Table_Index_Type
=> Int
,
62 Table_Initial
=> Alloc
.Ignored_Ghost_Units_Initial
,
63 Table_Increment
=> Alloc
.Ignored_Ghost_Units_Increment
,
64 Table_Name
=> "Ignored_Ghost_Units");
66 -----------------------
67 -- Local subprograms --
68 -----------------------
70 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
;
71 -- Find the entity of a reference to a Ghost entity. Return Empty if there
74 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
);
75 pragma Inline
(Install_Ghost_Mode
);
76 -- Install Ghost mode Mode as the Ghost mode in effect
78 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
);
79 pragma Inline
(Install_Ghost_Region
);
80 -- Install a Ghost region comprised of mode Mode and ignored region start
83 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean;
84 -- Determine whether declaration or body N is subject to aspect or pragma
85 -- Ghost. This routine must be used in cases where pragma Ghost has not
86 -- been analyzed yet, but the context needs to establish the "ghostness"
89 procedure Mark_Ghost_Declaration_Or_Body
92 -- Mark the defining entity of declaration or body N as Ghost depending on
93 -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
96 function Name_To_Ghost_Mode
(Mode
: Name_Id
) return Ghost_Mode_Type
;
97 pragma Inline
(Name_To_Ghost_Mode
);
98 -- Convert a Ghost mode denoted by name Mode into its respective enumerated
101 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
);
102 -- Signal all enclosing scopes that they now contain at least one ignored
103 -- Ghost node denoted by N. Add the compilation unit containing N to table
104 -- Ignored_Ghost_Units for post processing.
106 ----------------------------
107 -- Add_Ignored_Ghost_Unit --
108 ----------------------------
110 procedure Add_Ignored_Ghost_Unit
(Unit
: Node_Id
) is
112 pragma Assert
(Nkind
(Unit
) = N_Compilation_Unit
);
114 -- Avoid duplicates in the table as pruning the same unit more than once
115 -- is wasteful. Since ignored Ghost code tends to be grouped up, check
116 -- the contents of the table in reverse.
118 for Index
in reverse Ignored_Ghost_Units
.First
..
119 Ignored_Ghost_Units
.Last
121 -- If the unit is already present in the table, do not add it again
123 if Unit
= Ignored_Ghost_Units
.Table
(Index
) then
128 -- If we get here, then this is the first time the unit is being added
130 Ignored_Ghost_Units
.Append
(Unit
);
131 end Add_Ignored_Ghost_Unit
;
133 ----------------------------
134 -- Check_Ghost_Completion --
135 ----------------------------
137 procedure Check_Ghost_Completion
138 (Prev_Id
: Entity_Id
;
139 Compl_Id
: Entity_Id
)
141 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
144 -- Nothing to do if one of the views is missing
146 if No
(Prev_Id
) or else No
(Compl_Id
) then
149 -- The Ghost policy in effect at the point of declaration and at the
150 -- point of completion must match (SPARK RM 6.9(14)).
152 elsif Is_Checked_Ghost_Entity
(Prev_Id
)
153 and then Policy
= Name_Ignore
155 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
157 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
158 Error_Msg_N
("\& declared with ghost policy `Check`", Prev_Id
);
159 Error_Msg_N
("\& completed # with ghost policy `Ignore`", Prev_Id
);
161 elsif Is_Ignored_Ghost_Entity
(Prev_Id
)
162 and then Policy
= Name_Check
164 Error_Msg_Sloc
:= Sloc
(Compl_Id
);
166 Error_Msg_N
("incompatible ghost policies in effect", Prev_Id
);
167 Error_Msg_N
("\& declared with ghost policy `Ignore`", Prev_Id
);
168 Error_Msg_N
("\& completed # with ghost policy `Check`", Prev_Id
);
170 end Check_Ghost_Completion
;
172 -------------------------
173 -- Check_Ghost_Context --
174 -------------------------
176 procedure Check_Ghost_Context
(Ghost_Id
: Entity_Id
; Ghost_Ref
: Node_Id
) is
177 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
);
178 -- Verify that the Ghost policy at the point of declaration of entity Id
179 -- matches the policy at the point of reference Ref. If this is not the
180 -- case emit an error at Ref.
182 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean;
183 -- Determine whether node Context denotes a Ghost-friendly context where
184 -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
186 -------------------------
187 -- Is_OK_Ghost_Context --
188 -------------------------
190 function Is_OK_Ghost_Context
(Context
: Node_Id
) return Boolean is
191 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean;
192 -- Determine whether node Decl is a suitable context for a reference
193 -- to a Ghost entity. To qualify as such, Decl must either
195 -- * Define a Ghost entity
197 -- * Be subject to pragma Ghost
199 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean;
200 -- Determine whether node Prag is a suitable context for a reference
201 -- to a Ghost entity. To qualify as such, Prag must either
203 -- * Be an assertion expression pragma
205 -- * Denote pragma Global, Depends, Initializes, Refined_Global,
206 -- Refined_Depends or Refined_State.
208 -- * Specify an aspect of a Ghost entity
210 -- * Contain a reference to a Ghost entity
212 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean;
213 -- Determine whether node Stmt is a suitable context for a reference
214 -- to a Ghost entity. To qualify as such, Stmt must either
216 -- * Denote a procedure call to a Ghost procedure
218 -- * Denote an assignment statement whose target is Ghost
220 -----------------------
221 -- Is_OK_Declaration --
222 -----------------------
224 function Is_OK_Declaration
(Decl
: Node_Id
) return Boolean is
225 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean;
226 -- Determine whether node N appears in the profile of a subprogram
229 --------------------------------
230 -- In_Subprogram_Body_Profile --
231 --------------------------------
233 function In_Subprogram_Body_Profile
(N
: Node_Id
) return Boolean is
234 Spec
: constant Node_Id
:= Parent
(N
);
237 -- The node appears in a parameter specification in which case
238 -- it is either the parameter type or the default expression or
239 -- the node appears as the result definition of a function.
242 (Nkind
(N
) = N_Parameter_Specification
244 (Nkind
(Spec
) = N_Function_Specification
245 and then N
= Result_Definition
(Spec
)))
246 and then Nkind
(Parent
(Spec
)) = N_Subprogram_Body
;
247 end In_Subprogram_Body_Profile
;
254 -- Start of processing for Is_OK_Declaration
257 if Is_Ghost_Declaration
(Decl
) then
262 -- A reference to a Ghost entity may appear within the profile of
263 -- a subprogram body. This context is treated as suitable because
264 -- it duplicates the context of the corresponding spec. The real
265 -- check was already performed during the analysis of the spec.
267 elsif In_Subprogram_Body_Profile
(Decl
) then
270 -- A reference to a Ghost entity may appear within an expression
271 -- function which is still being analyzed. This context is treated
272 -- as suitable because it is not yet known whether the expression
273 -- function is an initial declaration or a completion. The real
274 -- check is performed when the expression function is expanded.
276 elsif Nkind
(Decl
) = N_Expression_Function
277 and then not Analyzed
(Decl
)
281 -- References to Ghost entities may be relocated in internally
284 elsif Nkind
(Decl
) = N_Subprogram_Body
285 and then not Comes_From_Source
(Decl
)
287 Subp_Id
:= Corresponding_Spec
(Decl
);
289 if Present
(Subp_Id
) then
291 -- The context is the internally built _Postconditions
292 -- procedure, which is OK because the real check was done
293 -- before expansion activities.
295 if Chars
(Subp_Id
) = Name_uPostconditions
then
298 -- The context is the internally built predicate function,
299 -- which is OK because the real check was done before the
300 -- predicate function was generated.
302 elsif Is_Predicate_Function
(Subp_Id
) then
307 Original_Node
(Unit_Declaration_Node
(Subp_Id
));
309 -- The original context is an expression function that
310 -- has been split into a spec and a body. The context is
311 -- OK as long as the initial declaration is Ghost.
313 if Nkind
(Subp_Decl
) = N_Expression_Function
then
314 return Is_Ghost_Declaration
(Subp_Decl
);
318 -- Otherwise this is either an internal body or an internal
319 -- completion. Both are OK because the real check was done
320 -- before expansion activities.
328 end Is_OK_Declaration
;
334 function Is_OK_Pragma
(Prag
: Node_Id
) return Boolean is
335 procedure Check_Policies
(Prag_Nam
: Name_Id
);
336 -- Verify that the Ghost policy in effect is the same as the
337 -- assertion policy for pragma name Prag_Nam. Emit an error if
338 -- this is not the case.
344 procedure Check_Policies
(Prag_Nam
: Name_Id
) is
345 AP
: constant Name_Id
:= Check_Kind
(Prag_Nam
);
346 GP
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
349 -- If the Ghost policy in effect at the point of a Ghost entity
350 -- reference is Ignore, then the assertion policy of the pragma
351 -- must be Ignore (SPARK RM 6.9(18)).
353 if GP
= Name_Ignore
and then AP
/= Name_Ignore
then
355 ("incompatible ghost policies in effect",
358 ("\ghost entity & has policy `Ignore`",
359 Ghost_Ref
, Ghost_Id
);
361 Error_Msg_Name_1
:= AP
;
363 ("\assertion expression has policy %", Ghost_Ref
);
372 -- Start of processing for Is_OK_Pragma
375 if Nkind
(Prag
) = N_Pragma
then
376 Prag_Id
:= Get_Pragma_Id
(Prag
);
377 Prag_Nam
:= Original_Aspect_Pragma_Name
(Prag
);
379 -- A pragma that applies to a Ghost construct or specifies an
380 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
382 if Is_Ghost_Pragma
(Prag
) then
385 -- An assertion expression pragma is Ghost when it contains a
386 -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
387 -- predicate pragmas (SPARK RM 6.9(11)).
389 elsif Assertion_Expression_Pragma
(Prag_Id
)
390 and then Prag_Id
/= Pragma_Predicate
392 -- Ensure that the assertion policy and the Ghost policy are
393 -- compatible (SPARK RM 6.9(18)).
395 Check_Policies
(Prag_Nam
);
398 -- Several pragmas that may apply to a non-Ghost entity are
399 -- treated as Ghost when they contain a reference to a Ghost
400 -- entity (SPARK RM 6.9(11)).
402 elsif Nam_In
(Prag_Nam
, Name_Global
,
406 Name_Refined_Depends
,
416 ---------------------
417 -- Is_OK_Statement --
418 ---------------------
420 function Is_OK_Statement
(Stmt
: Node_Id
) return Boolean is
422 -- An assignment statement is Ghost when the target is a Ghost
425 if Nkind
(Stmt
) = N_Assignment_Statement
then
426 return Is_Ghost_Assignment
(Stmt
);
428 -- A procedure call is Ghost when it calls a Ghost procedure
430 elsif Nkind
(Stmt
) = N_Procedure_Call_Statement
then
431 return Is_Ghost_Procedure_Call
(Stmt
);
435 -- An if statement is a suitable context for a Ghost entity if it
436 -- is the byproduct of assertion expression expansion. Note that
437 -- the assertion expression may not be related to a Ghost entity,
438 -- but it may still contain references to Ghost entities.
440 elsif Nkind
(Stmt
) = N_If_Statement
441 and then Nkind
(Original_Node
(Stmt
)) = N_Pragma
442 and then Assertion_Expression_Pragma
443 (Get_Pragma_Id
(Original_Node
(Stmt
)))
455 -- Start of processing for Is_OK_Ghost_Context
458 -- The context is Ghost when it appears within a Ghost package or
461 if Ghost_Mode
> None
then
464 -- A Ghost type may be referenced in a use_type clause
465 -- (SPARK RM 6.9.10).
467 elsif Present
(Parent
(Context
))
468 and then Nkind
(Parent
(Context
)) = N_Use_Type_Clause
472 -- Routine Expand_Record_Extension creates a parent subtype without
473 -- inserting it into the tree. There is no good way of recognizing
474 -- this special case as there is no parent. Try to approximate the
477 elsif No
(Parent
(Context
)) and then Is_Tagged_Type
(Ghost_Id
) then
480 -- Otherwise climb the parent chain looking for a suitable Ghost
485 while Present
(Par
) loop
486 if Is_Ignored_Ghost_Node
(Par
) then
489 -- A reference to a Ghost entity can appear within an aspect
490 -- specification (SPARK RM 6.9(10)). The precise checking will
491 -- occur when analyzing the corresponding pragma. We make an
492 -- exception for predicate aspects that only allow referencing
493 -- a Ghost entity when the corresponding type declaration is
494 -- Ghost (SPARK RM 6.9(11)).
496 elsif Nkind
(Par
) = N_Aspect_Specification
497 and then not Same_Aspect
498 (Get_Aspect_Id
(Par
), Aspect_Predicate
)
502 elsif Is_OK_Declaration
(Par
) then
505 elsif Is_OK_Pragma
(Par
) then
508 elsif Is_OK_Statement
(Par
) then
511 -- Prevent the search from going too far
513 elsif Is_Body_Or_Package_Declaration
(Par
) then
520 -- The expansion of assertion expression pragmas and attribute Old
521 -- may cause a legal Ghost entity reference to become illegal due
522 -- to node relocation. Check the In_Assertion_Expr counter as last
523 -- resort to try and infer the original legal context.
525 if In_Assertion_Expr
> 0 then
528 -- Otherwise the context is not suitable for a reference to a
535 end Is_OK_Ghost_Context
;
537 ------------------------
538 -- Check_Ghost_Policy --
539 ------------------------
541 procedure Check_Ghost_Policy
(Id
: Entity_Id
; Ref
: Node_Id
) is
542 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
545 -- The Ghost policy in effect a the point of declaration and at the
546 -- point of use must match (SPARK RM 6.9(13)).
548 if Is_Checked_Ghost_Entity
(Id
)
549 and then Policy
= Name_Ignore
550 and then May_Be_Lvalue
(Ref
)
552 Error_Msg_Sloc
:= Sloc
(Ref
);
554 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
555 Error_Msg_NE
("\& declared with ghost policy `Check`", Ref
, Id
);
556 Error_Msg_NE
("\& used # with ghost policy `Ignore`", Ref
, Id
);
558 elsif Is_Ignored_Ghost_Entity
(Id
) and then Policy
= Name_Check
then
559 Error_Msg_Sloc
:= Sloc
(Ref
);
561 Error_Msg_N
("incompatible ghost policies in effect", Ref
);
562 Error_Msg_NE
("\& declared with ghost policy `Ignore`", Ref
, Id
);
563 Error_Msg_NE
("\& used # with ghost policy `Check`", Ref
, Id
);
565 end Check_Ghost_Policy
;
567 -- Start of processing for Check_Ghost_Context
570 -- Once it has been established that the reference to the Ghost entity
571 -- is within a suitable context, ensure that the policy at the point of
572 -- declaration and at the point of use match.
574 if Is_OK_Ghost_Context
(Ghost_Ref
) then
575 Check_Ghost_Policy
(Ghost_Id
, Ghost_Ref
);
577 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
578 -- its behavior or value (SPARK RM 6.9(10,11)).
581 Error_Msg_N
("ghost entity cannot appear in this context", Ghost_Ref
);
583 end Check_Ghost_Context
;
585 ----------------------------
586 -- Check_Ghost_Overriding --
587 ----------------------------
589 procedure Check_Ghost_Overriding
591 Overridden_Subp
: Entity_Id
)
593 Deriv_Typ
: Entity_Id
;
594 Over_Subp
: Entity_Id
;
597 if Present
(Subp
) and then Present
(Overridden_Subp
) then
598 Over_Subp
:= Ultimate_Alias
(Overridden_Subp
);
599 Deriv_Typ
:= Find_Dispatching_Type
(Subp
);
601 -- A Ghost primitive of a non-Ghost type extension cannot override an
602 -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
604 if Is_Ghost_Entity
(Subp
)
605 and then Present
(Deriv_Typ
)
606 and then not Is_Ghost_Entity
(Deriv_Typ
)
607 and then not Is_Ghost_Entity
(Over_Subp
)
608 and then not Is_Abstract_Subprogram
(Over_Subp
)
610 Error_Msg_N
("incompatible overriding in effect", Subp
);
612 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
613 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
615 Error_Msg_Sloc
:= Sloc
(Subp
);
616 Error_Msg_N
("\overridden # with ghost subprogram", Subp
);
619 -- A non-Ghost primitive of a type extension cannot override an
620 -- inherited Ghost primitive (SPARK RM 6.9(8)).
622 if Is_Ghost_Entity
(Over_Subp
)
623 and then not Is_Ghost_Entity
(Subp
)
624 and then not Is_Abstract_Subprogram
(Subp
)
626 Error_Msg_N
("incompatible overriding in effect", Subp
);
628 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
629 Error_Msg_N
("\& declared # as ghost subprogram", Subp
);
631 Error_Msg_Sloc
:= Sloc
(Subp
);
632 Error_Msg_N
("\overridden # with non-ghost subprogram", Subp
);
635 if Present
(Deriv_Typ
)
636 and then not Is_Ignored_Ghost_Entity
(Deriv_Typ
)
638 -- When a tagged type is either non-Ghost or checked Ghost and
639 -- one of its primitives overrides an inherited operation, the
640 -- overridden operation of the ancestor type must be ignored Ghost
641 -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
643 if Is_Ignored_Ghost_Entity
(Subp
) then
645 -- Both the parent subprogram and overriding subprogram are
648 if Is_Ignored_Ghost_Entity
(Over_Subp
) then
651 -- The parent subprogram carries policy Check
653 elsif Is_Checked_Ghost_Entity
(Over_Subp
) then
655 ("incompatible ghost policies in effect", Subp
);
657 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
659 ("\& declared # with ghost policy `Check`", Subp
);
661 Error_Msg_Sloc
:= Sloc
(Subp
);
663 ("\overridden # with ghost policy `Ignore`", Subp
);
665 -- The parent subprogram is non-Ghost
669 ("incompatible ghost policies in effect", Subp
);
671 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
672 Error_Msg_N
("\& declared # as non-ghost subprogram", Subp
);
674 Error_Msg_Sloc
:= Sloc
(Subp
);
676 ("\overridden # with ghost policy `Ignore`", Subp
);
679 -- When a tagged type is either non-Ghost or checked Ghost and
680 -- one of its primitives overrides an inherited operation, the
681 -- the primitive of the tagged type must be ignored Ghost if the
682 -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
684 elsif Is_Ignored_Ghost_Entity
(Over_Subp
) then
686 -- Both the parent subprogram and the overriding subprogram are
689 if Is_Ignored_Ghost_Entity
(Subp
) then
692 -- The overriding subprogram carries policy Check
694 elsif Is_Checked_Ghost_Entity
(Subp
) then
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 Ghost policy `Check`", Subp
);
706 -- The overriding subprogram is non-Ghost
710 ("incompatible ghost policies in effect", Subp
);
712 Error_Msg_Sloc
:= Sloc
(Over_Subp
);
714 ("\& declared # with ghost policy `Ignore`", Subp
);
716 Error_Msg_Sloc
:= Sloc
(Subp
);
718 ("\overridden # with non-ghost subprogram", Subp
);
723 end Check_Ghost_Overriding
;
725 ---------------------------
726 -- Check_Ghost_Primitive --
727 ---------------------------
729 procedure Check_Ghost_Primitive
(Prim
: Entity_Id
; Typ
: Entity_Id
) is
731 -- The Ghost policy in effect at the point of declaration of a primitive
732 -- operation and a tagged type must match (SPARK RM 6.9(16)).
734 if Is_Tagged_Type
(Typ
) then
735 if Is_Checked_Ghost_Entity
(Prim
)
736 and then Is_Ignored_Ghost_Entity
(Typ
)
738 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
740 Error_Msg_Sloc
:= Sloc
(Typ
);
742 ("\tagged type & declared # with ghost policy `Ignore`",
745 Error_Msg_Sloc
:= Sloc
(Prim
);
747 ("\primitive subprogram & declared # with ghost policy `Check`",
750 elsif Is_Ignored_Ghost_Entity
(Prim
)
751 and then Is_Checked_Ghost_Entity
(Typ
)
753 Error_Msg_N
("incompatible ghost policies in effect", Prim
);
755 Error_Msg_Sloc
:= Sloc
(Typ
);
757 ("\tagged type & declared # with ghost policy `Check`",
760 Error_Msg_Sloc
:= Sloc
(Prim
);
762 ("\primitive subprogram & declared # with ghost policy `Ignore`",
766 end Check_Ghost_Primitive
;
768 ----------------------------
769 -- Check_Ghost_Refinement --
770 ----------------------------
772 procedure Check_Ghost_Refinement
774 State_Id
: Entity_Id
;
776 Constit_Id
: Entity_Id
)
779 if Is_Ghost_Entity
(State_Id
) then
780 if Is_Ghost_Entity
(Constit_Id
) then
782 -- The Ghost policy in effect at the point of abstract state
783 -- declaration and constituent must match (SPARK RM 6.9(15)).
785 if Is_Checked_Ghost_Entity
(State_Id
)
786 and then Is_Ignored_Ghost_Entity
(Constit_Id
)
788 Error_Msg_Sloc
:= Sloc
(Constit
);
789 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
792 ("\abstract state & declared with ghost policy `Check`",
795 ("\constituent & declared # with ghost policy `Ignore`",
798 elsif Is_Ignored_Ghost_Entity
(State_Id
)
799 and then Is_Checked_Ghost_Entity
(Constit_Id
)
801 Error_Msg_Sloc
:= Sloc
(Constit
);
802 SPARK_Msg_N
("incompatible ghost policies in effect", State
);
805 ("\abstract state & declared with ghost policy `Ignore`",
808 ("\constituent & declared # with ghost policy `Check`",
812 -- A constituent of a Ghost abstract state must be a Ghost entity
813 -- (SPARK RM 7.2.2(12)).
817 ("constituent of ghost state & must be ghost",
821 end Check_Ghost_Refinement
;
823 ----------------------
824 -- Check_Ghost_Type --
825 ----------------------
827 procedure Check_Ghost_Type
(Typ
: Entity_Id
) is
828 Conc_Typ
: Entity_Id
;
829 Full_Typ
: Entity_Id
;
832 if Is_Ghost_Entity
(Typ
) then
836 if Is_Single_Concurrent_Type
(Typ
) then
837 Conc_Typ
:= Anonymous_Object
(Typ
);
838 Full_Typ
:= Conc_Typ
;
840 elsif Is_Concurrent_Type
(Typ
) then
844 -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
845 -- legality rule first to give a finer-grained diagnostic.
847 if Present
(Conc_Typ
) then
848 Error_Msg_N
("ghost type & cannot be concurrent", Conc_Typ
);
851 -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
853 if Is_Effectively_Volatile
(Full_Typ
) then
854 Error_Msg_N
("ghost type & cannot be volatile", Full_Typ
);
857 end Check_Ghost_Type
;
863 function Ghost_Entity
(N
: Node_Id
) return Entity_Id
is
867 -- When the reference denotes a subcomponent, recover the related
868 -- object (SPARK RM 6.9(1)).
871 while Nkind_In
(Ref
, N_Explicit_Dereference
,
873 N_Selected_Component
,
879 if Is_Entity_Name
(Ref
) then
886 --------------------------------
887 -- Implements_Ghost_Interface --
888 --------------------------------
890 function Implements_Ghost_Interface
(Typ
: Entity_Id
) return Boolean is
891 Iface_Elmt
: Elmt_Id
;
894 -- Traverse the list of interfaces looking for a Ghost interface
896 if Is_Tagged_Type
(Typ
) and then Present
(Interfaces
(Typ
)) then
897 Iface_Elmt
:= First_Elmt
(Interfaces
(Typ
));
898 while Present
(Iface_Elmt
) loop
899 if Is_Ghost_Entity
(Node
(Iface_Elmt
)) then
903 Next_Elmt
(Iface_Elmt
);
908 end Implements_Ghost_Interface
;
914 procedure Initialize
is
916 Ignored_Ghost_Units
.Init
;
919 ------------------------
920 -- Install_Ghost_Mode --
921 ------------------------
923 procedure Install_Ghost_Mode
(Mode
: Ghost_Mode_Type
) is
925 Install_Ghost_Region
(Mode
, Empty
);
926 end Install_Ghost_Mode
;
928 --------------------------
929 -- Install_Ghost_Region --
930 --------------------------
932 procedure Install_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
934 -- The context is already within an ignored Ghost region. Maintain the
935 -- start of the outermost ignored Ghost region.
937 if Present
(Ignored_Ghost_Region
) then
940 -- The current region is the outermost ignored Ghost region. Save its
943 elsif Present
(N
) and then Mode
= Ignore
then
944 Ignored_Ghost_Region
:= N
;
946 -- Otherwise the current region is not ignored, nothing to save
949 Ignored_Ghost_Region
:= Empty
;
953 end Install_Ghost_Region
;
955 procedure Install_Ghost_Region
(Mode
: Name_Id
; N
: Node_Id
) is
957 Install_Ghost_Region
(Name_To_Ghost_Mode
(Mode
), N
);
958 end Install_Ghost_Region
;
960 -------------------------
961 -- Is_Ghost_Assignment --
962 -------------------------
964 function Is_Ghost_Assignment
(N
: Node_Id
) return Boolean is
968 -- An assignment statement is Ghost when its target denotes a Ghost
971 if Nkind
(N
) = N_Assignment_Statement
then
972 Id
:= Ghost_Entity
(Name
(N
));
974 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
978 end Is_Ghost_Assignment
;
980 --------------------------
981 -- Is_Ghost_Declaration --
982 --------------------------
984 function Is_Ghost_Declaration
(N
: Node_Id
) return Boolean is
988 -- A declaration is Ghost when it elaborates a Ghost entity or is
989 -- subject to pragma Ghost.
991 if Is_Declaration
(N
) then
992 Id
:= Defining_Entity
(N
);
994 return Is_Ghost_Entity
(Id
) or else Is_Subject_To_Ghost
(N
);
998 end Is_Ghost_Declaration
;
1000 ---------------------
1001 -- Is_Ghost_Pragma --
1002 ---------------------
1004 function Is_Ghost_Pragma
(N
: Node_Id
) return Boolean is
1006 return Is_Checked_Ghost_Pragma
(N
) or else Is_Ignored_Ghost_Pragma
(N
);
1007 end Is_Ghost_Pragma
;
1009 -----------------------------
1010 -- Is_Ghost_Procedure_Call --
1011 -----------------------------
1013 function Is_Ghost_Procedure_Call
(N
: Node_Id
) return Boolean is
1017 -- A procedure call is Ghost when it invokes a Ghost procedure
1019 if Nkind
(N
) = N_Procedure_Call_Statement
then
1020 Id
:= Ghost_Entity
(Name
(N
));
1022 return Present
(Id
) and then Is_Ghost_Entity
(Id
);
1026 end Is_Ghost_Procedure_Call
;
1028 ---------------------------
1029 -- Is_Ignored_Ghost_Unit --
1030 ---------------------------
1032 function Is_Ignored_Ghost_Unit
(N
: Node_Id
) return Boolean is
1034 -- Inspect the original node of the unit in case removal of ignored
1035 -- Ghost code has already taken place.
1038 Nkind
(N
) = N_Compilation_Unit
1039 and then Is_Ignored_Ghost_Entity
1040 (Defining_Entity
(Original_Node
(Unit
(N
))));
1041 end Is_Ignored_Ghost_Unit
;
1043 -------------------------
1044 -- Is_Subject_To_Ghost --
1045 -------------------------
1047 function Is_Subject_To_Ghost
(N
: Node_Id
) return Boolean is
1048 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean;
1049 -- Determine whether aspect or pragma argument Arg enables "ghostness"
1051 -----------------------
1052 -- Enables_Ghostness --
1053 -----------------------
1055 function Enables_Ghostness
(Arg
: Node_Id
) return Boolean is
1061 if Nkind
(Expr
) = N_Pragma_Argument_Association
then
1062 Expr
:= Get_Pragma_Arg
(Expr
);
1065 -- Determine whether the expression of the aspect or pragma is static
1066 -- and denotes True.
1068 if Present
(Expr
) then
1069 Preanalyze_And_Resolve
(Expr
);
1072 Is_OK_Static_Expression
(Expr
)
1073 and then Is_True
(Expr_Value
(Expr
));
1075 -- Otherwise Ghost defaults to True
1080 end Enables_Ghostness
;
1084 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1087 Prev_Id
: Entity_Id
;
1089 -- Start of processing for Is_Subject_To_Ghost
1092 -- The related entity of the declaration has not been analyzed yet, do
1093 -- not inspect its attributes.
1095 if Ekind
(Id
) = E_Void
then
1098 elsif Is_Ghost_Entity
(Id
) then
1101 -- The completion of a type or a constant is not fully analyzed when the
1102 -- reference to the Ghost entity is resolved. Because the completion is
1103 -- not marked as Ghost yet, inspect the partial view.
1105 elsif Is_Record_Type
(Id
)
1106 or else Ekind
(Id
) = E_Constant
1107 or else (Nkind
(N
) = N_Object_Declaration
1108 and then Constant_Present
(N
))
1110 Prev_Id
:= Incomplete_Or_Partial_View
(Id
);
1112 if Present
(Prev_Id
) and then Is_Ghost_Entity
(Prev_Id
) then
1117 -- Examine the aspect specifications (if any) looking for aspect Ghost
1119 if Permits_Aspect_Specifications
(N
) then
1120 Asp
:= First
(Aspect_Specifications
(N
));
1121 while Present
(Asp
) loop
1122 if Chars
(Identifier
(Asp
)) = Name_Ghost
then
1123 return Enables_Ghostness
(Expression
(Asp
));
1132 -- When the context is a [generic] package declaration, pragma Ghost
1133 -- resides in the visible declarations.
1135 if Nkind_In
(N
, N_Generic_Package_Declaration
,
1136 N_Package_Declaration
)
1138 Decl
:= First
(Visible_Declarations
(Specification
(N
)));
1140 -- When the context is a package or a subprogram body, pragma Ghost
1141 -- resides in the declarative part.
1143 elsif Nkind_In
(N
, N_Package_Body
, N_Subprogram_Body
) then
1144 Decl
:= First
(Declarations
(N
));
1146 -- Otherwise pragma Ghost appears in the declarations following N
1148 elsif Is_List_Member
(N
) then
1152 while Present
(Decl
) loop
1153 if Nkind
(Decl
) = N_Pragma
1154 and then Pragma_Name
(Decl
) = Name_Ghost
1157 Enables_Ghostness
(First
(Pragma_Argument_Associations
(Decl
)));
1159 -- A source construct ends the region where pragma Ghost may appear,
1160 -- stop the traversal. Check the original node as source constructs
1161 -- may be rewritten into something else by expansion.
1163 elsif Comes_From_Source
(Original_Node
(Decl
)) then
1171 end Is_Subject_To_Ghost
;
1179 Ignored_Ghost_Units
.Release
;
1180 Ignored_Ghost_Units
.Locked
:= True;
1183 -----------------------------------
1184 -- Mark_And_Set_Ghost_Assignment --
1185 -----------------------------------
1187 procedure Mark_And_Set_Ghost_Assignment
(N
: Node_Id
) is
1191 -- An assignment statement becomes Ghost when its target denotes a Ghost
1192 -- object. Install the Ghost mode of the target.
1194 Id
:= Ghost_Entity
(Name
(N
));
1196 if Present
(Id
) then
1197 if Is_Checked_Ghost_Entity
(Id
) then
1198 Install_Ghost_Region
(Check
, N
);
1200 elsif Is_Ignored_Ghost_Entity
(Id
) then
1201 Install_Ghost_Region
(Ignore
, N
);
1203 Set_Is_Ignored_Ghost_Node
(N
);
1204 Propagate_Ignored_Ghost_Code
(N
);
1207 end Mark_And_Set_Ghost_Assignment
;
1209 -----------------------------
1210 -- Mark_And_Set_Ghost_Body --
1211 -----------------------------
1213 procedure Mark_And_Set_Ghost_Body
1215 Spec_Id
: Entity_Id
)
1217 Body_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1218 Policy
: Name_Id
:= No_Name
;
1221 -- A body becomes Ghost when it is subject to aspect or pragma Ghost
1223 if Is_Subject_To_Ghost
(N
) then
1224 Policy
:= Policy_In_Effect
(Name_Ghost
);
1226 -- A body declared within a Ghost region is automatically Ghost
1227 -- (SPARK RM 6.9(2)).
1229 elsif Ghost_Mode
= Check
then
1230 Policy
:= Name_Check
;
1232 elsif Ghost_Mode
= Ignore
then
1233 Policy
:= Name_Ignore
;
1235 -- Inherit the "ghostness" of the previous declaration when the body
1236 -- acts as a completion.
1238 elsif Present
(Spec_Id
) then
1239 if Is_Checked_Ghost_Entity
(Spec_Id
) then
1240 Policy
:= Name_Check
;
1242 elsif Is_Ignored_Ghost_Entity
(Spec_Id
) then
1243 Policy
:= Name_Ignore
;
1247 -- The Ghost policy in effect at the point of declaration and at the
1248 -- point of completion must match (SPARK RM 6.9(14)).
1250 Check_Ghost_Completion
1251 (Prev_Id
=> Spec_Id
,
1252 Compl_Id
=> Body_Id
);
1254 -- Mark the body as its formals as Ghost
1256 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1258 -- Install the appropriate Ghost region
1260 Install_Ghost_Region
(Policy
, N
);
1261 end Mark_And_Set_Ghost_Body
;
1263 -----------------------------------
1264 -- Mark_And_Set_Ghost_Completion --
1265 -----------------------------------
1267 procedure Mark_And_Set_Ghost_Completion
1269 Prev_Id
: Entity_Id
)
1271 Compl_Id
: constant Entity_Id
:= Defining_Entity
(N
);
1272 Policy
: Name_Id
:= No_Name
;
1275 -- A completion elaborated in a Ghost region is automatically Ghost
1276 -- (SPARK RM 6.9(2)).
1278 if Ghost_Mode
= Check
then
1279 Policy
:= Name_Check
;
1281 elsif Ghost_Mode
= Ignore
then
1282 Policy
:= Name_Ignore
;
1284 -- The completion becomes Ghost when its initial declaration is also
1287 elsif Is_Checked_Ghost_Entity
(Prev_Id
) then
1288 Policy
:= Name_Check
;
1290 elsif Is_Ignored_Ghost_Entity
(Prev_Id
) then
1291 Policy
:= Name_Ignore
;
1294 -- The Ghost policy in effect at the point of declaration and at the
1295 -- point of completion must match (SPARK RM 6.9(14)).
1297 Check_Ghost_Completion
1298 (Prev_Id
=> Prev_Id
,
1299 Compl_Id
=> Compl_Id
);
1301 -- Mark the completion as Ghost
1303 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1305 -- Install the appropriate Ghost region
1307 Install_Ghost_Region
(Policy
, N
);
1308 end Mark_And_Set_Ghost_Completion
;
1310 ------------------------------------
1311 -- Mark_And_Set_Ghost_Declaration --
1312 ------------------------------------
1314 procedure Mark_And_Set_Ghost_Declaration
(N
: Node_Id
) is
1316 Policy
: Name_Id
:= No_Name
;
1319 -- A declaration becomes Ghost when it is subject to aspect or pragma
1322 if Is_Subject_To_Ghost
(N
) then
1323 Policy
:= Policy_In_Effect
(Name_Ghost
);
1325 -- A declaration elaborated in a Ghost region is automatically Ghost
1326 -- (SPARK RM 6.9(2)).
1328 elsif Ghost_Mode
= Check
then
1329 Policy
:= Name_Check
;
1331 elsif Ghost_Mode
= Ignore
then
1332 Policy
:= Name_Ignore
;
1334 -- A child package or subprogram declaration becomes Ghost when its
1335 -- parent is Ghost (SPARK RM 6.9(2)).
1337 elsif Nkind_In
(N
, N_Generic_Function_Renaming_Declaration
,
1338 N_Generic_Package_Declaration
,
1339 N_Generic_Package_Renaming_Declaration
,
1340 N_Generic_Procedure_Renaming_Declaration
,
1341 N_Generic_Subprogram_Declaration
,
1342 N_Package_Declaration
,
1343 N_Package_Renaming_Declaration
,
1344 N_Subprogram_Declaration
,
1345 N_Subprogram_Renaming_Declaration
)
1346 and then Present
(Parent_Spec
(N
))
1348 Par_Id
:= Defining_Entity
(Unit
(Parent_Spec
(N
)));
1350 if Is_Checked_Ghost_Entity
(Par_Id
) then
1351 Policy
:= Name_Check
;
1353 elsif Is_Ignored_Ghost_Entity
(Par_Id
) then
1354 Policy
:= Name_Ignore
;
1358 -- Mark the declaration and its formals as Ghost
1360 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1362 -- Install the appropriate Ghost region
1364 Install_Ghost_Region
(Policy
, N
);
1365 end Mark_And_Set_Ghost_Declaration
;
1367 --------------------------------------
1368 -- Mark_And_Set_Ghost_Instantiation --
1369 --------------------------------------
1371 procedure Mark_And_Set_Ghost_Instantiation
1375 procedure Check_Ghost_Actuals
;
1376 -- Check the context of ghost actuals
1378 -------------------------
1379 -- Check_Ghost_Actuals --
1380 -------------------------
1382 procedure Check_Ghost_Actuals
is
1383 Assoc
: Node_Id
:= First
(Generic_Associations
(N
));
1387 while Present
(Assoc
) loop
1388 if Nkind
(Assoc
) /= N_Others_Choice
then
1389 Act
:= Explicit_Generic_Actual_Parameter
(Assoc
);
1391 -- Within a nested instantiation, a defaulted actual is an
1392 -- empty association, so nothing to check.
1397 elsif Comes_From_Source
(Act
)
1398 and then Nkind
(Act
) in N_Has_Etype
1399 and then Present
(Etype
(Act
))
1400 and then Is_Ghost_Entity
(Etype
(Act
))
1402 Check_Ghost_Context
(Etype
(Act
), Act
);
1408 end Check_Ghost_Actuals
;
1412 Policy
: Name_Id
:= No_Name
;
1415 -- An instantiation becomes Ghost when it is subject to pragma Ghost
1417 if Is_Subject_To_Ghost
(N
) then
1418 Policy
:= Policy_In_Effect
(Name_Ghost
);
1420 -- An instantiation declaration within a Ghost region is automatically
1421 -- Ghost (SPARK RM 6.9(2)).
1423 elsif Ghost_Mode
= Check
then
1424 Policy
:= Name_Check
;
1426 elsif Ghost_Mode
= Ignore
then
1427 Policy
:= Name_Ignore
;
1429 -- Inherit the "ghostness" of the generic unit
1431 elsif Is_Checked_Ghost_Entity
(Gen_Id
) then
1432 Policy
:= Name_Check
;
1434 elsif Is_Ignored_Ghost_Entity
(Gen_Id
) then
1435 Policy
:= Name_Ignore
;
1438 -- Mark the instantiation as Ghost
1440 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1442 -- Install the appropriate Ghost region
1444 Install_Ghost_Region
(Policy
, N
);
1446 -- Check Ghost actuals. Given that this routine is unconditionally
1447 -- invoked with subprogram and package instantiations, this check
1448 -- verifies the context of all the ghost entities passed in generic
1451 Check_Ghost_Actuals
;
1452 end Mark_And_Set_Ghost_Instantiation
;
1454 ---------------------------------------
1455 -- Mark_And_Set_Ghost_Procedure_Call --
1456 ---------------------------------------
1458 procedure Mark_And_Set_Ghost_Procedure_Call
(N
: Node_Id
) is
1462 -- A procedure call becomes Ghost when the procedure being invoked is
1463 -- Ghost. Install the Ghost mode of the procedure.
1465 Id
:= Ghost_Entity
(Name
(N
));
1467 if Present
(Id
) then
1468 if Is_Checked_Ghost_Entity
(Id
) then
1469 Install_Ghost_Region
(Check
, N
);
1471 elsif Is_Ignored_Ghost_Entity
(Id
) then
1472 Install_Ghost_Region
(Ignore
, N
);
1474 Set_Is_Ignored_Ghost_Node
(N
);
1475 Propagate_Ignored_Ghost_Code
(N
);
1478 end Mark_And_Set_Ghost_Procedure_Call
;
1480 ------------------------------------
1481 -- Mark_Ghost_Declaration_Or_Body --
1482 ------------------------------------
1484 procedure Mark_Ghost_Declaration_Or_Body
1488 Id
: constant Entity_Id
:= Defining_Entity
(N
);
1490 Mark_Formals
: Boolean := False;
1492 Param_Id
: Entity_Id
;
1495 -- Mark the related node and its entity
1497 if Mode
= Name_Check
then
1498 Mark_Formals
:= True;
1499 Set_Is_Checked_Ghost_Entity
(Id
);
1501 elsif Mode
= Name_Ignore
then
1502 Mark_Formals
:= True;
1503 Set_Is_Ignored_Ghost_Entity
(Id
);
1504 Set_Is_Ignored_Ghost_Node
(N
);
1505 Propagate_Ignored_Ghost_Code
(N
);
1508 -- Mark all formal parameters when the related node denotes a subprogram
1509 -- or a body. The traversal is performed via the specification because
1510 -- the related subprogram or body may be unanalyzed.
1512 -- ??? could extra formal parameters cause a Ghost leak?
1515 and then Nkind_In
(N
, N_Abstract_Subprogram_Declaration
,
1516 N_Formal_Abstract_Subprogram_Declaration
,
1517 N_Formal_Concrete_Subprogram_Declaration
,
1518 N_Generic_Subprogram_Declaration
,
1520 N_Subprogram_Body_Stub
,
1521 N_Subprogram_Declaration
,
1522 N_Subprogram_Renaming_Declaration
)
1524 Param
:= First
(Parameter_Specifications
(Specification
(N
)));
1525 while Present
(Param
) loop
1526 Param_Id
:= Defining_Entity
(Param
);
1528 if Mode
= Name_Check
then
1529 Set_Is_Checked_Ghost_Entity
(Param_Id
);
1531 elsif Mode
= Name_Ignore
then
1532 Set_Is_Ignored_Ghost_Entity
(Param_Id
);
1538 end Mark_Ghost_Declaration_Or_Body
;
1540 -----------------------
1541 -- Mark_Ghost_Clause --
1542 -----------------------
1544 procedure Mark_Ghost_Clause
(N
: Node_Id
) is
1545 Nam
: Node_Id
:= Empty
;
1548 if Nkind
(N
) = N_Use_Package_Clause
then
1551 elsif Nkind
(N
) = N_Use_Type_Clause
then
1552 Nam
:= Subtype_Mark
(N
);
1554 elsif Nkind
(N
) = N_With_Clause
then
1559 and then Is_Entity_Name
(Nam
)
1560 and then Present
(Entity
(Nam
))
1561 and then Is_Ignored_Ghost_Entity
(Entity
(Nam
))
1563 Set_Is_Ignored_Ghost_Node
(N
);
1564 Propagate_Ignored_Ghost_Code
(N
);
1566 end Mark_Ghost_Clause
;
1568 -----------------------
1569 -- Mark_Ghost_Pragma --
1570 -----------------------
1572 procedure Mark_Ghost_Pragma
1577 -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
1580 if Is_Checked_Ghost_Entity
(Id
) then
1581 Set_Is_Checked_Ghost_Pragma
(N
);
1583 elsif Is_Ignored_Ghost_Entity
(Id
) then
1584 Set_Is_Ignored_Ghost_Pragma
(N
);
1585 Set_Is_Ignored_Ghost_Node
(N
);
1586 Propagate_Ignored_Ghost_Code
(N
);
1588 end Mark_Ghost_Pragma
;
1590 -------------------------
1591 -- Mark_Ghost_Renaming --
1592 -------------------------
1594 procedure Mark_Ghost_Renaming
1598 Policy
: Name_Id
:= No_Name
;
1601 -- A renaming becomes Ghost when it renames a Ghost entity
1603 if Is_Checked_Ghost_Entity
(Id
) then
1604 Policy
:= Name_Check
;
1606 elsif Is_Ignored_Ghost_Entity
(Id
) then
1607 Policy
:= Name_Ignore
;
1610 Mark_Ghost_Declaration_Or_Body
(N
, Policy
);
1611 end Mark_Ghost_Renaming
;
1613 ------------------------
1614 -- Name_To_Ghost_Mode --
1615 ------------------------
1617 function Name_To_Ghost_Mode
(Mode
: Name_Id
) return Ghost_Mode_Type
is
1619 if Mode
= Name_Check
then
1622 elsif Mode
= Name_Ignore
then
1625 -- Otherwise the mode must denote one of the following:
1627 -- * Disable indicates that the Ghost policy in effect is Disable
1629 -- * None or No_Name indicates that the associated construct is not
1630 -- subject to any Ghost annotation.
1633 pragma Assert
(Nam_In
(Mode
, Name_Disable
, Name_None
, No_Name
));
1636 end Name_To_Ghost_Mode
;
1638 ----------------------------------
1639 -- Propagate_Ignored_Ghost_Code --
1640 ----------------------------------
1642 procedure Propagate_Ignored_Ghost_Code
(N
: Node_Id
) is
1647 -- Traverse the parent chain looking for blocks, packages, and
1648 -- subprograms or their respective bodies.
1651 while Present
(Nod
) loop
1654 if Nkind
(Nod
) = N_Block_Statement
1655 and then Present
(Identifier
(Nod
))
1657 Scop
:= Entity
(Identifier
(Nod
));
1659 elsif Nkind_In
(Nod
, N_Package_Body
,
1660 N_Package_Declaration
,
1662 N_Subprogram_Declaration
)
1664 Scop
:= Defining_Entity
(Nod
);
1667 -- The current node denotes a scoping construct
1669 if Present
(Scop
) then
1671 -- Stop the traversal when the scope already contains ignored
1672 -- Ghost code as all enclosing scopes have already been marked.
1674 if Contains_Ignored_Ghost_Code
(Scop
) then
1677 -- Otherwise mark this scope and keep climbing
1680 Set_Contains_Ignored_Ghost_Code
(Scop
);
1684 Nod
:= Parent
(Nod
);
1687 -- The unit containing the ignored Ghost code must be post processed
1688 -- before invoking the back end.
1690 Add_Ignored_Ghost_Unit
(Cunit
(Get_Code_Unit
(N
)));
1691 end Propagate_Ignored_Ghost_Code
;
1693 -------------------------------
1694 -- Remove_Ignored_Ghost_Code --
1695 -------------------------------
1697 procedure Remove_Ignored_Ghost_Code
is
1698 procedure Prune_Tree
(Root
: Node_Id
);
1699 -- Remove all code marked as ignored Ghost from the tree of denoted by
1706 procedure Prune_Tree
(Root
: Node_Id
) is
1707 procedure Prune
(N
: Node_Id
);
1708 -- Remove a given node from the tree by rewriting it into null
1710 function Prune_Node
(N
: Node_Id
) return Traverse_Result
;
1711 -- Determine whether node N denotes an ignored Ghost construct. If
1712 -- this is the case, rewrite N as a null statement. See the body for
1719 procedure Prune
(N
: Node_Id
) is
1721 -- Destroy any aspects that may be associated with the node
1723 if Permits_Aspect_Specifications
(N
) and then Has_Aspects
(N
) then
1727 Rewrite
(N
, Make_Null_Statement
(Sloc
(N
)));
1734 function Prune_Node
(N
: Node_Id
) return Traverse_Result
is
1738 -- Do not prune compilation unit nodes because many mechanisms
1739 -- depend on their presence. Note that context items are still
1742 if Nkind
(N
) = N_Compilation_Unit
then
1745 -- The node is either declared as ignored Ghost or is a byproduct
1746 -- of expansion. Destroy it and stop the traversal on this branch.
1748 elsif Is_Ignored_Ghost_Node
(N
) then
1752 -- Scoping constructs such as blocks, packages, subprograms and
1753 -- bodies offer some flexibility with respect to pruning.
1755 elsif Nkind_In
(N
, N_Block_Statement
,
1757 N_Package_Declaration
,
1759 N_Subprogram_Declaration
)
1761 if Nkind
(N
) = N_Block_Statement
then
1762 Id
:= Entity
(Identifier
(N
));
1764 Id
:= Defining_Entity
(N
);
1767 -- The scoping construct contains both living and ignored Ghost
1768 -- code, let the traversal prune all relevant nodes.
1770 if Contains_Ignored_Ghost_Code
(Id
) then
1773 -- Otherwise the construct contains only living code and should
1780 -- Otherwise keep searching for ignored Ghost nodes
1787 procedure Prune_Nodes
is new Traverse_Proc
(Prune_Node
);
1789 -- Start of processing for Prune_Tree
1795 -- Start of processing for Remove_Ignored_Ghost_Code
1798 for Index
in Ignored_Ghost_Units
.First
.. Ignored_Ghost_Units
.Last
loop
1799 Prune_Tree
(Ignored_Ghost_Units
.Table
(Index
));
1801 end Remove_Ignored_Ghost_Code
;
1803 --------------------------
1804 -- Restore_Ghost_Region --
1805 --------------------------
1807 procedure Restore_Ghost_Region
(Mode
: Ghost_Mode_Type
; N
: Node_Id
) is
1810 Ignored_Ghost_Region
:= N
;
1811 end Restore_Ghost_Region
;
1813 --------------------
1814 -- Set_Ghost_Mode --
1815 --------------------
1817 procedure Set_Ghost_Mode
(N
: Node_Or_Entity_Id
) is
1818 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
);
1819 -- Install the Ghost mode of entity Id
1821 --------------------------------
1822 -- Set_Ghost_Mode_From_Entity --
1823 --------------------------------
1825 procedure Set_Ghost_Mode_From_Entity
(Id
: Entity_Id
) is
1827 if Is_Checked_Ghost_Entity
(Id
) then
1828 Install_Ghost_Mode
(Check
);
1829 elsif Is_Ignored_Ghost_Entity
(Id
) then
1830 Install_Ghost_Mode
(Ignore
);
1832 Install_Ghost_Mode
(None
);
1834 end Set_Ghost_Mode_From_Entity
;
1840 -- Start of processing for Set_Ghost_Mode
1843 -- The Ghost mode of an assignment statement depends on the Ghost mode
1846 if Nkind
(N
) = N_Assignment_Statement
then
1847 Id
:= Ghost_Entity
(Name
(N
));
1849 if Present
(Id
) then
1850 Set_Ghost_Mode_From_Entity
(Id
);
1853 -- The Ghost mode of a body or a declaration depends on the Ghost mode
1854 -- of its defining entity.
1856 elsif Is_Body
(N
) or else Is_Declaration
(N
) then
1857 Set_Ghost_Mode_From_Entity
(Defining_Entity
(N
));
1859 -- The Ghost mode of an entity depends on the entity itself
1861 elsif Nkind
(N
) in N_Entity
then
1862 Set_Ghost_Mode_From_Entity
(N
);
1864 -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
1865 -- of the entity being frozen.
1867 elsif Nkind_In
(N
, N_Freeze_Entity
, N_Freeze_Generic_Entity
) then
1868 Set_Ghost_Mode_From_Entity
(Entity
(N
));
1870 -- The Ghost mode of a pragma depends on the associated entity. The
1871 -- property is encoded in the pragma itself.
1873 elsif Nkind
(N
) = N_Pragma
then
1874 if Is_Checked_Ghost_Pragma
(N
) then
1875 Install_Ghost_Mode
(Check
);
1876 elsif Is_Ignored_Ghost_Pragma
(N
) then
1877 Install_Ghost_Mode
(Ignore
);
1879 Install_Ghost_Mode
(None
);
1882 -- The Ghost mode of a procedure call depends on the Ghost mode of the
1883 -- procedure being invoked.
1885 elsif Nkind
(N
) = N_Procedure_Call_Statement
then
1886 Id
:= Ghost_Entity
(Name
(N
));
1888 if Present
(Id
) then
1889 Set_Ghost_Mode_From_Entity
(Id
);
1894 -------------------------
1895 -- Set_Is_Ghost_Entity --
1896 -------------------------
1898 procedure Set_Is_Ghost_Entity
(Id
: Entity_Id
) is
1899 Policy
: constant Name_Id
:= Policy_In_Effect
(Name_Ghost
);
1901 if Policy
= Name_Check
then
1902 Set_Is_Checked_Ghost_Entity
(Id
);
1903 elsif Policy
= Name_Ignore
then
1904 Set_Is_Ignored_Ghost_Entity
(Id
);
1906 end Set_Is_Ghost_Entity
;