]>
Commit | Line | Data |
---|---|---|
8636f52f HK |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- G H O S T -- | |
6 | -- -- | |
7 | -- B o d y -- | |
8 | -- -- | |
f9a8f910 | 9 | -- Copyright (C) 2014-2017, Free Software Foundation, Inc. -- |
8636f52f HK |
10 | -- -- |
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. -- | |
20 | -- -- | |
21 | -- GNAT was originally developed by the GNAT team at New York University. -- | |
22 | -- Extensive contributions were provided by Ada Core Technologies Inc. -- | |
23 | -- -- | |
24 | ------------------------------------------------------------------------------ | |
25 | ||
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; | |
32 | with Lib; use Lib; | |
33 | with Namet; use Namet; | |
34 | with Nlists; use Nlists; | |
35 | with Nmake; use Nmake; | |
8636f52f HK |
36 | with Sem; use Sem; |
37 | with Sem_Aux; use Sem_Aux; | |
4179af27 | 38 | with Sem_Disp; use Sem_Disp; |
8636f52f | 39 | with Sem_Eval; use Sem_Eval; |
241ebe89 | 40 | with Sem_Prag; use Sem_Prag; |
8636f52f HK |
41 | with Sem_Res; use Sem_Res; |
42 | with Sem_Util; use Sem_Util; | |
43 | with Sinfo; use Sinfo; | |
44 | with Snames; use Snames; | |
45 | with Table; | |
46 | ||
47 | package body Ghost is | |
48 | ||
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 | |
52 | -- units. | |
53 | ||
54 | package Ignored_Ghost_Units is new Table.Table ( | |
55 | Table_Component_Type => Node_Id, | |
56 | Table_Index_Type => Int, | |
57 | Table_Low_Bound => 0, | |
58 | Table_Initial => Alloc.Ignored_Ghost_Units_Initial, | |
59 | Table_Increment => Alloc.Ignored_Ghost_Units_Increment, | |
60 | Table_Name => "Ignored_Ghost_Units"); | |
61 | ||
62 | ----------------------- | |
63 | -- Local Subprograms -- | |
64 | ----------------------- | |
65 | ||
241ebe89 | 66 | function Ghost_Entity (N : Node_Id) return Entity_Id; |
d65a80fd HK |
67 | -- Find the entity of a reference to a Ghost entity. Return Empty if there |
68 | -- is no such entity. | |
69 | ||
70 | procedure Install_Ghost_Mode (Mode : Name_Id); | |
71 | -- Install a specific Ghost mode denoted by Mode by setting global variable | |
72 | -- Ghost_Mode. | |
241ebe89 | 73 | |
1af4455a | 74 | function Is_Subject_To_Ghost (N : Node_Id) return Boolean; |
d65a80fd HK |
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" | |
78 | -- of N. | |
79 | ||
80 | procedure Mark_Ghost_Declaration_Or_Body | |
81 | (N : Node_Id; | |
82 | Mode : Name_Id); | |
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 | |
85 | -- body. | |
1af4455a | 86 | |
8636f52f | 87 | procedure Propagate_Ignored_Ghost_Code (N : Node_Id); |
d65a80fd HK |
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. | |
8636f52f HK |
91 | |
92 | ---------------------------- | |
93 | -- Add_Ignored_Ghost_Unit -- | |
94 | ---------------------------- | |
95 | ||
96 | procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is | |
97 | begin | |
98 | pragma Assert (Nkind (Unit) = N_Compilation_Unit); | |
99 | ||
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. | |
103 | ||
104 | for Index in reverse Ignored_Ghost_Units.First .. | |
105 | Ignored_Ghost_Units.Last | |
106 | loop | |
18dae814 | 107 | -- If the unit is already present in the table, do not add it again |
8636f52f HK |
108 | |
109 | if Unit = Ignored_Ghost_Units.Table (Index) then | |
110 | return; | |
111 | end if; | |
112 | end loop; | |
113 | ||
114 | -- If we get here, then this is the first time the unit is being added | |
115 | ||
116 | Ignored_Ghost_Units.Append (Unit); | |
117 | end Add_Ignored_Ghost_Unit; | |
118 | ||
119 | ---------------------------- | |
120 | -- Check_Ghost_Completion -- | |
121 | ---------------------------- | |
122 | ||
123 | procedure Check_Ghost_Completion | |
d65a80fd HK |
124 | (Prev_Id : Entity_Id; |
125 | Compl_Id : Entity_Id) | |
8636f52f HK |
126 | is |
127 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); | |
128 | ||
129 | begin | |
d65a80fd HK |
130 | -- Nothing to do if one of the views is missing |
131 | ||
132 | if No (Prev_Id) or else No (Compl_Id) then | |
133 | null; | |
134 | ||
8636f52f | 135 | -- The Ghost policy in effect at the point of declaration and at the |
c2cfccb1 | 136 | -- point of completion must match (SPARK RM 6.9(14)). |
8636f52f | 137 | |
d65a80fd | 138 | elsif Is_Checked_Ghost_Entity (Prev_Id) |
8636f52f HK |
139 | and then Policy = Name_Ignore |
140 | then | |
d65a80fd | 141 | Error_Msg_Sloc := Sloc (Compl_Id); |
8636f52f | 142 | |
d65a80fd HK |
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); | |
8636f52f | 146 | |
d65a80fd | 147 | elsif Is_Ignored_Ghost_Entity (Prev_Id) |
8636f52f HK |
148 | and then Policy = Name_Check |
149 | then | |
d65a80fd | 150 | Error_Msg_Sloc := Sloc (Compl_Id); |
8636f52f | 151 | |
d65a80fd HK |
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); | |
8636f52f HK |
155 | end if; |
156 | end Check_Ghost_Completion; | |
157 | ||
158 | ------------------------- | |
159 | -- Check_Ghost_Context -- | |
160 | ------------------------- | |
161 | ||
162 | procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is | |
ac8380d5 | 163 | procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id); |
8636f52f | 164 | -- Verify that the Ghost policy at the point of declaration of entity Id |
ac8380d5 AC |
165 | -- matches the policy at the point of reference Ref. If this is not the |
166 | -- case emit an error at Ref. | |
8636f52f HK |
167 | |
168 | function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; | |
169 | -- Determine whether node Context denotes a Ghost-friendly context where | |
4179af27 | 170 | -- a Ghost entity can safely reside (SPARK RM 6.9(10)). |
8636f52f HK |
171 | |
172 | ------------------------- | |
173 | -- Is_OK_Ghost_Context -- | |
174 | ------------------------- | |
175 | ||
176 | function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is | |
241ebe89 HK |
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 | |
d65a80fd HK |
180 | -- |
181 | -- * Define a Ghost entity | |
182 | -- | |
183 | -- * Be subject to pragma Ghost | |
241ebe89 HK |
184 | |
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 | |
d65a80fd HK |
188 | -- |
189 | -- * Be an assertion expression pragma | |
190 | -- | |
191 | -- * Denote pragma Global, Depends, Initializes, Refined_Global, | |
192 | -- Refined_Depends or Refined_State. | |
193 | -- | |
194 | -- * Specify an aspect of a Ghost entity | |
195 | -- | |
196 | -- * Contain a reference to a Ghost entity | |
241ebe89 HK |
197 | |
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 | |
d65a80fd HK |
201 | -- |
202 | -- * Denote a procedure call to a Ghost procedure | |
203 | -- | |
204 | -- * Denote an assignment statement whose target is Ghost | |
241ebe89 HK |
205 | |
206 | ----------------------- | |
207 | -- Is_OK_Declaration -- | |
208 | ----------------------- | |
209 | ||
210 | function Is_OK_Declaration (Decl : Node_Id) return Boolean is | |
6d0d18dc AC |
211 | function In_Subprogram_Body_Profile (N : Node_Id) return Boolean; |
212 | -- Determine whether node N appears in the profile of a subprogram | |
213 | -- body. | |
214 | ||
6d0d18dc AC |
215 | -------------------------------- |
216 | -- In_Subprogram_Body_Profile -- | |
217 | -------------------------------- | |
218 | ||
219 | function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is | |
220 | Spec : constant Node_Id := Parent (N); | |
221 | ||
222 | begin | |
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. | |
226 | ||
227 | return | |
228 | (Nkind (N) = N_Parameter_Specification | |
229 | or else | |
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; | |
234 | ||
241ebe89 HK |
235 | -- Local variables |
236 | ||
8636f52f HK |
237 | Subp_Decl : Node_Id; |
238 | Subp_Id : Entity_Id; | |
239 | ||
241ebe89 HK |
240 | -- Start of processing for Is_OK_Declaration |
241 | ||
8636f52f | 242 | begin |
d65a80fd HK |
243 | if Is_Ghost_Declaration (Decl) then |
244 | return True; | |
8636f52f | 245 | |
241ebe89 | 246 | -- Special cases |
8636f52f | 247 | |
6d0d18dc AC |
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. | |
252 | ||
253 | elsif In_Subprogram_Body_Profile (Decl) then | |
254 | return True; | |
255 | ||
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. | |
8636f52f | 261 | |
6d0d18dc AC |
262 | elsif Nkind (Decl) = N_Expression_Function |
263 | and then not Analyzed (Decl) | |
241ebe89 HK |
264 | then |
265 | return True; | |
8636f52f | 266 | |
241ebe89 HK |
267 | -- References to Ghost entities may be relocated in internally |
268 | -- generated bodies. | |
8636f52f | 269 | |
241ebe89 HK |
270 | elsif Nkind (Decl) = N_Subprogram_Body |
271 | and then not Comes_From_Source (Decl) | |
272 | then | |
273 | Subp_Id := Corresponding_Spec (Decl); | |
8636f52f | 274 | |
241ebe89 | 275 | if Present (Subp_Id) then |
241ebe89 | 276 | |
c37e6613 HK |
277 | -- The context is the internally built _Postconditions |
278 | -- procedure, which is OK because the real check was done | |
279 | -- before expansion activities. | |
7f5e1dee JM |
280 | |
281 | if Chars (Subp_Id) = Name_uPostconditions then | |
282 | return True; | |
283 | ||
1155ae01 AC |
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. | |
287 | ||
288 | elsif Is_Predicate_Function (Subp_Id) then | |
289 | return True; | |
290 | ||
7f5e1dee JM |
291 | else |
292 | Subp_Decl := | |
293 | Original_Node (Unit_Declaration_Node (Subp_Id)); | |
294 | ||
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. | |
298 | ||
299 | if Nkind (Subp_Decl) = N_Expression_Function then | |
d65a80fd | 300 | return Is_Ghost_Declaration (Subp_Decl); |
7f5e1dee | 301 | end if; |
8636f52f HK |
302 | end if; |
303 | ||
241ebe89 HK |
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. | |
8636f52f | 307 | |
241ebe89 | 308 | else |
8636f52f HK |
309 | return True; |
310 | end if; | |
241ebe89 | 311 | end if; |
8636f52f HK |
312 | |
313 | return False; | |
241ebe89 | 314 | end Is_OK_Declaration; |
8636f52f | 315 | |
241ebe89 HK |
316 | ------------------ |
317 | -- Is_OK_Pragma -- | |
318 | ------------------ | |
8636f52f | 319 | |
241ebe89 HK |
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. | |
8636f52f | 325 | |
241ebe89 HK |
326 | -------------------- |
327 | -- Check_Policies -- | |
328 | -------------------- | |
8636f52f | 329 | |
241ebe89 HK |
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); | |
8636f52f HK |
333 | |
334 | begin | |
241ebe89 HK |
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)). | |
338 | ||
339 | if GP = Name_Ignore and then AP /= Name_Ignore then | |
340 | Error_Msg_N | |
ad4ba28b AC |
341 | ("incompatible ghost policies in effect", |
342 | Ghost_Ref); | |
241ebe89 HK |
343 | Error_Msg_NE |
344 | ("\ghost entity & has policy `Ignore`", | |
345 | Ghost_Ref, Ghost_Id); | |
346 | ||
347 | Error_Msg_Name_1 := AP; | |
348 | Error_Msg_N | |
349 | ("\assertion expression has policy %", Ghost_Ref); | |
350 | end if; | |
351 | end Check_Policies; | |
8636f52f HK |
352 | |
353 | -- Local variables | |
354 | ||
241ebe89 HK |
355 | Prag_Id : Pragma_Id; |
356 | Prag_Nam : Name_Id; | |
8636f52f | 357 | |
241ebe89 | 358 | -- Start of processing for Is_OK_Pragma |
8636f52f HK |
359 | |
360 | begin | |
241ebe89 HK |
361 | if Nkind (Prag) = N_Pragma then |
362 | Prag_Id := Get_Pragma_Id (Prag); | |
363 | Prag_Nam := Original_Aspect_Pragma_Name (Prag); | |
8636f52f | 364 | |
241ebe89 HK |
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)) | |
8636f52f | 367 | |
241ebe89 | 368 | if Is_Ghost_Pragma (Prag) then |
8636f52f | 369 | return True; |
8636f52f | 370 | |
95fef24f | 371 | -- An assertion expression pragma is Ghost when it contains a |
1155ae01 AC |
372 | -- reference to a Ghost entity (SPARK RM 6.9(10)), except for |
373 | -- predicate pragmas (SPARK RM 6.9(11)). | |
8636f52f | 374 | |
1155ae01 AC |
375 | elsif Assertion_Expression_Pragma (Prag_Id) |
376 | and then Prag_Id /= Pragma_Predicate | |
377 | then | |
4179af27 HK |
378 | -- Ensure that the assertion policy and the Ghost policy are |
379 | -- compatible (SPARK RM 6.9(18)). | |
8636f52f | 380 | |
4179af27 HK |
381 | Check_Policies (Prag_Nam); |
382 | return True; | |
8636f52f | 383 | |
241ebe89 HK |
384 | -- Several pragmas that may apply to a non-Ghost entity are |
385 | -- treated as Ghost when they contain a reference to a Ghost | |
4179af27 | 386 | -- entity (SPARK RM 6.9(11)). |
8636f52f | 387 | |
241ebe89 HK |
388 | elsif Nam_In (Prag_Nam, Name_Global, |
389 | Name_Depends, | |
390 | Name_Initializes, | |
391 | Name_Refined_Global, | |
392 | Name_Refined_Depends, | |
393 | Name_Refined_State) | |
394 | then | |
395 | return True; | |
241ebe89 HK |
396 | end if; |
397 | end if; | |
8636f52f HK |
398 | |
399 | return False; | |
241ebe89 | 400 | end Is_OK_Pragma; |
8636f52f | 401 | |
241ebe89 HK |
402 | --------------------- |
403 | -- Is_OK_Statement -- | |
404 | --------------------- | |
8636f52f | 405 | |
241ebe89 | 406 | function Is_OK_Statement (Stmt : Node_Id) return Boolean is |
241ebe89 | 407 | begin |
d65a80fd HK |
408 | -- An assignment statement is Ghost when the target is a Ghost |
409 | -- entity. | |
8636f52f | 410 | |
d65a80fd HK |
411 | if Nkind (Stmt) = N_Assignment_Statement then |
412 | return Is_Ghost_Assignment (Stmt); | |
8636f52f | 413 | |
d65a80fd HK |
414 | -- A procedure call is Ghost when it calls a Ghost procedure |
415 | ||
416 | elsif Nkind (Stmt) = N_Procedure_Call_Statement then | |
417 | return Is_Ghost_Procedure_Call (Stmt); | |
241ebe89 HK |
418 | |
419 | -- Special cases | |
420 | ||
95fef24f AC |
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. | |
241ebe89 | 425 | |
95fef24f AC |
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))) | |
430 | then | |
431 | return True; | |
241ebe89 HK |
432 | end if; |
433 | ||
434 | return False; | |
435 | end Is_OK_Statement; | |
436 | ||
437 | -- Local variables | |
8636f52f | 438 | |
241ebe89 | 439 | Par : Node_Id; |
8636f52f | 440 | |
241ebe89 HK |
441 | -- Start of processing for Is_OK_Ghost_Context |
442 | ||
443 | begin | |
444 | -- The context is Ghost when it appears within a Ghost package or | |
445 | -- subprogram. | |
446 | ||
447 | if Ghost_Mode > None then | |
8636f52f HK |
448 | return True; |
449 | ||
0bb97bdf YM |
450 | -- A Ghost type may be referenced in a use_type clause |
451 | -- (SPARK RM 6.9.10). | |
452 | ||
453 | elsif Present (Parent (Context)) | |
454 | and then Nkind (Parent (Context)) = N_Use_Type_Clause | |
455 | then | |
456 | return True; | |
457 | ||
8636f52f HK |
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 | |
461 | -- context. | |
462 | ||
463 | elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then | |
464 | return True; | |
465 | ||
241ebe89 HK |
466 | -- Otherwise climb the parent chain looking for a suitable Ghost |
467 | -- context. | |
468 | ||
8636f52f | 469 | else |
241ebe89 HK |
470 | Par := Context; |
471 | while Present (Par) loop | |
472 | if Is_Ignored_Ghost_Node (Par) then | |
473 | return True; | |
474 | ||
475 | -- A reference to a Ghost entity can appear within an aspect | |
1155ae01 AC |
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)). | |
481 | ||
482 | elsif Nkind (Par) = N_Aspect_Specification | |
483 | and then not Same_Aspect | |
484 | (Get_Aspect_Id (Par), Aspect_Predicate) | |
485 | then | |
241ebe89 HK |
486 | return True; |
487 | ||
488 | elsif Is_OK_Declaration (Par) then | |
489 | return True; | |
490 | ||
491 | elsif Is_OK_Pragma (Par) then | |
492 | return True; | |
493 | ||
494 | elsif Is_OK_Statement (Par) then | |
495 | return True; | |
496 | ||
497 | -- Prevent the search from going too far | |
498 | ||
499 | elsif Is_Body_Or_Package_Declaration (Par) then | |
95fef24f | 500 | exit; |
241ebe89 HK |
501 | end if; |
502 | ||
503 | Par := Parent (Par); | |
504 | end loop; | |
505 | ||
95fef24f AC |
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. | |
510 | ||
511 | if In_Assertion_Expr > 0 then | |
512 | return True; | |
513 | ||
514 | -- Otherwise the context is not suitable for a reference to a | |
515 | -- Ghost entity. | |
516 | ||
517 | else | |
518 | return False; | |
519 | end if; | |
8636f52f HK |
520 | end if; |
521 | end Is_OK_Ghost_Context; | |
522 | ||
523 | ------------------------ | |
524 | -- Check_Ghost_Policy -- | |
525 | ------------------------ | |
526 | ||
ac8380d5 | 527 | procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is |
8636f52f HK |
528 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); |
529 | ||
530 | begin | |
531 | -- The Ghost policy in effect a the point of declaration and at the | |
4179af27 | 532 | -- point of use must match (SPARK RM 6.9(13)). |
8636f52f | 533 | |
ac8380d5 AC |
534 | if Is_Checked_Ghost_Entity (Id) |
535 | and then Policy = Name_Ignore | |
536 | and then May_Be_Lvalue (Ref) | |
537 | then | |
538 | Error_Msg_Sloc := Sloc (Ref); | |
8636f52f | 539 | |
ac8380d5 AC |
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); | |
8636f52f HK |
543 | |
544 | elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then | |
ac8380d5 | 545 | Error_Msg_Sloc := Sloc (Ref); |
8636f52f | 546 | |
ac8380d5 AC |
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); | |
8636f52f HK |
550 | end if; |
551 | end Check_Ghost_Policy; | |
552 | ||
553 | -- Start of processing for Check_Ghost_Context | |
554 | ||
555 | begin | |
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. | |
559 | ||
560 | if Is_OK_Ghost_Context (Ghost_Ref) then | |
561 | Check_Ghost_Policy (Ghost_Id, Ghost_Ref); | |
562 | ||
563 | -- Otherwise the Ghost entity appears in a non-Ghost context and affects | |
ac8380d5 | 564 | -- its behavior or value (SPARK RM 6.9(10,11)). |
8636f52f HK |
565 | |
566 | else | |
1af4455a | 567 | Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref); |
8636f52f HK |
568 | end if; |
569 | end Check_Ghost_Context; | |
570 | ||
241ebe89 HK |
571 | ---------------------------- |
572 | -- Check_Ghost_Overriding -- | |
573 | ---------------------------- | |
574 | ||
575 | procedure Check_Ghost_Overriding | |
576 | (Subp : Entity_Id; | |
577 | Overridden_Subp : Entity_Id) | |
578 | is | |
4179af27 | 579 | Deriv_Typ : Entity_Id; |
95fef24f | 580 | Over_Subp : Entity_Id; |
241ebe89 HK |
581 | |
582 | begin | |
583 | if Present (Subp) and then Present (Overridden_Subp) then | |
95fef24f | 584 | Over_Subp := Ultimate_Alias (Overridden_Subp); |
4179af27 | 585 | Deriv_Typ := Find_Dispatching_Type (Subp); |
241ebe89 | 586 | |
4179af27 HK |
587 | -- A Ghost primitive of a non-Ghost type extension cannot override an |
588 | -- inherited non-Ghost primitive (SPARK RM 6.9(8)). | |
241ebe89 | 589 | |
4179af27 HK |
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) | |
393525af | 594 | and then not Is_Abstract_Subprogram (Over_Subp) |
241ebe89 | 595 | then |
4179af27 | 596 | Error_Msg_N ("incompatible overriding in effect", Subp); |
241ebe89 | 597 | |
95fef24f | 598 | Error_Msg_Sloc := Sloc (Over_Subp); |
4179af27 | 599 | Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); |
241ebe89 HK |
600 | |
601 | Error_Msg_Sloc := Sloc (Subp); | |
4179af27 HK |
602 | Error_Msg_N ("\overridden # with ghost subprogram", Subp); |
603 | end if; | |
604 | ||
605 | -- A non-Ghost primitive of a type extension cannot override an | |
606 | -- inherited Ghost primitive (SPARK RM 6.9(8)). | |
241ebe89 | 607 | |
f31dcd99 HK |
608 | if Is_Ghost_Entity (Over_Subp) |
609 | and then not Is_Ghost_Entity (Subp) | |
393525af | 610 | and then not Is_Abstract_Subprogram (Subp) |
241ebe89 | 611 | then |
4179af27 | 612 | Error_Msg_N ("incompatible overriding in effect", Subp); |
241ebe89 | 613 | |
95fef24f | 614 | Error_Msg_Sloc := Sloc (Over_Subp); |
4179af27 | 615 | Error_Msg_N ("\& declared # as ghost subprogram", Subp); |
241ebe89 HK |
616 | |
617 | Error_Msg_Sloc := Sloc (Subp); | |
4179af27 HK |
618 | Error_Msg_N ("\overridden # with non-ghost subprogram", Subp); |
619 | end if; | |
620 | ||
621 | if Present (Deriv_Typ) | |
622 | and then not Is_Ignored_Ghost_Entity (Deriv_Typ) | |
623 | then | |
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)). | |
628 | ||
629 | if Is_Ignored_Ghost_Entity (Subp) then | |
630 | ||
631 | -- Both the parent subprogram and overriding subprogram are | |
632 | -- ignored Ghost. | |
633 | ||
634 | if Is_Ignored_Ghost_Entity (Over_Subp) then | |
635 | null; | |
636 | ||
637 | -- The parent subprogram carries policy Check | |
638 | ||
639 | elsif Is_Checked_Ghost_Entity (Over_Subp) then | |
640 | Error_Msg_N | |
641 | ("incompatible ghost policies in effect", Subp); | |
642 | ||
643 | Error_Msg_Sloc := Sloc (Over_Subp); | |
644 | Error_Msg_N | |
645 | ("\& declared # with ghost policy `Check`", Subp); | |
646 | ||
647 | Error_Msg_Sloc := Sloc (Subp); | |
648 | Error_Msg_N | |
649 | ("\overridden # with ghost policy `Ignore`", Subp); | |
650 | ||
651 | -- The parent subprogram is non-Ghost | |
652 | ||
653 | else | |
654 | Error_Msg_N | |
655 | ("incompatible ghost policies in effect", Subp); | |
656 | ||
657 | Error_Msg_Sloc := Sloc (Over_Subp); | |
658 | Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); | |
659 | ||
660 | Error_Msg_Sloc := Sloc (Subp); | |
661 | Error_Msg_N | |
662 | ("\overridden # with ghost policy `Ignore`", Subp); | |
663 | end if; | |
664 | ||
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)). | |
669 | ||
670 | elsif Is_Ignored_Ghost_Entity (Over_Subp) then | |
671 | ||
672 | -- Both the parent subprogram and the overriding subprogram are | |
673 | -- ignored Ghost. | |
674 | ||
675 | if Is_Ignored_Ghost_Entity (Subp) then | |
676 | null; | |
677 | ||
678 | -- The overriding subprogram carries policy Check | |
679 | ||
680 | elsif Is_Checked_Ghost_Entity (Subp) then | |
681 | Error_Msg_N | |
682 | ("incompatible ghost policies in effect", Subp); | |
683 | ||
684 | Error_Msg_Sloc := Sloc (Over_Subp); | |
685 | Error_Msg_N | |
686 | ("\& declared # with ghost policy `Ignore`", Subp); | |
687 | ||
688 | Error_Msg_Sloc := Sloc (Subp); | |
689 | Error_Msg_N | |
690 | ("\overridden # with Ghost policy `Check`", Subp); | |
691 | ||
692 | -- The overriding subprogram is non-Ghost | |
693 | ||
694 | else | |
695 | Error_Msg_N | |
696 | ("incompatible ghost policies in effect", Subp); | |
697 | ||
698 | Error_Msg_Sloc := Sloc (Over_Subp); | |
699 | Error_Msg_N | |
700 | ("\& declared # with ghost policy `Ignore`", Subp); | |
701 | ||
702 | Error_Msg_Sloc := Sloc (Subp); | |
703 | Error_Msg_N | |
704 | ("\overridden # with non-ghost subprogram", Subp); | |
705 | end if; | |
706 | end if; | |
241ebe89 HK |
707 | end if; |
708 | end if; | |
709 | end Check_Ghost_Overriding; | |
710 | ||
4179af27 HK |
711 | --------------------------- |
712 | -- Check_Ghost_Primitive -- | |
713 | --------------------------- | |
714 | ||
715 | procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is | |
716 | begin | |
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)). | |
719 | ||
720 | if Is_Tagged_Type (Typ) then | |
721 | if Is_Checked_Ghost_Entity (Prim) | |
722 | and then Is_Ignored_Ghost_Entity (Typ) | |
723 | then | |
724 | Error_Msg_N ("incompatible ghost policies in effect", Prim); | |
725 | ||
726 | Error_Msg_Sloc := Sloc (Typ); | |
727 | Error_Msg_NE | |
728 | ("\tagged type & declared # with ghost policy `Ignore`", | |
729 | Prim, Typ); | |
730 | ||
731 | Error_Msg_Sloc := Sloc (Prim); | |
732 | Error_Msg_N | |
733 | ("\primitive subprogram & declared # with ghost policy `Check`", | |
734 | Prim); | |
735 | ||
736 | elsif Is_Ignored_Ghost_Entity (Prim) | |
737 | and then Is_Checked_Ghost_Entity (Typ) | |
738 | then | |
739 | Error_Msg_N ("incompatible ghost policies in effect", Prim); | |
740 | ||
741 | Error_Msg_Sloc := Sloc (Typ); | |
742 | Error_Msg_NE | |
743 | ("\tagged type & declared # with ghost policy `Check`", | |
744 | Prim, Typ); | |
745 | ||
746 | Error_Msg_Sloc := Sloc (Prim); | |
747 | Error_Msg_N | |
748 | ("\primitive subprogram & declared # with ghost policy `Ignore`", | |
749 | Prim); | |
750 | end if; | |
751 | end if; | |
752 | end Check_Ghost_Primitive; | |
753 | ||
754 | ---------------------------- | |
755 | -- Check_Ghost_Refinement -- | |
756 | ---------------------------- | |
757 | ||
758 | procedure Check_Ghost_Refinement | |
759 | (State : Node_Id; | |
760 | State_Id : Entity_Id; | |
761 | Constit : Node_Id; | |
762 | Constit_Id : Entity_Id) | |
763 | is | |
764 | begin | |
765 | if Is_Ghost_Entity (State_Id) then | |
766 | if Is_Ghost_Entity (Constit_Id) then | |
767 | ||
768 | -- The Ghost policy in effect at the point of abstract state | |
769 | -- declaration and constituent must match (SPARK RM 6.9(15)). | |
770 | ||
771 | if Is_Checked_Ghost_Entity (State_Id) | |
772 | and then Is_Ignored_Ghost_Entity (Constit_Id) | |
773 | then | |
774 | Error_Msg_Sloc := Sloc (Constit); | |
775 | SPARK_Msg_N ("incompatible ghost policies in effect", State); | |
776 | ||
777 | SPARK_Msg_NE | |
778 | ("\abstract state & declared with ghost policy `Check`", | |
779 | State, State_Id); | |
780 | SPARK_Msg_NE | |
781 | ("\constituent & declared # with ghost policy `Ignore`", | |
782 | State, Constit_Id); | |
783 | ||
784 | elsif Is_Ignored_Ghost_Entity (State_Id) | |
785 | and then Is_Checked_Ghost_Entity (Constit_Id) | |
786 | then | |
787 | Error_Msg_Sloc := Sloc (Constit); | |
788 | SPARK_Msg_N ("incompatible ghost policies in effect", State); | |
789 | ||
790 | SPARK_Msg_NE | |
791 | ("\abstract state & declared with ghost policy `Ignore`", | |
792 | State, State_Id); | |
793 | SPARK_Msg_NE | |
794 | ("\constituent & declared # with ghost policy `Check`", | |
795 | State, Constit_Id); | |
796 | end if; | |
797 | ||
798 | -- A constituent of a Ghost abstract state must be a Ghost entity | |
799 | -- (SPARK RM 7.2.2(12)). | |
800 | ||
801 | else | |
802 | SPARK_Msg_NE | |
803 | ("constituent of ghost state & must be ghost", | |
804 | Constit, State_Id); | |
805 | end if; | |
806 | end if; | |
807 | end Check_Ghost_Refinement; | |
808 | ||
241ebe89 HK |
809 | ------------------ |
810 | -- Ghost_Entity -- | |
811 | ------------------ | |
812 | ||
813 | function Ghost_Entity (N : Node_Id) return Entity_Id is | |
814 | Ref : Node_Id; | |
815 | ||
816 | begin | |
d65a80fd | 817 | -- When the reference denotes a subcomponent, recover the related |
241ebe89 HK |
818 | -- object (SPARK RM 6.9(1)). |
819 | ||
820 | Ref := N; | |
821 | while Nkind_In (Ref, N_Explicit_Dereference, | |
822 | N_Indexed_Component, | |
823 | N_Selected_Component, | |
824 | N_Slice) | |
825 | loop | |
826 | Ref := Prefix (Ref); | |
827 | end loop; | |
828 | ||
829 | if Is_Entity_Name (Ref) then | |
830 | return Entity (Ref); | |
831 | else | |
832 | return Empty; | |
833 | end if; | |
834 | end Ghost_Entity; | |
835 | ||
8636f52f HK |
836 | -------------------------------- |
837 | -- Implements_Ghost_Interface -- | |
838 | -------------------------------- | |
839 | ||
840 | function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is | |
841 | Iface_Elmt : Elmt_Id; | |
842 | ||
843 | begin | |
844 | -- Traverse the list of interfaces looking for a Ghost interface | |
845 | ||
846 | if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then | |
847 | Iface_Elmt := First_Elmt (Interfaces (Typ)); | |
848 | while Present (Iface_Elmt) loop | |
849 | if Is_Ghost_Entity (Node (Iface_Elmt)) then | |
850 | return True; | |
851 | end if; | |
852 | ||
853 | Next_Elmt (Iface_Elmt); | |
854 | end loop; | |
855 | end if; | |
856 | ||
857 | return False; | |
858 | end Implements_Ghost_Interface; | |
859 | ||
860 | ---------------- | |
861 | -- Initialize -- | |
862 | ---------------- | |
863 | ||
864 | procedure Initialize is | |
865 | begin | |
866 | Ignored_Ghost_Units.Init; | |
867 | end Initialize; | |
868 | ||
d65a80fd HK |
869 | ------------------------ |
870 | -- Install_Ghost_Mode -- | |
871 | ------------------------ | |
872 | ||
873 | procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is | |
874 | begin | |
875 | Ghost_Mode := Mode; | |
876 | end Install_Ghost_Mode; | |
877 | ||
878 | procedure Install_Ghost_Mode (Mode : Name_Id) is | |
879 | begin | |
880 | if Mode = Name_Check then | |
881 | Ghost_Mode := Check; | |
882 | ||
883 | elsif Mode = Name_Ignore then | |
884 | Ghost_Mode := Ignore; | |
885 | ||
886 | elsif Mode = Name_None then | |
887 | Ghost_Mode := None; | |
888 | end if; | |
889 | end Install_Ghost_Mode; | |
890 | ||
891 | ------------------------- | |
892 | -- Is_Ghost_Assignment -- | |
893 | ------------------------- | |
894 | ||
895 | function Is_Ghost_Assignment (N : Node_Id) return Boolean is | |
896 | Id : Entity_Id; | |
897 | ||
898 | begin | |
899 | -- An assignment statement is Ghost when its target denotes a Ghost | |
900 | -- entity. | |
901 | ||
902 | if Nkind (N) = N_Assignment_Statement then | |
903 | Id := Ghost_Entity (Name (N)); | |
904 | ||
905 | return Present (Id) and then Is_Ghost_Entity (Id); | |
906 | end if; | |
907 | ||
908 | return False; | |
909 | end Is_Ghost_Assignment; | |
910 | ||
911 | -------------------------- | |
912 | -- Is_Ghost_Declaration -- | |
913 | -------------------------- | |
914 | ||
915 | function Is_Ghost_Declaration (N : Node_Id) return Boolean is | |
916 | Id : Entity_Id; | |
917 | ||
918 | begin | |
919 | -- A declaration is Ghost when it elaborates a Ghost entity or is | |
920 | -- subject to pragma Ghost. | |
921 | ||
922 | if Is_Declaration (N) then | |
923 | Id := Defining_Entity (N); | |
924 | ||
925 | return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N); | |
926 | end if; | |
927 | ||
928 | return False; | |
929 | end Is_Ghost_Declaration; | |
930 | ||
931 | --------------------- | |
932 | -- Is_Ghost_Pragma -- | |
933 | --------------------- | |
934 | ||
935 | function Is_Ghost_Pragma (N : Node_Id) return Boolean is | |
936 | begin | |
937 | return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N); | |
938 | end Is_Ghost_Pragma; | |
939 | ||
940 | ----------------------------- | |
941 | -- Is_Ghost_Procedure_Call -- | |
942 | ----------------------------- | |
943 | ||
944 | function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is | |
945 | Id : Entity_Id; | |
946 | ||
947 | begin | |
948 | -- A procedure call is Ghost when it invokes a Ghost procedure | |
949 | ||
950 | if Nkind (N) = N_Procedure_Call_Statement then | |
951 | Id := Ghost_Entity (Name (N)); | |
952 | ||
953 | return Present (Id) and then Is_Ghost_Entity (Id); | |
954 | end if; | |
955 | ||
956 | return False; | |
957 | end Is_Ghost_Procedure_Call; | |
958 | ||
dafe11cd HK |
959 | --------------------------- |
960 | -- Is_Ignored_Ghost_Unit -- | |
961 | --------------------------- | |
962 | ||
963 | function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is | |
964 | begin | |
965 | -- Inspect the original node of the unit in case removal of ignored | |
966 | -- Ghost code has already taken place. | |
967 | ||
968 | return | |
969 | Nkind (N) = N_Compilation_Unit | |
970 | and then Is_Ignored_Ghost_Entity | |
971 | (Defining_Entity (Original_Node (Unit (N)))); | |
972 | end Is_Ignored_Ghost_Unit; | |
973 | ||
8636f52f HK |
974 | ------------------------- |
975 | -- Is_Subject_To_Ghost -- | |
976 | ------------------------- | |
977 | ||
978 | function Is_Subject_To_Ghost (N : Node_Id) return Boolean is | |
979 | function Enables_Ghostness (Arg : Node_Id) return Boolean; | |
980 | -- Determine whether aspect or pragma argument Arg enables "ghostness" | |
981 | ||
982 | ----------------------- | |
983 | -- Enables_Ghostness -- | |
984 | ----------------------- | |
985 | ||
986 | function Enables_Ghostness (Arg : Node_Id) return Boolean is | |
987 | Expr : Node_Id; | |
988 | ||
989 | begin | |
990 | Expr := Arg; | |
991 | ||
992 | if Nkind (Expr) = N_Pragma_Argument_Association then | |
993 | Expr := Get_Pragma_Arg (Expr); | |
994 | end if; | |
995 | ||
1af4455a HK |
996 | -- Determine whether the expression of the aspect or pragma is static |
997 | -- and denotes True. | |
8636f52f HK |
998 | |
999 | if Present (Expr) then | |
1000 | Preanalyze_And_Resolve (Expr); | |
1001 | ||
1002 | return | |
1003 | Is_OK_Static_Expression (Expr) | |
1004 | and then Is_True (Expr_Value (Expr)); | |
1005 | ||
1006 | -- Otherwise Ghost defaults to True | |
1007 | ||
1008 | else | |
1009 | return True; | |
1010 | end if; | |
1011 | end Enables_Ghostness; | |
1012 | ||
1013 | -- Local variables | |
1014 | ||
1015 | Id : constant Entity_Id := Defining_Entity (N); | |
1016 | Asp : Node_Id; | |
1017 | Decl : Node_Id; | |
1018 | Prev_Id : Entity_Id; | |
1019 | ||
1020 | -- Start of processing for Is_Subject_To_Ghost | |
1021 | ||
1022 | begin | |
1023 | -- The related entity of the declaration has not been analyzed yet, do | |
1024 | -- not inspect its attributes. | |
1025 | ||
1026 | if Ekind (Id) = E_Void then | |
1027 | null; | |
1028 | ||
1029 | elsif Is_Ghost_Entity (Id) then | |
1030 | return True; | |
1031 | ||
1032 | -- The completion of a type or a constant is not fully analyzed when the | |
1033 | -- reference to the Ghost entity is resolved. Because the completion is | |
1034 | -- not marked as Ghost yet, inspect the partial view. | |
1035 | ||
1036 | elsif Is_Record_Type (Id) | |
1037 | or else Ekind (Id) = E_Constant | |
1038 | or else (Nkind (N) = N_Object_Declaration | |
1039 | and then Constant_Present (N)) | |
1040 | then | |
1041 | Prev_Id := Incomplete_Or_Partial_View (Id); | |
1042 | ||
1043 | if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then | |
1044 | return True; | |
1045 | end if; | |
1046 | end if; | |
1047 | ||
1048 | -- Examine the aspect specifications (if any) looking for aspect Ghost | |
1049 | ||
1050 | if Permits_Aspect_Specifications (N) then | |
1051 | Asp := First (Aspect_Specifications (N)); | |
1052 | while Present (Asp) loop | |
1053 | if Chars (Identifier (Asp)) = Name_Ghost then | |
1054 | return Enables_Ghostness (Expression (Asp)); | |
1055 | end if; | |
1056 | ||
1057 | Next (Asp); | |
1058 | end loop; | |
1059 | end if; | |
1060 | ||
1061 | Decl := Empty; | |
1062 | ||
1063 | -- When the context is a [generic] package declaration, pragma Ghost | |
1064 | -- resides in the visible declarations. | |
1065 | ||
1066 | if Nkind_In (N, N_Generic_Package_Declaration, | |
1067 | N_Package_Declaration) | |
1068 | then | |
1069 | Decl := First (Visible_Declarations (Specification (N))); | |
1070 | ||
1071 | -- When the context is a package or a subprogram body, pragma Ghost | |
1072 | -- resides in the declarative part. | |
1073 | ||
1074 | elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then | |
1075 | Decl := First (Declarations (N)); | |
1076 | ||
1077 | -- Otherwise pragma Ghost appears in the declarations following N | |
1078 | ||
1079 | elsif Is_List_Member (N) then | |
1080 | Decl := Next (N); | |
1081 | end if; | |
1082 | ||
1083 | while Present (Decl) loop | |
1084 | if Nkind (Decl) = N_Pragma | |
6e759c2a | 1085 | and then Pragma_Name (Decl) = Name_Ghost |
8636f52f HK |
1086 | then |
1087 | return | |
1088 | Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); | |
1089 | ||
1090 | -- A source construct ends the region where pragma Ghost may appear, | |
2700b9c1 AC |
1091 | -- stop the traversal. Check the original node as source constructs |
1092 | -- may be rewritten into something else by expansion. | |
8636f52f | 1093 | |
2700b9c1 | 1094 | elsif Comes_From_Source (Original_Node (Decl)) then |
8636f52f HK |
1095 | exit; |
1096 | end if; | |
1097 | ||
1098 | Next (Decl); | |
1099 | end loop; | |
1100 | ||
1101 | return False; | |
1102 | end Is_Subject_To_Ghost; | |
1103 | ||
1104 | ---------- | |
1105 | -- Lock -- | |
1106 | ---------- | |
1107 | ||
1108 | procedure Lock is | |
1109 | begin | |
8636f52f | 1110 | Ignored_Ghost_Units.Release; |
de33eb38 | 1111 | Ignored_Ghost_Units.Locked := True; |
8636f52f HK |
1112 | end Lock; |
1113 | ||
d65a80fd HK |
1114 | ----------------------------------- |
1115 | -- Mark_And_Set_Ghost_Assignment -- | |
1116 | ----------------------------------- | |
1117 | ||
f9a8f910 | 1118 | procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is |
d65a80fd HK |
1119 | Id : Entity_Id; |
1120 | ||
1121 | begin | |
d65a80fd HK |
1122 | -- An assignment statement becomes Ghost when its target denotes a Ghost |
1123 | -- object. Install the Ghost mode of the target. | |
1124 | ||
1125 | Id := Ghost_Entity (Name (N)); | |
1126 | ||
1127 | if Present (Id) then | |
1128 | if Is_Checked_Ghost_Entity (Id) then | |
1129 | Install_Ghost_Mode (Check); | |
1130 | ||
1131 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1132 | Install_Ghost_Mode (Ignore); | |
1133 | ||
1134 | Set_Is_Ignored_Ghost_Node (N); | |
1135 | Propagate_Ignored_Ghost_Code (N); | |
1136 | end if; | |
1137 | end if; | |
1138 | end Mark_And_Set_Ghost_Assignment; | |
1139 | ||
241ebe89 | 1140 | ----------------------------- |
d65a80fd | 1141 | -- Mark_And_Set_Ghost_Body -- |
241ebe89 HK |
1142 | ----------------------------- |
1143 | ||
d65a80fd HK |
1144 | procedure Mark_And_Set_Ghost_Body |
1145 | (N : Node_Id; | |
f9a8f910 | 1146 | Spec_Id : Entity_Id) |
241ebe89 | 1147 | is |
d65a80fd HK |
1148 | Body_Id : constant Entity_Id := Defining_Entity (N); |
1149 | Policy : Name_Id := No_Name; | |
241ebe89 HK |
1150 | |
1151 | begin | |
d65a80fd | 1152 | -- A body becomes Ghost when it is subject to aspect or pragma Ghost |
241ebe89 | 1153 | |
d65a80fd HK |
1154 | if Is_Subject_To_Ghost (N) then |
1155 | Policy := Policy_In_Effect (Name_Ghost); | |
1156 | ||
1157 | -- A body declared within a Ghost region is automatically Ghost | |
1158 | -- (SPARK RM 6.9(2)). | |
1159 | ||
1160 | elsif Ghost_Mode = Check then | |
1161 | Policy := Name_Check; | |
1162 | ||
1163 | elsif Ghost_Mode = Ignore then | |
1164 | Policy := Name_Ignore; | |
1165 | ||
1166 | -- Inherit the "ghostness" of the previous declaration when the body | |
1167 | -- acts as a completion. | |
1168 | ||
1169 | elsif Present (Spec_Id) then | |
1170 | if Is_Checked_Ghost_Entity (Spec_Id) then | |
1171 | Policy := Name_Check; | |
1172 | ||
1173 | elsif Is_Ignored_Ghost_Entity (Spec_Id) then | |
1174 | Policy := Name_Ignore; | |
1175 | end if; | |
241ebe89 | 1176 | end if; |
241ebe89 | 1177 | |
d65a80fd HK |
1178 | -- The Ghost policy in effect at the point of declaration and at the |
1179 | -- point of completion must match (SPARK RM 6.9(14)). | |
1180 | ||
1181 | Check_Ghost_Completion | |
1182 | (Prev_Id => Spec_Id, | |
1183 | Compl_Id => Body_Id); | |
1184 | ||
1185 | -- Mark the body as its formals as Ghost | |
1186 | ||
1187 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1188 | ||
1189 | -- Install the appropriate Ghost mode | |
1190 | ||
1191 | Install_Ghost_Mode (Policy); | |
1192 | end Mark_And_Set_Ghost_Body; | |
1193 | ||
1194 | ----------------------------------- | |
1195 | -- Mark_And_Set_Ghost_Completion -- | |
1196 | ----------------------------------- | |
241ebe89 | 1197 | |
d65a80fd HK |
1198 | procedure Mark_And_Set_Ghost_Completion |
1199 | (N : Node_Id; | |
f9a8f910 | 1200 | Prev_Id : Entity_Id) |
241ebe89 | 1201 | is |
d65a80fd HK |
1202 | Compl_Id : constant Entity_Id := Defining_Entity (N); |
1203 | Policy : Name_Id := No_Name; | |
1204 | ||
241ebe89 | 1205 | begin |
d65a80fd HK |
1206 | -- A completion elaborated in a Ghost region is automatically Ghost |
1207 | -- (SPARK RM 6.9(2)). | |
1208 | ||
1209 | if Ghost_Mode = Check then | |
1210 | Policy := Name_Check; | |
1211 | ||
1212 | elsif Ghost_Mode = Ignore then | |
1213 | Policy := Name_Ignore; | |
1214 | ||
1215 | -- The completion becomes Ghost when its initial declaration is also | |
1216 | -- Ghost. | |
1217 | ||
1218 | elsif Is_Checked_Ghost_Entity (Prev_Id) then | |
1219 | Policy := Name_Check; | |
241ebe89 | 1220 | |
d65a80fd HK |
1221 | elsif Is_Ignored_Ghost_Entity (Prev_Id) then |
1222 | Policy := Name_Ignore; | |
241ebe89 | 1223 | end if; |
241ebe89 | 1224 | |
d65a80fd HK |
1225 | -- The Ghost policy in effect at the point of declaration and at the |
1226 | -- point of completion must match (SPARK RM 6.9(14)). | |
1227 | ||
1228 | Check_Ghost_Completion | |
1229 | (Prev_Id => Prev_Id, | |
1230 | Compl_Id => Compl_Id); | |
1231 | ||
1232 | -- Mark the completion as Ghost | |
1233 | ||
1234 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1235 | ||
1236 | -- Install the appropriate Ghost mode | |
1237 | ||
1238 | Install_Ghost_Mode (Policy); | |
1239 | end Mark_And_Set_Ghost_Completion; | |
241ebe89 | 1240 | |
d65a80fd HK |
1241 | ------------------------------------ |
1242 | -- Mark_And_Set_Ghost_Declaration -- | |
1243 | ------------------------------------ | |
1244 | ||
f9a8f910 | 1245 | procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is |
d65a80fd HK |
1246 | Par_Id : Entity_Id; |
1247 | Policy : Name_Id := No_Name; | |
241ebe89 HK |
1248 | |
1249 | begin | |
d65a80fd HK |
1250 | -- A declaration becomes Ghost when it is subject to aspect or pragma |
1251 | -- Ghost. | |
1252 | ||
1253 | if Is_Subject_To_Ghost (N) then | |
1254 | Policy := Policy_In_Effect (Name_Ghost); | |
1255 | ||
1256 | -- A declaration elaborated in a Ghost region is automatically Ghost | |
1257 | -- (SPARK RM 6.9(2)). | |
1258 | ||
1259 | elsif Ghost_Mode = Check then | |
1260 | Policy := Name_Check; | |
1261 | ||
1262 | elsif Ghost_Mode = Ignore then | |
1263 | Policy := Name_Ignore; | |
1264 | ||
1265 | -- A child package or subprogram declaration becomes Ghost when its | |
1266 | -- parent is Ghost (SPARK RM 6.9(2)). | |
241ebe89 | 1267 | |
d65a80fd HK |
1268 | elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration, |
1269 | N_Generic_Package_Declaration, | |
1270 | N_Generic_Package_Renaming_Declaration, | |
1271 | N_Generic_Procedure_Renaming_Declaration, | |
1272 | N_Generic_Subprogram_Declaration, | |
1273 | N_Package_Declaration, | |
1274 | N_Package_Renaming_Declaration, | |
1275 | N_Subprogram_Declaration, | |
1276 | N_Subprogram_Renaming_Declaration) | |
1277 | and then Present (Parent_Spec (N)) | |
1278 | then | |
1279 | Par_Id := Defining_Entity (Unit (Parent_Spec (N))); | |
1280 | ||
1281 | if Is_Checked_Ghost_Entity (Par_Id) then | |
1282 | Policy := Name_Check; | |
1283 | ||
1284 | elsif Is_Ignored_Ghost_Entity (Par_Id) then | |
1285 | Policy := Name_Ignore; | |
1286 | end if; | |
1287 | end if; | |
1288 | ||
1289 | -- Mark the declaration and its formals as Ghost | |
1290 | ||
1291 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1292 | ||
1293 | -- Install the appropriate Ghost mode | |
1294 | ||
1295 | Install_Ghost_Mode (Policy); | |
1296 | end Mark_And_Set_Ghost_Declaration; | |
1297 | ||
1298 | -------------------------------------- | |
1299 | -- Mark_And_Set_Ghost_Instantiation -- | |
1300 | -------------------------------------- | |
1301 | ||
1302 | procedure Mark_And_Set_Ghost_Instantiation | |
1303 | (N : Node_Id; | |
f9a8f910 | 1304 | Gen_Id : Entity_Id) |
d65a80fd HK |
1305 | is |
1306 | Policy : Name_Id := No_Name; | |
1307 | ||
1308 | begin | |
d65a80fd HK |
1309 | -- An instantiation becomes Ghost when it is subject to pragma Ghost |
1310 | ||
1311 | if Is_Subject_To_Ghost (N) then | |
1312 | Policy := Policy_In_Effect (Name_Ghost); | |
1313 | ||
1314 | -- An instantiation declaration within a Ghost region is automatically | |
1315 | -- Ghost (SPARK RM 6.9(2)). | |
1316 | ||
1317 | elsif Ghost_Mode = Check then | |
1318 | Policy := Name_Check; | |
1319 | ||
1320 | elsif Ghost_Mode = Ignore then | |
1321 | Policy := Name_Ignore; | |
1322 | ||
1323 | -- Inherit the "ghostness" of the generic unit | |
1324 | ||
1325 | elsif Is_Checked_Ghost_Entity (Gen_Id) then | |
1326 | Policy := Name_Check; | |
1327 | ||
1328 | elsif Is_Ignored_Ghost_Entity (Gen_Id) then | |
1329 | Policy := Name_Ignore; | |
1330 | end if; | |
1331 | ||
1332 | -- Mark the instantiation as Ghost | |
1333 | ||
1334 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1335 | ||
1336 | -- Install the appropriate Ghost mode | |
1337 | ||
1338 | Install_Ghost_Mode (Policy); | |
1339 | end Mark_And_Set_Ghost_Instantiation; | |
1340 | ||
1341 | --------------------------------------- | |
1342 | -- Mark_And_Set_Ghost_Procedure_Call -- | |
1343 | --------------------------------------- | |
1344 | ||
f9a8f910 | 1345 | procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is |
d65a80fd HK |
1346 | Id : Entity_Id; |
1347 | ||
1348 | begin | |
d65a80fd HK |
1349 | -- A procedure call becomes Ghost when the procedure being invoked is |
1350 | -- Ghost. Install the Ghost mode of the procedure. | |
1351 | ||
1352 | Id := Ghost_Entity (Name (N)); | |
1353 | ||
1354 | if Present (Id) then | |
1355 | if Is_Checked_Ghost_Entity (Id) then | |
1356 | Install_Ghost_Mode (Check); | |
1357 | ||
1358 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1359 | Install_Ghost_Mode (Ignore); | |
1360 | ||
1361 | Set_Is_Ignored_Ghost_Node (N); | |
1362 | Propagate_Ignored_Ghost_Code (N); | |
1363 | end if; | |
1364 | end if; | |
1365 | end Mark_And_Set_Ghost_Procedure_Call; | |
1366 | ||
1367 | ------------------------------------ | |
1368 | -- Mark_Ghost_Declaration_Or_Body -- | |
1369 | ------------------------------------ | |
1370 | ||
1371 | procedure Mark_Ghost_Declaration_Or_Body | |
1372 | (N : Node_Id; | |
1373 | Mode : Name_Id) | |
1374 | is | |
1375 | Id : constant Entity_Id := Defining_Entity (N); | |
1376 | ||
1377 | Mark_Formals : Boolean := False; | |
1378 | Param : Node_Id; | |
1379 | Param_Id : Entity_Id; | |
1380 | ||
1381 | begin | |
1382 | -- Mark the related node and its entity | |
1383 | ||
1384 | if Mode = Name_Check then | |
1385 | Mark_Formals := True; | |
1386 | Set_Is_Checked_Ghost_Entity (Id); | |
1387 | ||
1388 | elsif Mode = Name_Ignore then | |
1389 | Mark_Formals := True; | |
1390 | Set_Is_Ignored_Ghost_Entity (Id); | |
1391 | Set_Is_Ignored_Ghost_Node (N); | |
1392 | Propagate_Ignored_Ghost_Code (N); | |
1393 | end if; | |
1394 | ||
1395 | -- Mark all formal parameters when the related node denotes a subprogram | |
1396 | -- or a body. The traversal is performed via the specification because | |
1397 | -- the related subprogram or body may be unanalyzed. | |
1398 | ||
1399 | -- ??? could extra formal parameters cause a Ghost leak? | |
1400 | ||
1401 | if Mark_Formals | |
1402 | and then Nkind_In (N, N_Abstract_Subprogram_Declaration, | |
1403 | N_Formal_Abstract_Subprogram_Declaration, | |
1404 | N_Formal_Concrete_Subprogram_Declaration, | |
1405 | N_Generic_Subprogram_Declaration, | |
1406 | N_Subprogram_Body, | |
1407 | N_Subprogram_Body_Stub, | |
1408 | N_Subprogram_Declaration, | |
1409 | N_Subprogram_Renaming_Declaration) | |
1410 | then | |
1411 | Param := First (Parameter_Specifications (Specification (N))); | |
1412 | while Present (Param) loop | |
1413 | Param_Id := Defining_Entity (Param); | |
1414 | ||
1415 | if Mode = Name_Check then | |
1416 | Set_Is_Checked_Ghost_Entity (Param_Id); | |
1417 | ||
1418 | elsif Mode = Name_Ignore then | |
1419 | Set_Is_Ignored_Ghost_Entity (Param_Id); | |
1420 | end if; | |
1421 | ||
1422 | Next (Param); | |
1423 | end loop; | |
1424 | end if; | |
1425 | end Mark_Ghost_Declaration_Or_Body; | |
1426 | ||
6e9e35e1 AC |
1427 | ----------------------- |
1428 | -- Mark_Ghost_Clause -- | |
1429 | ----------------------- | |
1430 | ||
1431 | procedure Mark_Ghost_Clause (N : Node_Id) is | |
1432 | Nam : Node_Id := Empty; | |
1433 | ||
1434 | begin | |
1435 | if Nkind (N) = N_Use_Package_Clause then | |
1436 | Nam := First (Names (N)); | |
1437 | ||
1438 | elsif Nkind (N) = N_Use_Type_Clause then | |
1439 | Nam := First (Subtype_Marks (N)); | |
1440 | ||
1441 | elsif Nkind (N) = N_With_Clause then | |
1442 | Nam := Name (N); | |
1443 | end if; | |
1444 | ||
1445 | if Present (Nam) | |
1446 | and then Is_Entity_Name (Nam) | |
1447 | and then Present (Entity (Nam)) | |
1448 | and then Is_Ignored_Ghost_Entity (Entity (Nam)) | |
1449 | then | |
1450 | Set_Is_Ignored_Ghost_Node (N); | |
1451 | Propagate_Ignored_Ghost_Code (N); | |
1452 | end if; | |
1453 | end Mark_Ghost_Clause; | |
1454 | ||
d65a80fd HK |
1455 | ----------------------- |
1456 | -- Mark_Ghost_Pragma -- | |
1457 | ----------------------- | |
1458 | ||
1459 | procedure Mark_Ghost_Pragma | |
1460 | (N : Node_Id; | |
1461 | Id : Entity_Id) | |
1462 | is | |
1463 | begin | |
1464 | -- A pragma becomes Ghost when it encloses a Ghost entity or relates to | |
1465 | -- a Ghost entity. | |
1466 | ||
1467 | if Is_Checked_Ghost_Entity (Id) then | |
1468 | Set_Is_Checked_Ghost_Pragma (N); | |
1469 | ||
1470 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1471 | Set_Is_Ignored_Ghost_Pragma (N); | |
1472 | Set_Is_Ignored_Ghost_Node (N); | |
1473 | Propagate_Ignored_Ghost_Code (N); | |
1474 | end if; | |
1475 | end Mark_Ghost_Pragma; | |
1476 | ||
1477 | ------------------------- | |
1478 | -- Mark_Ghost_Renaming -- | |
1479 | ------------------------- | |
1480 | ||
1481 | procedure Mark_Ghost_Renaming | |
1482 | (N : Node_Id; | |
1483 | Id : Entity_Id) | |
1484 | is | |
1485 | Policy : Name_Id := No_Name; | |
1486 | ||
1487 | begin | |
1488 | -- A renaming becomes Ghost when it renames a Ghost entity | |
1489 | ||
1490 | if Is_Checked_Ghost_Entity (Id) then | |
1491 | Policy := Name_Check; | |
1492 | ||
1493 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1494 | Policy := Name_Ignore; | |
241ebe89 | 1495 | end if; |
d65a80fd HK |
1496 | |
1497 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1498 | end Mark_Ghost_Renaming; | |
241ebe89 | 1499 | |
8636f52f HK |
1500 | ---------------------------------- |
1501 | -- Propagate_Ignored_Ghost_Code -- | |
1502 | ---------------------------------- | |
1503 | ||
1504 | procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is | |
1505 | Nod : Node_Id; | |
1506 | Scop : Entity_Id; | |
1507 | ||
1508 | begin | |
d65a80fd | 1509 | -- Traverse the parent chain looking for blocks, packages, and |
8636f52f HK |
1510 | -- subprograms or their respective bodies. |
1511 | ||
1512 | Nod := Parent (N); | |
1513 | while Present (Nod) loop | |
1514 | Scop := Empty; | |
1515 | ||
7c323fbe AC |
1516 | if Nkind (Nod) = N_Block_Statement |
1517 | and then Present (Identifier (Nod)) | |
1518 | then | |
8636f52f HK |
1519 | Scop := Entity (Identifier (Nod)); |
1520 | ||
1521 | elsif Nkind_In (Nod, N_Package_Body, | |
1522 | N_Package_Declaration, | |
1523 | N_Subprogram_Body, | |
1524 | N_Subprogram_Declaration) | |
1525 | then | |
1526 | Scop := Defining_Entity (Nod); | |
1527 | end if; | |
1528 | ||
1529 | -- The current node denotes a scoping construct | |
1530 | ||
1531 | if Present (Scop) then | |
1532 | ||
1533 | -- Stop the traversal when the scope already contains ignored | |
1534 | -- Ghost code as all enclosing scopes have already been marked. | |
1535 | ||
1536 | if Contains_Ignored_Ghost_Code (Scop) then | |
1537 | exit; | |
1538 | ||
1539 | -- Otherwise mark this scope and keep climbing | |
1540 | ||
1541 | else | |
1542 | Set_Contains_Ignored_Ghost_Code (Scop); | |
1543 | end if; | |
1544 | end if; | |
1545 | ||
1546 | Nod := Parent (Nod); | |
1547 | end loop; | |
1548 | ||
1549 | -- The unit containing the ignored Ghost code must be post processed | |
1550 | -- before invoking the back end. | |
1551 | ||
1552 | Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N))); | |
1553 | end Propagate_Ignored_Ghost_Code; | |
1554 | ||
1555 | ------------------------------- | |
1556 | -- Remove_Ignored_Ghost_Code -- | |
1557 | ------------------------------- | |
1558 | ||
1559 | procedure Remove_Ignored_Ghost_Code is | |
1560 | procedure Prune_Tree (Root : Node_Id); | |
1561 | -- Remove all code marked as ignored Ghost from the tree of denoted by | |
1562 | -- Root. | |
1563 | ||
1564 | ---------------- | |
1565 | -- Prune_Tree -- | |
1566 | ---------------- | |
1567 | ||
1568 | procedure Prune_Tree (Root : Node_Id) is | |
1569 | procedure Prune (N : Node_Id); | |
1570 | -- Remove a given node from the tree by rewriting it into null | |
1571 | ||
1572 | function Prune_Node (N : Node_Id) return Traverse_Result; | |
1573 | -- Determine whether node N denotes an ignored Ghost construct. If | |
1574 | -- this is the case, rewrite N as a null statement. See the body for | |
1575 | -- special cases. | |
1576 | ||
1577 | ----------- | |
1578 | -- Prune -- | |
1579 | ----------- | |
1580 | ||
1581 | procedure Prune (N : Node_Id) is | |
1582 | begin | |
1583 | -- Destroy any aspects that may be associated with the node | |
1584 | ||
1585 | if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then | |
1586 | Remove_Aspects (N); | |
1587 | end if; | |
1588 | ||
1589 | Rewrite (N, Make_Null_Statement (Sloc (N))); | |
1590 | end Prune; | |
1591 | ||
1592 | ---------------- | |
1593 | -- Prune_Node -- | |
1594 | ---------------- | |
1595 | ||
1596 | function Prune_Node (N : Node_Id) return Traverse_Result is | |
1597 | Id : Entity_Id; | |
1598 | ||
1599 | begin | |
6e9e35e1 | 1600 | -- Do not prune compilation unit nodes because many mechanisms |
dafe11cd HK |
1601 | -- depend on their presence. Note that context items are still |
1602 | -- being processed. | |
6e9e35e1 AC |
1603 | |
1604 | if Nkind (N) = N_Compilation_Unit then | |
1605 | return OK; | |
1606 | ||
8636f52f HK |
1607 | -- The node is either declared as ignored Ghost or is a byproduct |
1608 | -- of expansion. Destroy it and stop the traversal on this branch. | |
1609 | ||
6e9e35e1 | 1610 | elsif Is_Ignored_Ghost_Node (N) then |
8636f52f HK |
1611 | Prune (N); |
1612 | return Skip; | |
1613 | ||
1614 | -- Scoping constructs such as blocks, packages, subprograms and | |
1615 | -- bodies offer some flexibility with respect to pruning. | |
1616 | ||
1617 | elsif Nkind_In (N, N_Block_Statement, | |
1618 | N_Package_Body, | |
1619 | N_Package_Declaration, | |
1620 | N_Subprogram_Body, | |
1621 | N_Subprogram_Declaration) | |
1622 | then | |
1623 | if Nkind (N) = N_Block_Statement then | |
1624 | Id := Entity (Identifier (N)); | |
1625 | else | |
1626 | Id := Defining_Entity (N); | |
1627 | end if; | |
1628 | ||
1629 | -- The scoping construct contains both living and ignored Ghost | |
1630 | -- code, let the traversal prune all relevant nodes. | |
1631 | ||
1632 | if Contains_Ignored_Ghost_Code (Id) then | |
1633 | return OK; | |
1634 | ||
1635 | -- Otherwise the construct contains only living code and should | |
1636 | -- not be pruned. | |
1637 | ||
1638 | else | |
1639 | return Skip; | |
1640 | end if; | |
1641 | ||
1642 | -- Otherwise keep searching for ignored Ghost nodes | |
1643 | ||
1644 | else | |
1645 | return OK; | |
1646 | end if; | |
1647 | end Prune_Node; | |
1648 | ||
1649 | procedure Prune_Nodes is new Traverse_Proc (Prune_Node); | |
1650 | ||
1651 | -- Start of processing for Prune_Tree | |
1652 | ||
1653 | begin | |
1654 | Prune_Nodes (Root); | |
1655 | end Prune_Tree; | |
1656 | ||
1657 | -- Start of processing for Remove_Ignored_Ghost_Code | |
1658 | ||
1659 | begin | |
1660 | for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop | |
6e9e35e1 | 1661 | Prune_Tree (Ignored_Ghost_Units.Table (Index)); |
8636f52f HK |
1662 | end loop; |
1663 | end Remove_Ignored_Ghost_Code; | |
1664 | ||
d65a80fd HK |
1665 | ------------------------ |
1666 | -- Restore_Ghost_Mode -- | |
1667 | ------------------------ | |
1668 | ||
1669 | procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is | |
1670 | begin | |
1671 | Ghost_Mode := Mode; | |
1672 | end Restore_Ghost_Mode; | |
1673 | ||
8636f52f HK |
1674 | -------------------- |
1675 | -- Set_Ghost_Mode -- | |
1676 | -------------------- | |
1677 | ||
f9a8f910 | 1678 | procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is |
d65a80fd HK |
1679 | procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); |
1680 | -- Install the Ghost mode of entity Id | |
8636f52f | 1681 | |
d65a80fd HK |
1682 | -------------------------------- |
1683 | -- Set_Ghost_Mode_From_Entity -- | |
1684 | -------------------------------- | |
8636f52f | 1685 | |
d65a80fd | 1686 | procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is |
8636f52f | 1687 | begin |
d65a80fd HK |
1688 | if Is_Checked_Ghost_Entity (Id) then |
1689 | Install_Ghost_Mode (Check); | |
1690 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1691 | Install_Ghost_Mode (Ignore); | |
1692 | else | |
1693 | Install_Ghost_Mode (None); | |
8636f52f | 1694 | end if; |
d65a80fd | 1695 | end Set_Ghost_Mode_From_Entity; |
8636f52f HK |
1696 | |
1697 | -- Local variables | |
1698 | ||
d65a80fd | 1699 | Id : Entity_Id; |
8636f52f HK |
1700 | |
1701 | -- Start of processing for Set_Ghost_Mode | |
1702 | ||
1703 | begin | |
d65a80fd HK |
1704 | -- The Ghost mode of an assignment statement depends on the Ghost mode |
1705 | -- of the target. | |
8636f52f | 1706 | |
d65a80fd HK |
1707 | if Nkind (N) = N_Assignment_Statement then |
1708 | Id := Ghost_Entity (Name (N)); | |
8636f52f | 1709 | |
d65a80fd HK |
1710 | if Present (Id) then |
1711 | Set_Ghost_Mode_From_Entity (Id); | |
8636f52f HK |
1712 | end if; |
1713 | ||
d65a80fd HK |
1714 | -- The Ghost mode of a body or a declaration depends on the Ghost mode |
1715 | -- of its defining entity. | |
8636f52f | 1716 | |
d65a80fd HK |
1717 | elsif Is_Body (N) or else Is_Declaration (N) then |
1718 | Set_Ghost_Mode_From_Entity (Defining_Entity (N)); | |
8636f52f | 1719 | |
d65a80fd | 1720 | -- The Ghost mode of an entity depends on the entity itself |
8636f52f | 1721 | |
d65a80fd HK |
1722 | elsif Nkind (N) in N_Entity then |
1723 | Set_Ghost_Mode_From_Entity (N); | |
8636f52f | 1724 | |
d65a80fd HK |
1725 | -- The Ghost mode of a [generic] freeze node depends on the Ghost mode |
1726 | -- of the entity being frozen. | |
1727 | ||
1728 | elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then | |
1729 | Set_Ghost_Mode_From_Entity (Entity (N)); | |
241ebe89 | 1730 | |
d65a80fd HK |
1731 | -- The Ghost mode of a pragma depends on the associated entity. The |
1732 | -- property is encoded in the pragma itself. | |
241ebe89 | 1733 | |
d65a80fd HK |
1734 | elsif Nkind (N) = N_Pragma then |
1735 | if Is_Checked_Ghost_Pragma (N) then | |
1736 | Install_Ghost_Mode (Check); | |
1737 | elsif Is_Ignored_Ghost_Pragma (N) then | |
1738 | Install_Ghost_Mode (Ignore); | |
241ebe89 | 1739 | else |
d65a80fd | 1740 | Install_Ghost_Mode (None); |
8636f52f | 1741 | end if; |
241ebe89 | 1742 | |
d65a80fd HK |
1743 | -- The Ghost mode of a procedure call depends on the Ghost mode of the |
1744 | -- procedure being invoked. | |
241ebe89 | 1745 | |
d65a80fd HK |
1746 | elsif Nkind (N) = N_Procedure_Call_Statement then |
1747 | Id := Ghost_Entity (Name (N)); | |
8636f52f | 1748 | |
d65a80fd HK |
1749 | if Present (Id) then |
1750 | Set_Ghost_Mode_From_Entity (Id); | |
1751 | end if; | |
8636f52f | 1752 | end if; |
d65a80fd | 1753 | end Set_Ghost_Mode; |
8636f52f HK |
1754 | |
1755 | ------------------------- | |
1756 | -- Set_Is_Ghost_Entity -- | |
1757 | ------------------------- | |
1758 | ||
1759 | procedure Set_Is_Ghost_Entity (Id : Entity_Id) is | |
1760 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); | |
8636f52f HK |
1761 | begin |
1762 | if Policy = Name_Check then | |
1763 | Set_Is_Checked_Ghost_Entity (Id); | |
8636f52f HK |
1764 | elsif Policy = Name_Ignore then |
1765 | Set_Is_Ignored_Ghost_Entity (Id); | |
1766 | end if; | |
1767 | end Set_Is_Ghost_Entity; | |
1768 | ||
1769 | end Ghost; |