]>
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 | -- -- | |
1d005acc | 9 | -- Copyright (C) 2014-2019, 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 | ||
851e9f19 | 26 | with Alloc; |
8636f52f HK |
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; | |
8636f52f HK |
32 | with Namet; use Namet; |
33 | with Nlists; use Nlists; | |
34 | with Nmake; use Nmake; | |
8636f52f HK |
35 | with Sem; use Sem; |
36 | with Sem_Aux; use Sem_Aux; | |
b3b3ada9 | 37 | with Sem_Ch8; use Sem_Ch8; |
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 | ||
9057bd6a HK |
49 | --------------------- |
50 | -- Data strictures -- | |
51 | --------------------- | |
52 | ||
980f94b7 HK |
53 | -- The following table contains all ignored Ghost nodes that must be |
54 | -- eliminated from the tree by routine Remove_Ignored_Ghost_Code. | |
8636f52f | 55 | |
980f94b7 | 56 | package Ignored_Ghost_Nodes is new Table.Table ( |
8636f52f HK |
57 | Table_Component_Type => Node_Id, |
58 | Table_Index_Type => Int, | |
59 | Table_Low_Bound => 0, | |
980f94b7 HK |
60 | Table_Initial => Alloc.Ignored_Ghost_Nodes_Initial, |
61 | Table_Increment => Alloc.Ignored_Ghost_Nodes_Increment, | |
62 | Table_Name => "Ignored_Ghost_Nodes"); | |
8636f52f HK |
63 | |
64 | ----------------------- | |
9057bd6a | 65 | -- Local subprograms -- |
8636f52f HK |
66 | ----------------------- |
67 | ||
b3b3ada9 HK |
68 | function Ghost_Entity (Ref : Node_Id) return Entity_Id; |
69 | pragma Inline (Ghost_Entity); | |
70 | -- Obtain the entity of a Ghost entity from reference Ref. Return Empty if | |
71 | -- no such entity exists. | |
d65a80fd | 72 | |
9057bd6a HK |
73 | procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); |
74 | pragma Inline (Install_Ghost_Mode); | |
75 | -- Install Ghost mode Mode as the Ghost mode in effect | |
76 | ||
77 | procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id); | |
78 | pragma Inline (Install_Ghost_Region); | |
79 | -- Install a Ghost region comprised of mode Mode and ignored region start | |
80 | -- node N. | |
241ebe89 | 81 | |
1af4455a | 82 | function Is_Subject_To_Ghost (N : Node_Id) return Boolean; |
d65a80fd HK |
83 | -- Determine whether declaration or body N is subject to aspect or pragma |
84 | -- Ghost. This routine must be used in cases where pragma Ghost has not | |
85 | -- been analyzed yet, but the context needs to establish the "ghostness" | |
86 | -- of N. | |
87 | ||
88 | procedure Mark_Ghost_Declaration_Or_Body | |
89 | (N : Node_Id; | |
90 | Mode : Name_Id); | |
91 | -- Mark the defining entity of declaration or body N as Ghost depending on | |
92 | -- mode Mode. Mark all formals parameters when N denotes a subprogram or a | |
93 | -- body. | |
1af4455a | 94 | |
9057bd6a HK |
95 | function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type; |
96 | pragma Inline (Name_To_Ghost_Mode); | |
97 | -- Convert a Ghost mode denoted by name Mode into its respective enumerated | |
98 | -- value. | |
99 | ||
980f94b7 HK |
100 | procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id); |
101 | -- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for | |
102 | -- later elimination. | |
8636f52f HK |
103 | |
104 | ---------------------------- | |
105 | -- Check_Ghost_Completion -- | |
106 | ---------------------------- | |
107 | ||
108 | procedure Check_Ghost_Completion | |
d65a80fd HK |
109 | (Prev_Id : Entity_Id; |
110 | Compl_Id : Entity_Id) | |
8636f52f HK |
111 | is |
112 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); | |
113 | ||
114 | begin | |
d65a80fd HK |
115 | -- Nothing to do if one of the views is missing |
116 | ||
117 | if No (Prev_Id) or else No (Compl_Id) then | |
118 | null; | |
119 | ||
8636f52f | 120 | -- The Ghost policy in effect at the point of declaration and at the |
c2cfccb1 | 121 | -- point of completion must match (SPARK RM 6.9(14)). |
8636f52f | 122 | |
d65a80fd | 123 | elsif Is_Checked_Ghost_Entity (Prev_Id) |
8636f52f HK |
124 | and then Policy = Name_Ignore |
125 | then | |
d65a80fd | 126 | Error_Msg_Sloc := Sloc (Compl_Id); |
8636f52f | 127 | |
d65a80fd HK |
128 | Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); |
129 | Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id); | |
130 | Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id); | |
8636f52f | 131 | |
d65a80fd | 132 | elsif Is_Ignored_Ghost_Entity (Prev_Id) |
8636f52f HK |
133 | and then Policy = Name_Check |
134 | then | |
d65a80fd | 135 | Error_Msg_Sloc := Sloc (Compl_Id); |
8636f52f | 136 | |
d65a80fd HK |
137 | Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); |
138 | Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id); | |
139 | Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id); | |
8636f52f HK |
140 | end if; |
141 | end Check_Ghost_Completion; | |
142 | ||
143 | ------------------------- | |
144 | -- Check_Ghost_Context -- | |
145 | ------------------------- | |
146 | ||
147 | procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is | |
ac8380d5 | 148 | procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id); |
8636f52f | 149 | -- Verify that the Ghost policy at the point of declaration of entity Id |
ac8380d5 AC |
150 | -- matches the policy at the point of reference Ref. If this is not the |
151 | -- case emit an error at Ref. | |
8636f52f HK |
152 | |
153 | function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; | |
154 | -- Determine whether node Context denotes a Ghost-friendly context where | |
4179af27 | 155 | -- a Ghost entity can safely reside (SPARK RM 6.9(10)). |
8636f52f HK |
156 | |
157 | ------------------------- | |
158 | -- Is_OK_Ghost_Context -- | |
159 | ------------------------- | |
160 | ||
161 | function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is | |
241ebe89 HK |
162 | function Is_OK_Declaration (Decl : Node_Id) return Boolean; |
163 | -- Determine whether node Decl is a suitable context for a reference | |
164 | -- to a Ghost entity. To qualify as such, Decl must either | |
d65a80fd HK |
165 | -- |
166 | -- * Define a Ghost entity | |
167 | -- | |
168 | -- * Be subject to pragma Ghost | |
241ebe89 HK |
169 | |
170 | function Is_OK_Pragma (Prag : Node_Id) return Boolean; | |
171 | -- Determine whether node Prag is a suitable context for a reference | |
172 | -- to a Ghost entity. To qualify as such, Prag must either | |
d65a80fd HK |
173 | -- |
174 | -- * Be an assertion expression pragma | |
175 | -- | |
176 | -- * Denote pragma Global, Depends, Initializes, Refined_Global, | |
177 | -- Refined_Depends or Refined_State. | |
178 | -- | |
179 | -- * Specify an aspect of a Ghost entity | |
180 | -- | |
181 | -- * Contain a reference to a Ghost entity | |
241ebe89 HK |
182 | |
183 | function Is_OK_Statement (Stmt : Node_Id) return Boolean; | |
184 | -- Determine whether node Stmt is a suitable context for a reference | |
185 | -- to a Ghost entity. To qualify as such, Stmt must either | |
d65a80fd HK |
186 | -- |
187 | -- * Denote a procedure call to a Ghost procedure | |
188 | -- | |
189 | -- * Denote an assignment statement whose target is Ghost | |
241ebe89 HK |
190 | |
191 | ----------------------- | |
192 | -- Is_OK_Declaration -- | |
193 | ----------------------- | |
194 | ||
195 | function Is_OK_Declaration (Decl : Node_Id) return Boolean is | |
6d0d18dc AC |
196 | function In_Subprogram_Body_Profile (N : Node_Id) return Boolean; |
197 | -- Determine whether node N appears in the profile of a subprogram | |
198 | -- body. | |
199 | ||
6d0d18dc AC |
200 | -------------------------------- |
201 | -- In_Subprogram_Body_Profile -- | |
202 | -------------------------------- | |
203 | ||
204 | function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is | |
205 | Spec : constant Node_Id := Parent (N); | |
206 | ||
207 | begin | |
208 | -- The node appears in a parameter specification in which case | |
209 | -- it is either the parameter type or the default expression or | |
210 | -- the node appears as the result definition of a function. | |
211 | ||
212 | return | |
213 | (Nkind (N) = N_Parameter_Specification | |
214 | or else | |
215 | (Nkind (Spec) = N_Function_Specification | |
216 | and then N = Result_Definition (Spec))) | |
217 | and then Nkind (Parent (Spec)) = N_Subprogram_Body; | |
218 | end In_Subprogram_Body_Profile; | |
219 | ||
241ebe89 HK |
220 | -- Local variables |
221 | ||
8636f52f HK |
222 | Subp_Decl : Node_Id; |
223 | Subp_Id : Entity_Id; | |
224 | ||
241ebe89 HK |
225 | -- Start of processing for Is_OK_Declaration |
226 | ||
8636f52f | 227 | begin |
d65a80fd HK |
228 | if Is_Ghost_Declaration (Decl) then |
229 | return True; | |
8636f52f | 230 | |
241ebe89 | 231 | -- Special cases |
8636f52f | 232 | |
6d0d18dc AC |
233 | -- A reference to a Ghost entity may appear within the profile of |
234 | -- a subprogram body. This context is treated as suitable because | |
235 | -- it duplicates the context of the corresponding spec. The real | |
236 | -- check was already performed during the analysis of the spec. | |
237 | ||
238 | elsif In_Subprogram_Body_Profile (Decl) then | |
239 | return True; | |
240 | ||
241 | -- A reference to a Ghost entity may appear within an expression | |
242 | -- function which is still being analyzed. This context is treated | |
243 | -- as suitable because it is not yet known whether the expression | |
244 | -- function is an initial declaration or a completion. The real | |
245 | -- check is performed when the expression function is expanded. | |
8636f52f | 246 | |
6d0d18dc AC |
247 | elsif Nkind (Decl) = N_Expression_Function |
248 | and then not Analyzed (Decl) | |
241ebe89 HK |
249 | then |
250 | return True; | |
8636f52f | 251 | |
241ebe89 HK |
252 | -- References to Ghost entities may be relocated in internally |
253 | -- generated bodies. | |
8636f52f | 254 | |
241ebe89 HK |
255 | elsif Nkind (Decl) = N_Subprogram_Body |
256 | and then not Comes_From_Source (Decl) | |
257 | then | |
258 | Subp_Id := Corresponding_Spec (Decl); | |
8636f52f | 259 | |
241ebe89 | 260 | if Present (Subp_Id) then |
241ebe89 | 261 | |
c37e6613 HK |
262 | -- The context is the internally built _Postconditions |
263 | -- procedure, which is OK because the real check was done | |
264 | -- before expansion activities. | |
7f5e1dee JM |
265 | |
266 | if Chars (Subp_Id) = Name_uPostconditions then | |
267 | return True; | |
268 | ||
1155ae01 AC |
269 | -- The context is the internally built predicate function, |
270 | -- which is OK because the real check was done before the | |
271 | -- predicate function was generated. | |
272 | ||
273 | elsif Is_Predicate_Function (Subp_Id) then | |
274 | return True; | |
275 | ||
7f5e1dee JM |
276 | else |
277 | Subp_Decl := | |
278 | Original_Node (Unit_Declaration_Node (Subp_Id)); | |
279 | ||
280 | -- The original context is an expression function that | |
281 | -- has been split into a spec and a body. The context is | |
282 | -- OK as long as the initial declaration is Ghost. | |
283 | ||
284 | if Nkind (Subp_Decl) = N_Expression_Function then | |
d65a80fd | 285 | return Is_Ghost_Declaration (Subp_Decl); |
7f5e1dee | 286 | end if; |
8636f52f HK |
287 | end if; |
288 | ||
241ebe89 HK |
289 | -- Otherwise this is either an internal body or an internal |
290 | -- completion. Both are OK because the real check was done | |
291 | -- before expansion activities. | |
8636f52f | 292 | |
241ebe89 | 293 | else |
8636f52f HK |
294 | return True; |
295 | end if; | |
241ebe89 | 296 | end if; |
8636f52f HK |
297 | |
298 | return False; | |
241ebe89 | 299 | end Is_OK_Declaration; |
8636f52f | 300 | |
241ebe89 HK |
301 | ------------------ |
302 | -- Is_OK_Pragma -- | |
303 | ------------------ | |
8636f52f | 304 | |
241ebe89 HK |
305 | function Is_OK_Pragma (Prag : Node_Id) return Boolean is |
306 | procedure Check_Policies (Prag_Nam : Name_Id); | |
307 | -- Verify that the Ghost policy in effect is the same as the | |
308 | -- assertion policy for pragma name Prag_Nam. Emit an error if | |
309 | -- this is not the case. | |
8636f52f | 310 | |
241ebe89 HK |
311 | -------------------- |
312 | -- Check_Policies -- | |
313 | -------------------- | |
8636f52f | 314 | |
241ebe89 HK |
315 | procedure Check_Policies (Prag_Nam : Name_Id) is |
316 | AP : constant Name_Id := Check_Kind (Prag_Nam); | |
317 | GP : constant Name_Id := Policy_In_Effect (Name_Ghost); | |
8636f52f HK |
318 | |
319 | begin | |
241ebe89 HK |
320 | -- If the Ghost policy in effect at the point of a Ghost entity |
321 | -- reference is Ignore, then the assertion policy of the pragma | |
322 | -- must be Ignore (SPARK RM 6.9(18)). | |
323 | ||
324 | if GP = Name_Ignore and then AP /= Name_Ignore then | |
325 | Error_Msg_N | |
ad4ba28b AC |
326 | ("incompatible ghost policies in effect", |
327 | Ghost_Ref); | |
241ebe89 HK |
328 | Error_Msg_NE |
329 | ("\ghost entity & has policy `Ignore`", | |
330 | Ghost_Ref, Ghost_Id); | |
331 | ||
332 | Error_Msg_Name_1 := AP; | |
333 | Error_Msg_N | |
334 | ("\assertion expression has policy %", Ghost_Ref); | |
335 | end if; | |
336 | end Check_Policies; | |
8636f52f HK |
337 | |
338 | -- Local variables | |
339 | ||
241ebe89 HK |
340 | Prag_Id : Pragma_Id; |
341 | Prag_Nam : Name_Id; | |
8636f52f | 342 | |
241ebe89 | 343 | -- Start of processing for Is_OK_Pragma |
8636f52f HK |
344 | |
345 | begin | |
241ebe89 HK |
346 | if Nkind (Prag) = N_Pragma then |
347 | Prag_Id := Get_Pragma_Id (Prag); | |
348 | Prag_Nam := Original_Aspect_Pragma_Name (Prag); | |
8636f52f | 349 | |
241ebe89 HK |
350 | -- A pragma that applies to a Ghost construct or specifies an |
351 | -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3)) | |
8636f52f | 352 | |
241ebe89 | 353 | if Is_Ghost_Pragma (Prag) then |
8636f52f | 354 | return True; |
8636f52f | 355 | |
95fef24f | 356 | -- An assertion expression pragma is Ghost when it contains a |
1155ae01 AC |
357 | -- reference to a Ghost entity (SPARK RM 6.9(10)), except for |
358 | -- predicate pragmas (SPARK RM 6.9(11)). | |
8636f52f | 359 | |
1155ae01 AC |
360 | elsif Assertion_Expression_Pragma (Prag_Id) |
361 | and then Prag_Id /= Pragma_Predicate | |
362 | then | |
4179af27 HK |
363 | -- Ensure that the assertion policy and the Ghost policy are |
364 | -- compatible (SPARK RM 6.9(18)). | |
8636f52f | 365 | |
4179af27 HK |
366 | Check_Policies (Prag_Nam); |
367 | return True; | |
8636f52f | 368 | |
241ebe89 HK |
369 | -- Several pragmas that may apply to a non-Ghost entity are |
370 | -- treated as Ghost when they contain a reference to a Ghost | |
4179af27 | 371 | -- entity (SPARK RM 6.9(11)). |
8636f52f | 372 | |
241ebe89 HK |
373 | elsif Nam_In (Prag_Nam, Name_Global, |
374 | Name_Depends, | |
375 | Name_Initializes, | |
376 | Name_Refined_Global, | |
377 | Name_Refined_Depends, | |
378 | Name_Refined_State) | |
379 | then | |
380 | return True; | |
241ebe89 HK |
381 | end if; |
382 | end if; | |
8636f52f HK |
383 | |
384 | return False; | |
241ebe89 | 385 | end Is_OK_Pragma; |
8636f52f | 386 | |
241ebe89 HK |
387 | --------------------- |
388 | -- Is_OK_Statement -- | |
389 | --------------------- | |
8636f52f | 390 | |
241ebe89 | 391 | function Is_OK_Statement (Stmt : Node_Id) return Boolean is |
241ebe89 | 392 | begin |
d65a80fd HK |
393 | -- An assignment statement is Ghost when the target is a Ghost |
394 | -- entity. | |
8636f52f | 395 | |
d65a80fd HK |
396 | if Nkind (Stmt) = N_Assignment_Statement then |
397 | return Is_Ghost_Assignment (Stmt); | |
8636f52f | 398 | |
d65a80fd HK |
399 | -- A procedure call is Ghost when it calls a Ghost procedure |
400 | ||
401 | elsif Nkind (Stmt) = N_Procedure_Call_Statement then | |
402 | return Is_Ghost_Procedure_Call (Stmt); | |
241ebe89 HK |
403 | |
404 | -- Special cases | |
405 | ||
95fef24f AC |
406 | -- An if statement is a suitable context for a Ghost entity if it |
407 | -- is the byproduct of assertion expression expansion. Note that | |
408 | -- the assertion expression may not be related to a Ghost entity, | |
409 | -- but it may still contain references to Ghost entities. | |
241ebe89 | 410 | |
95fef24f AC |
411 | elsif Nkind (Stmt) = N_If_Statement |
412 | and then Nkind (Original_Node (Stmt)) = N_Pragma | |
413 | and then Assertion_Expression_Pragma | |
414 | (Get_Pragma_Id (Original_Node (Stmt))) | |
415 | then | |
416 | return True; | |
241ebe89 HK |
417 | end if; |
418 | ||
419 | return False; | |
420 | end Is_OK_Statement; | |
421 | ||
422 | -- Local variables | |
8636f52f | 423 | |
241ebe89 | 424 | Par : Node_Id; |
8636f52f | 425 | |
241ebe89 HK |
426 | -- Start of processing for Is_OK_Ghost_Context |
427 | ||
428 | begin | |
429 | -- The context is Ghost when it appears within a Ghost package or | |
430 | -- subprogram. | |
431 | ||
432 | if Ghost_Mode > None then | |
8636f52f HK |
433 | return True; |
434 | ||
0bb97bdf YM |
435 | -- A Ghost type may be referenced in a use_type clause |
436 | -- (SPARK RM 6.9.10). | |
437 | ||
438 | elsif Present (Parent (Context)) | |
439 | and then Nkind (Parent (Context)) = N_Use_Type_Clause | |
440 | then | |
441 | return True; | |
442 | ||
8636f52f HK |
443 | -- Routine Expand_Record_Extension creates a parent subtype without |
444 | -- inserting it into the tree. There is no good way of recognizing | |
445 | -- this special case as there is no parent. Try to approximate the | |
446 | -- context. | |
447 | ||
448 | elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then | |
449 | return True; | |
450 | ||
241ebe89 HK |
451 | -- Otherwise climb the parent chain looking for a suitable Ghost |
452 | -- context. | |
453 | ||
8636f52f | 454 | else |
241ebe89 HK |
455 | Par := Context; |
456 | while Present (Par) loop | |
457 | if Is_Ignored_Ghost_Node (Par) then | |
458 | return True; | |
459 | ||
460 | -- A reference to a Ghost entity can appear within an aspect | |
1155ae01 AC |
461 | -- specification (SPARK RM 6.9(10)). The precise checking will |
462 | -- occur when analyzing the corresponding pragma. We make an | |
463 | -- exception for predicate aspects that only allow referencing | |
464 | -- a Ghost entity when the corresponding type declaration is | |
465 | -- Ghost (SPARK RM 6.9(11)). | |
466 | ||
467 | elsif Nkind (Par) = N_Aspect_Specification | |
468 | and then not Same_Aspect | |
469 | (Get_Aspect_Id (Par), Aspect_Predicate) | |
470 | then | |
241ebe89 HK |
471 | return True; |
472 | ||
473 | elsif Is_OK_Declaration (Par) then | |
474 | return True; | |
475 | ||
476 | elsif Is_OK_Pragma (Par) then | |
477 | return True; | |
478 | ||
479 | elsif Is_OK_Statement (Par) then | |
480 | return True; | |
481 | ||
482 | -- Prevent the search from going too far | |
483 | ||
484 | elsif Is_Body_Or_Package_Declaration (Par) then | |
95fef24f | 485 | exit; |
241ebe89 HK |
486 | end if; |
487 | ||
488 | Par := Parent (Par); | |
489 | end loop; | |
490 | ||
95fef24f AC |
491 | -- The expansion of assertion expression pragmas and attribute Old |
492 | -- may cause a legal Ghost entity reference to become illegal due | |
493 | -- to node relocation. Check the In_Assertion_Expr counter as last | |
494 | -- resort to try and infer the original legal context. | |
495 | ||
496 | if In_Assertion_Expr > 0 then | |
497 | return True; | |
498 | ||
499 | -- Otherwise the context is not suitable for a reference to a | |
500 | -- Ghost entity. | |
501 | ||
502 | else | |
503 | return False; | |
504 | end if; | |
8636f52f HK |
505 | end if; |
506 | end Is_OK_Ghost_Context; | |
507 | ||
508 | ------------------------ | |
509 | -- Check_Ghost_Policy -- | |
510 | ------------------------ | |
511 | ||
ac8380d5 | 512 | procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is |
8636f52f HK |
513 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); |
514 | ||
515 | begin | |
516 | -- The Ghost policy in effect a the point of declaration and at the | |
4179af27 | 517 | -- point of use must match (SPARK RM 6.9(13)). |
8636f52f | 518 | |
ac8380d5 AC |
519 | if Is_Checked_Ghost_Entity (Id) |
520 | and then Policy = Name_Ignore | |
521 | and then May_Be_Lvalue (Ref) | |
522 | then | |
523 | Error_Msg_Sloc := Sloc (Ref); | |
8636f52f | 524 | |
ac8380d5 AC |
525 | Error_Msg_N ("incompatible ghost policies in effect", Ref); |
526 | Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id); | |
527 | Error_Msg_NE ("\& used # with ghost policy `Ignore`", Ref, Id); | |
8636f52f HK |
528 | |
529 | elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then | |
ac8380d5 | 530 | Error_Msg_Sloc := Sloc (Ref); |
8636f52f | 531 | |
ac8380d5 AC |
532 | Error_Msg_N ("incompatible ghost policies in effect", Ref); |
533 | Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id); | |
534 | Error_Msg_NE ("\& used # with ghost policy `Check`", Ref, Id); | |
8636f52f HK |
535 | end if; |
536 | end Check_Ghost_Policy; | |
537 | ||
538 | -- Start of processing for Check_Ghost_Context | |
539 | ||
540 | begin | |
541 | -- Once it has been established that the reference to the Ghost entity | |
542 | -- is within a suitable context, ensure that the policy at the point of | |
543 | -- declaration and at the point of use match. | |
544 | ||
545 | if Is_OK_Ghost_Context (Ghost_Ref) then | |
546 | Check_Ghost_Policy (Ghost_Id, Ghost_Ref); | |
547 | ||
548 | -- Otherwise the Ghost entity appears in a non-Ghost context and affects | |
ac8380d5 | 549 | -- its behavior or value (SPARK RM 6.9(10,11)). |
8636f52f HK |
550 | |
551 | else | |
1af4455a | 552 | Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref); |
8636f52f HK |
553 | end if; |
554 | end Check_Ghost_Context; | |
555 | ||
241ebe89 HK |
556 | ---------------------------- |
557 | -- Check_Ghost_Overriding -- | |
558 | ---------------------------- | |
559 | ||
560 | procedure Check_Ghost_Overriding | |
561 | (Subp : Entity_Id; | |
562 | Overridden_Subp : Entity_Id) | |
563 | is | |
4179af27 | 564 | Deriv_Typ : Entity_Id; |
95fef24f | 565 | Over_Subp : Entity_Id; |
241ebe89 HK |
566 | |
567 | begin | |
568 | if Present (Subp) and then Present (Overridden_Subp) then | |
95fef24f | 569 | Over_Subp := Ultimate_Alias (Overridden_Subp); |
4179af27 | 570 | Deriv_Typ := Find_Dispatching_Type (Subp); |
241ebe89 | 571 | |
4179af27 HK |
572 | -- A Ghost primitive of a non-Ghost type extension cannot override an |
573 | -- inherited non-Ghost primitive (SPARK RM 6.9(8)). | |
241ebe89 | 574 | |
4179af27 HK |
575 | if Is_Ghost_Entity (Subp) |
576 | and then Present (Deriv_Typ) | |
577 | and then not Is_Ghost_Entity (Deriv_Typ) | |
578 | and then not Is_Ghost_Entity (Over_Subp) | |
393525af | 579 | and then not Is_Abstract_Subprogram (Over_Subp) |
241ebe89 | 580 | then |
4179af27 | 581 | Error_Msg_N ("incompatible overriding in effect", Subp); |
241ebe89 | 582 | |
95fef24f | 583 | Error_Msg_Sloc := Sloc (Over_Subp); |
4179af27 | 584 | Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); |
241ebe89 HK |
585 | |
586 | Error_Msg_Sloc := Sloc (Subp); | |
4179af27 HK |
587 | Error_Msg_N ("\overridden # with ghost subprogram", Subp); |
588 | end if; | |
589 | ||
590 | -- A non-Ghost primitive of a type extension cannot override an | |
591 | -- inherited Ghost primitive (SPARK RM 6.9(8)). | |
241ebe89 | 592 | |
f31dcd99 HK |
593 | if Is_Ghost_Entity (Over_Subp) |
594 | and then not Is_Ghost_Entity (Subp) | |
393525af | 595 | and then not Is_Abstract_Subprogram (Subp) |
241ebe89 | 596 | then |
4179af27 | 597 | Error_Msg_N ("incompatible overriding in effect", Subp); |
241ebe89 | 598 | |
95fef24f | 599 | Error_Msg_Sloc := Sloc (Over_Subp); |
4179af27 | 600 | Error_Msg_N ("\& declared # as ghost subprogram", Subp); |
241ebe89 HK |
601 | |
602 | Error_Msg_Sloc := Sloc (Subp); | |
4179af27 HK |
603 | Error_Msg_N ("\overridden # with non-ghost subprogram", Subp); |
604 | end if; | |
605 | ||
606 | if Present (Deriv_Typ) | |
607 | and then not Is_Ignored_Ghost_Entity (Deriv_Typ) | |
608 | then | |
609 | -- When a tagged type is either non-Ghost or checked Ghost and | |
610 | -- one of its primitives overrides an inherited operation, the | |
611 | -- overridden operation of the ancestor type must be ignored Ghost | |
612 | -- if the primitive is ignored Ghost (SPARK RM 6.9(17)). | |
613 | ||
614 | if Is_Ignored_Ghost_Entity (Subp) then | |
615 | ||
616 | -- Both the parent subprogram and overriding subprogram are | |
617 | -- ignored Ghost. | |
618 | ||
619 | if Is_Ignored_Ghost_Entity (Over_Subp) then | |
620 | null; | |
621 | ||
622 | -- The parent subprogram carries policy Check | |
623 | ||
624 | elsif Is_Checked_Ghost_Entity (Over_Subp) then | |
625 | Error_Msg_N | |
626 | ("incompatible ghost policies in effect", Subp); | |
627 | ||
628 | Error_Msg_Sloc := Sloc (Over_Subp); | |
629 | Error_Msg_N | |
630 | ("\& declared # with ghost policy `Check`", Subp); | |
631 | ||
632 | Error_Msg_Sloc := Sloc (Subp); | |
633 | Error_Msg_N | |
634 | ("\overridden # with ghost policy `Ignore`", Subp); | |
635 | ||
636 | -- The parent subprogram is non-Ghost | |
637 | ||
638 | else | |
639 | Error_Msg_N | |
640 | ("incompatible ghost policies in effect", Subp); | |
641 | ||
642 | Error_Msg_Sloc := Sloc (Over_Subp); | |
643 | Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); | |
644 | ||
645 | Error_Msg_Sloc := Sloc (Subp); | |
646 | Error_Msg_N | |
647 | ("\overridden # with ghost policy `Ignore`", Subp); | |
648 | end if; | |
649 | ||
650 | -- When a tagged type is either non-Ghost or checked Ghost and | |
651 | -- one of its primitives overrides an inherited operation, the | |
652 | -- the primitive of the tagged type must be ignored Ghost if the | |
653 | -- overridden operation is ignored Ghost (SPARK RM 6.9(17)). | |
654 | ||
655 | elsif Is_Ignored_Ghost_Entity (Over_Subp) then | |
656 | ||
657 | -- Both the parent subprogram and the overriding subprogram are | |
658 | -- ignored Ghost. | |
659 | ||
660 | if Is_Ignored_Ghost_Entity (Subp) then | |
661 | null; | |
662 | ||
663 | -- The overriding subprogram carries policy Check | |
664 | ||
665 | elsif Is_Checked_Ghost_Entity (Subp) then | |
666 | Error_Msg_N | |
667 | ("incompatible ghost policies in effect", Subp); | |
668 | ||
669 | Error_Msg_Sloc := Sloc (Over_Subp); | |
670 | Error_Msg_N | |
671 | ("\& declared # with ghost policy `Ignore`", Subp); | |
672 | ||
673 | Error_Msg_Sloc := Sloc (Subp); | |
674 | Error_Msg_N | |
675 | ("\overridden # with Ghost policy `Check`", Subp); | |
676 | ||
677 | -- The overriding subprogram is non-Ghost | |
678 | ||
679 | else | |
680 | Error_Msg_N | |
681 | ("incompatible ghost policies in effect", Subp); | |
682 | ||
683 | Error_Msg_Sloc := Sloc (Over_Subp); | |
684 | Error_Msg_N | |
685 | ("\& declared # with ghost policy `Ignore`", Subp); | |
686 | ||
687 | Error_Msg_Sloc := Sloc (Subp); | |
688 | Error_Msg_N | |
689 | ("\overridden # with non-ghost subprogram", Subp); | |
690 | end if; | |
691 | end if; | |
241ebe89 HK |
692 | end if; |
693 | end if; | |
694 | end Check_Ghost_Overriding; | |
695 | ||
4179af27 HK |
696 | --------------------------- |
697 | -- Check_Ghost_Primitive -- | |
698 | --------------------------- | |
699 | ||
700 | procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is | |
701 | begin | |
702 | -- The Ghost policy in effect at the point of declaration of a primitive | |
703 | -- operation and a tagged type must match (SPARK RM 6.9(16)). | |
704 | ||
705 | if Is_Tagged_Type (Typ) then | |
706 | if Is_Checked_Ghost_Entity (Prim) | |
707 | and then Is_Ignored_Ghost_Entity (Typ) | |
708 | then | |
709 | Error_Msg_N ("incompatible ghost policies in effect", Prim); | |
710 | ||
711 | Error_Msg_Sloc := Sloc (Typ); | |
712 | Error_Msg_NE | |
713 | ("\tagged type & declared # with ghost policy `Ignore`", | |
714 | Prim, Typ); | |
715 | ||
716 | Error_Msg_Sloc := Sloc (Prim); | |
717 | Error_Msg_N | |
718 | ("\primitive subprogram & declared # with ghost policy `Check`", | |
719 | Prim); | |
720 | ||
721 | elsif Is_Ignored_Ghost_Entity (Prim) | |
722 | and then Is_Checked_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 `Check`", | |
729 | Prim, Typ); | |
730 | ||
731 | Error_Msg_Sloc := Sloc (Prim); | |
732 | Error_Msg_N | |
733 | ("\primitive subprogram & declared # with ghost policy `Ignore`", | |
734 | Prim); | |
735 | end if; | |
736 | end if; | |
737 | end Check_Ghost_Primitive; | |
738 | ||
739 | ---------------------------- | |
740 | -- Check_Ghost_Refinement -- | |
741 | ---------------------------- | |
742 | ||
743 | procedure Check_Ghost_Refinement | |
744 | (State : Node_Id; | |
745 | State_Id : Entity_Id; | |
746 | Constit : Node_Id; | |
747 | Constit_Id : Entity_Id) | |
748 | is | |
749 | begin | |
750 | if Is_Ghost_Entity (State_Id) then | |
751 | if Is_Ghost_Entity (Constit_Id) then | |
752 | ||
753 | -- The Ghost policy in effect at the point of abstract state | |
754 | -- declaration and constituent must match (SPARK RM 6.9(15)). | |
755 | ||
756 | if Is_Checked_Ghost_Entity (State_Id) | |
757 | and then Is_Ignored_Ghost_Entity (Constit_Id) | |
758 | then | |
759 | Error_Msg_Sloc := Sloc (Constit); | |
760 | SPARK_Msg_N ("incompatible ghost policies in effect", State); | |
761 | ||
762 | SPARK_Msg_NE | |
763 | ("\abstract state & declared with ghost policy `Check`", | |
764 | State, State_Id); | |
765 | SPARK_Msg_NE | |
766 | ("\constituent & declared # with ghost policy `Ignore`", | |
767 | State, Constit_Id); | |
768 | ||
769 | elsif Is_Ignored_Ghost_Entity (State_Id) | |
770 | and then Is_Checked_Ghost_Entity (Constit_Id) | |
771 | then | |
772 | Error_Msg_Sloc := Sloc (Constit); | |
773 | SPARK_Msg_N ("incompatible ghost policies in effect", State); | |
774 | ||
775 | SPARK_Msg_NE | |
776 | ("\abstract state & declared with ghost policy `Ignore`", | |
777 | State, State_Id); | |
778 | SPARK_Msg_NE | |
779 | ("\constituent & declared # with ghost policy `Check`", | |
780 | State, Constit_Id); | |
781 | end if; | |
782 | ||
783 | -- A constituent of a Ghost abstract state must be a Ghost entity | |
784 | -- (SPARK RM 7.2.2(12)). | |
785 | ||
786 | else | |
787 | SPARK_Msg_NE | |
788 | ("constituent of ghost state & must be ghost", | |
789 | Constit, State_Id); | |
790 | end if; | |
791 | end if; | |
792 | end Check_Ghost_Refinement; | |
793 | ||
a85dbeec HK |
794 | ---------------------- |
795 | -- Check_Ghost_Type -- | |
796 | ---------------------- | |
797 | ||
798 | procedure Check_Ghost_Type (Typ : Entity_Id) is | |
799 | Conc_Typ : Entity_Id; | |
800 | Full_Typ : Entity_Id; | |
801 | ||
802 | begin | |
803 | if Is_Ghost_Entity (Typ) then | |
804 | Conc_Typ := Empty; | |
805 | Full_Typ := Typ; | |
806 | ||
807 | if Is_Single_Concurrent_Type (Typ) then | |
808 | Conc_Typ := Anonymous_Object (Typ); | |
809 | Full_Typ := Conc_Typ; | |
810 | ||
811 | elsif Is_Concurrent_Type (Typ) then | |
812 | Conc_Typ := Typ; | |
813 | end if; | |
814 | ||
815 | -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this | |
816 | -- legality rule first to give a finer-grained diagnostic. | |
817 | ||
818 | if Present (Conc_Typ) then | |
819 | Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ); | |
820 | end if; | |
821 | ||
822 | -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7)) | |
823 | ||
824 | if Is_Effectively_Volatile (Full_Typ) then | |
825 | Error_Msg_N ("ghost type & cannot be volatile", Full_Typ); | |
826 | end if; | |
827 | end if; | |
828 | end Check_Ghost_Type; | |
829 | ||
241ebe89 HK |
830 | ------------------ |
831 | -- Ghost_Entity -- | |
832 | ------------------ | |
833 | ||
b3b3ada9 HK |
834 | function Ghost_Entity (Ref : Node_Id) return Entity_Id is |
835 | Obj_Ref : constant Node_Id := Ultimate_Prefix (Ref); | |
241ebe89 HK |
836 | |
837 | begin | |
b3b3ada9 | 838 | -- When the reference denotes a subcomponent, recover the related whole |
241ebe89 HK |
839 | -- object (SPARK RM 6.9(1)). |
840 | ||
b3b3ada9 HK |
841 | if Is_Entity_Name (Obj_Ref) then |
842 | return Entity (Obj_Ref); | |
843 | ||
844 | -- Otherwise the reference cannot possibly denote a Ghost entity | |
241ebe89 | 845 | |
241ebe89 HK |
846 | else |
847 | return Empty; | |
848 | end if; | |
849 | end Ghost_Entity; | |
850 | ||
8636f52f HK |
851 | -------------------------------- |
852 | -- Implements_Ghost_Interface -- | |
853 | -------------------------------- | |
854 | ||
855 | function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is | |
856 | Iface_Elmt : Elmt_Id; | |
857 | ||
858 | begin | |
859 | -- Traverse the list of interfaces looking for a Ghost interface | |
860 | ||
861 | if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then | |
862 | Iface_Elmt := First_Elmt (Interfaces (Typ)); | |
863 | while Present (Iface_Elmt) loop | |
864 | if Is_Ghost_Entity (Node (Iface_Elmt)) then | |
865 | return True; | |
866 | end if; | |
867 | ||
868 | Next_Elmt (Iface_Elmt); | |
869 | end loop; | |
870 | end if; | |
871 | ||
872 | return False; | |
873 | end Implements_Ghost_Interface; | |
874 | ||
875 | ---------------- | |
876 | -- Initialize -- | |
877 | ---------------- | |
878 | ||
879 | procedure Initialize is | |
880 | begin | |
980f94b7 HK |
881 | Ignored_Ghost_Nodes.Init; |
882 | ||
883 | -- Set the soft link which enables Atree.Mark_New_Ghost_Node to record | |
884 | -- an ignored Ghost node or entity. | |
885 | ||
886 | Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access); | |
8636f52f HK |
887 | end Initialize; |
888 | ||
d65a80fd HK |
889 | ------------------------ |
890 | -- Install_Ghost_Mode -- | |
891 | ------------------------ | |
892 | ||
893 | procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is | |
894 | begin | |
9057bd6a | 895 | Install_Ghost_Region (Mode, Empty); |
d65a80fd HK |
896 | end Install_Ghost_Mode; |
897 | ||
9057bd6a HK |
898 | -------------------------- |
899 | -- Install_Ghost_Region -- | |
900 | -------------------------- | |
901 | ||
902 | procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is | |
d65a80fd | 903 | begin |
9057bd6a HK |
904 | -- The context is already within an ignored Ghost region. Maintain the |
905 | -- start of the outermost ignored Ghost region. | |
d65a80fd | 906 | |
9057bd6a HK |
907 | if Present (Ignored_Ghost_Region) then |
908 | null; | |
909 | ||
910 | -- The current region is the outermost ignored Ghost region. Save its | |
911 | -- starting node. | |
912 | ||
913 | elsif Present (N) and then Mode = Ignore then | |
914 | Ignored_Ghost_Region := N; | |
d65a80fd | 915 | |
9057bd6a HK |
916 | -- Otherwise the current region is not ignored, nothing to save |
917 | ||
918 | else | |
919 | Ignored_Ghost_Region := Empty; | |
d65a80fd | 920 | end if; |
9057bd6a HK |
921 | |
922 | Ghost_Mode := Mode; | |
923 | end Install_Ghost_Region; | |
924 | ||
925 | procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is | |
926 | begin | |
927 | Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N); | |
928 | end Install_Ghost_Region; | |
d65a80fd HK |
929 | |
930 | ------------------------- | |
931 | -- Is_Ghost_Assignment -- | |
932 | ------------------------- | |
933 | ||
934 | function Is_Ghost_Assignment (N : Node_Id) return Boolean is | |
935 | Id : Entity_Id; | |
936 | ||
937 | begin | |
938 | -- An assignment statement is Ghost when its target denotes a Ghost | |
939 | -- entity. | |
940 | ||
941 | if Nkind (N) = N_Assignment_Statement then | |
942 | Id := Ghost_Entity (Name (N)); | |
943 | ||
944 | return Present (Id) and then Is_Ghost_Entity (Id); | |
945 | end if; | |
946 | ||
947 | return False; | |
948 | end Is_Ghost_Assignment; | |
949 | ||
950 | -------------------------- | |
951 | -- Is_Ghost_Declaration -- | |
952 | -------------------------- | |
953 | ||
954 | function Is_Ghost_Declaration (N : Node_Id) return Boolean is | |
955 | Id : Entity_Id; | |
956 | ||
957 | begin | |
958 | -- A declaration is Ghost when it elaborates a Ghost entity or is | |
959 | -- subject to pragma Ghost. | |
960 | ||
961 | if Is_Declaration (N) then | |
962 | Id := Defining_Entity (N); | |
963 | ||
964 | return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N); | |
965 | end if; | |
966 | ||
967 | return False; | |
968 | end Is_Ghost_Declaration; | |
969 | ||
970 | --------------------- | |
971 | -- Is_Ghost_Pragma -- | |
972 | --------------------- | |
973 | ||
974 | function Is_Ghost_Pragma (N : Node_Id) return Boolean is | |
975 | begin | |
976 | return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N); | |
977 | end Is_Ghost_Pragma; | |
978 | ||
979 | ----------------------------- | |
980 | -- Is_Ghost_Procedure_Call -- | |
981 | ----------------------------- | |
982 | ||
983 | function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is | |
984 | Id : Entity_Id; | |
985 | ||
986 | begin | |
987 | -- A procedure call is Ghost when it invokes a Ghost procedure | |
988 | ||
989 | if Nkind (N) = N_Procedure_Call_Statement then | |
990 | Id := Ghost_Entity (Name (N)); | |
991 | ||
992 | return Present (Id) and then Is_Ghost_Entity (Id); | |
993 | end if; | |
994 | ||
995 | return False; | |
996 | end Is_Ghost_Procedure_Call; | |
997 | ||
dafe11cd HK |
998 | --------------------------- |
999 | -- Is_Ignored_Ghost_Unit -- | |
1000 | --------------------------- | |
1001 | ||
1002 | function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is | |
980f94b7 HK |
1003 | function Ultimate_Original_Node (Nod : Node_Id) return Node_Id; |
1004 | -- Obtain the original node of arbitrary node Nod following a potential | |
1005 | -- chain of rewritings. | |
1006 | ||
1007 | ---------------------------- | |
1008 | -- Ultimate_Original_Node -- | |
1009 | ---------------------------- | |
1010 | ||
1011 | function Ultimate_Original_Node (Nod : Node_Id) return Node_Id is | |
1012 | Res : Node_Id; | |
1013 | ||
1014 | begin | |
1015 | Res := Nod; | |
1016 | while Original_Node (Res) /= Res loop | |
1017 | Res := Original_Node (Res); | |
1018 | end loop; | |
1019 | ||
1020 | return Res; | |
1021 | end Ultimate_Original_Node; | |
1022 | ||
1023 | -- Start of processing for Is_Ignored_Ghost_Unit | |
1024 | ||
dafe11cd HK |
1025 | begin |
1026 | -- Inspect the original node of the unit in case removal of ignored | |
1027 | -- Ghost code has already taken place. | |
1028 | ||
1029 | return | |
1030 | Nkind (N) = N_Compilation_Unit | |
1031 | and then Is_Ignored_Ghost_Entity | |
980f94b7 | 1032 | (Defining_Entity (Ultimate_Original_Node (Unit (N)))); |
dafe11cd HK |
1033 | end Is_Ignored_Ghost_Unit; |
1034 | ||
8636f52f HK |
1035 | ------------------------- |
1036 | -- Is_Subject_To_Ghost -- | |
1037 | ------------------------- | |
1038 | ||
1039 | function Is_Subject_To_Ghost (N : Node_Id) return Boolean is | |
1040 | function Enables_Ghostness (Arg : Node_Id) return Boolean; | |
1041 | -- Determine whether aspect or pragma argument Arg enables "ghostness" | |
1042 | ||
1043 | ----------------------- | |
1044 | -- Enables_Ghostness -- | |
1045 | ----------------------- | |
1046 | ||
1047 | function Enables_Ghostness (Arg : Node_Id) return Boolean is | |
1048 | Expr : Node_Id; | |
1049 | ||
1050 | begin | |
1051 | Expr := Arg; | |
1052 | ||
1053 | if Nkind (Expr) = N_Pragma_Argument_Association then | |
1054 | Expr := Get_Pragma_Arg (Expr); | |
1055 | end if; | |
1056 | ||
1af4455a HK |
1057 | -- Determine whether the expression of the aspect or pragma is static |
1058 | -- and denotes True. | |
8636f52f HK |
1059 | |
1060 | if Present (Expr) then | |
1061 | Preanalyze_And_Resolve (Expr); | |
1062 | ||
1063 | return | |
1064 | Is_OK_Static_Expression (Expr) | |
1065 | and then Is_True (Expr_Value (Expr)); | |
1066 | ||
1067 | -- Otherwise Ghost defaults to True | |
1068 | ||
1069 | else | |
1070 | return True; | |
1071 | end if; | |
1072 | end Enables_Ghostness; | |
1073 | ||
1074 | -- Local variables | |
1075 | ||
1076 | Id : constant Entity_Id := Defining_Entity (N); | |
1077 | Asp : Node_Id; | |
1078 | Decl : Node_Id; | |
1079 | Prev_Id : Entity_Id; | |
1080 | ||
1081 | -- Start of processing for Is_Subject_To_Ghost | |
1082 | ||
1083 | begin | |
1084 | -- The related entity of the declaration has not been analyzed yet, do | |
1085 | -- not inspect its attributes. | |
1086 | ||
1087 | if Ekind (Id) = E_Void then | |
1088 | null; | |
1089 | ||
1090 | elsif Is_Ghost_Entity (Id) then | |
1091 | return True; | |
1092 | ||
1093 | -- The completion of a type or a constant is not fully analyzed when the | |
1094 | -- reference to the Ghost entity is resolved. Because the completion is | |
1095 | -- not marked as Ghost yet, inspect the partial view. | |
1096 | ||
1097 | elsif Is_Record_Type (Id) | |
1098 | or else Ekind (Id) = E_Constant | |
1099 | or else (Nkind (N) = N_Object_Declaration | |
1100 | and then Constant_Present (N)) | |
1101 | then | |
1102 | Prev_Id := Incomplete_Or_Partial_View (Id); | |
1103 | ||
1104 | if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then | |
1105 | return True; | |
1106 | end if; | |
1107 | end if; | |
1108 | ||
1109 | -- Examine the aspect specifications (if any) looking for aspect Ghost | |
1110 | ||
1111 | if Permits_Aspect_Specifications (N) then | |
1112 | Asp := First (Aspect_Specifications (N)); | |
1113 | while Present (Asp) loop | |
1114 | if Chars (Identifier (Asp)) = Name_Ghost then | |
1115 | return Enables_Ghostness (Expression (Asp)); | |
1116 | end if; | |
1117 | ||
1118 | Next (Asp); | |
1119 | end loop; | |
1120 | end if; | |
1121 | ||
1122 | Decl := Empty; | |
1123 | ||
1124 | -- When the context is a [generic] package declaration, pragma Ghost | |
1125 | -- resides in the visible declarations. | |
1126 | ||
1127 | if Nkind_In (N, N_Generic_Package_Declaration, | |
1128 | N_Package_Declaration) | |
1129 | then | |
1130 | Decl := First (Visible_Declarations (Specification (N))); | |
1131 | ||
1132 | -- When the context is a package or a subprogram body, pragma Ghost | |
1133 | -- resides in the declarative part. | |
1134 | ||
1135 | elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then | |
1136 | Decl := First (Declarations (N)); | |
1137 | ||
1138 | -- Otherwise pragma Ghost appears in the declarations following N | |
1139 | ||
1140 | elsif Is_List_Member (N) then | |
1141 | Decl := Next (N); | |
1142 | end if; | |
1143 | ||
1144 | while Present (Decl) loop | |
1145 | if Nkind (Decl) = N_Pragma | |
6e759c2a | 1146 | and then Pragma_Name (Decl) = Name_Ghost |
8636f52f HK |
1147 | then |
1148 | return | |
1149 | Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); | |
1150 | ||
1151 | -- A source construct ends the region where pragma Ghost may appear, | |
2700b9c1 AC |
1152 | -- stop the traversal. Check the original node as source constructs |
1153 | -- may be rewritten into something else by expansion. | |
8636f52f | 1154 | |
2700b9c1 | 1155 | elsif Comes_From_Source (Original_Node (Decl)) then |
8636f52f HK |
1156 | exit; |
1157 | end if; | |
1158 | ||
1159 | Next (Decl); | |
1160 | end loop; | |
1161 | ||
1162 | return False; | |
1163 | end Is_Subject_To_Ghost; | |
1164 | ||
1165 | ---------- | |
1166 | -- Lock -- | |
1167 | ---------- | |
1168 | ||
1169 | procedure Lock is | |
1170 | begin | |
980f94b7 HK |
1171 | Ignored_Ghost_Nodes.Release; |
1172 | Ignored_Ghost_Nodes.Locked := True; | |
8636f52f HK |
1173 | end Lock; |
1174 | ||
d65a80fd HK |
1175 | ----------------------------------- |
1176 | -- Mark_And_Set_Ghost_Assignment -- | |
1177 | ----------------------------------- | |
1178 | ||
f9a8f910 | 1179 | procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is |
b3b3ada9 HK |
1180 | Orig_Lhs : constant Node_Id := Name (N); |
1181 | Orig_Ref : constant Node_Id := Ultimate_Prefix (Orig_Lhs); | |
1182 | ||
1183 | Id : Entity_Id; | |
1184 | Ref : Node_Id; | |
d65a80fd HK |
1185 | |
1186 | begin | |
b3b3ada9 HK |
1187 | -- A reference to a whole Ghost object (SPARK RM 6.9(1)) appears as an |
1188 | -- identifier. If the reference has not been analyzed yet, preanalyze a | |
1189 | -- copy of the reference to discover the nature of its entity. | |
1190 | ||
1191 | if Nkind (Orig_Ref) = N_Identifier and then not Analyzed (Orig_Ref) then | |
1192 | Ref := New_Copy_Tree (Orig_Ref); | |
1193 | ||
1194 | -- Alter the assignment statement by setting its left-hand side to | |
1195 | -- the copy. | |
1196 | ||
1197 | Set_Name (N, Ref); | |
1198 | Set_Parent (Ref, N); | |
1199 | ||
1200 | -- Preanalysis is carried out by looking for a Ghost entity while | |
1201 | -- suppressing all possible side effects. | |
1202 | ||
1203 | Find_Direct_Name | |
1204 | (N => Ref, | |
1205 | Errors_OK => False, | |
1206 | Marker_OK => False, | |
1207 | Reference_OK => False); | |
1208 | ||
1209 | -- Restore the original state of the assignment statement | |
1210 | ||
1211 | Set_Name (N, Orig_Lhs); | |
1212 | ||
1213 | -- A potential reference to a Ghost entity is already properly resolved | |
1214 | -- when the left-hand side is analyzed. | |
1215 | ||
1216 | else | |
1217 | Ref := Orig_Ref; | |
1218 | end if; | |
1219 | ||
d65a80fd HK |
1220 | -- An assignment statement becomes Ghost when its target denotes a Ghost |
1221 | -- object. Install the Ghost mode of the target. | |
1222 | ||
b3b3ada9 | 1223 | Id := Ghost_Entity (Ref); |
d65a80fd HK |
1224 | |
1225 | if Present (Id) then | |
1226 | if Is_Checked_Ghost_Entity (Id) then | |
9057bd6a | 1227 | Install_Ghost_Region (Check, N); |
d65a80fd HK |
1228 | |
1229 | elsif Is_Ignored_Ghost_Entity (Id) then | |
9057bd6a | 1230 | Install_Ghost_Region (Ignore, N); |
d65a80fd HK |
1231 | |
1232 | Set_Is_Ignored_Ghost_Node (N); | |
980f94b7 | 1233 | Record_Ignored_Ghost_Node (N); |
d65a80fd HK |
1234 | end if; |
1235 | end if; | |
1236 | end Mark_And_Set_Ghost_Assignment; | |
1237 | ||
241ebe89 | 1238 | ----------------------------- |
d65a80fd | 1239 | -- Mark_And_Set_Ghost_Body -- |
241ebe89 HK |
1240 | ----------------------------- |
1241 | ||
d65a80fd HK |
1242 | procedure Mark_And_Set_Ghost_Body |
1243 | (N : Node_Id; | |
f9a8f910 | 1244 | Spec_Id : Entity_Id) |
241ebe89 | 1245 | is |
d65a80fd HK |
1246 | Body_Id : constant Entity_Id := Defining_Entity (N); |
1247 | Policy : Name_Id := No_Name; | |
241ebe89 HK |
1248 | |
1249 | begin | |
d65a80fd | 1250 | -- A body becomes Ghost when it is subject to aspect or pragma Ghost |
241ebe89 | 1251 | |
d65a80fd HK |
1252 | if Is_Subject_To_Ghost (N) then |
1253 | Policy := Policy_In_Effect (Name_Ghost); | |
1254 | ||
1255 | -- A body declared within a Ghost region is automatically Ghost | |
1256 | -- (SPARK RM 6.9(2)). | |
1257 | ||
1258 | elsif Ghost_Mode = Check then | |
1259 | Policy := Name_Check; | |
1260 | ||
1261 | elsif Ghost_Mode = Ignore then | |
1262 | Policy := Name_Ignore; | |
1263 | ||
1264 | -- Inherit the "ghostness" of the previous declaration when the body | |
1265 | -- acts as a completion. | |
1266 | ||
1267 | elsif Present (Spec_Id) then | |
1268 | if Is_Checked_Ghost_Entity (Spec_Id) then | |
1269 | Policy := Name_Check; | |
1270 | ||
1271 | elsif Is_Ignored_Ghost_Entity (Spec_Id) then | |
1272 | Policy := Name_Ignore; | |
1273 | end if; | |
241ebe89 | 1274 | end if; |
241ebe89 | 1275 | |
d65a80fd HK |
1276 | -- The Ghost policy in effect at the point of declaration and at the |
1277 | -- point of completion must match (SPARK RM 6.9(14)). | |
1278 | ||
1279 | Check_Ghost_Completion | |
1280 | (Prev_Id => Spec_Id, | |
1281 | Compl_Id => Body_Id); | |
1282 | ||
1283 | -- Mark the body as its formals as Ghost | |
1284 | ||
1285 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1286 | ||
9057bd6a | 1287 | -- Install the appropriate Ghost region |
d65a80fd | 1288 | |
9057bd6a | 1289 | Install_Ghost_Region (Policy, N); |
d65a80fd HK |
1290 | end Mark_And_Set_Ghost_Body; |
1291 | ||
1292 | ----------------------------------- | |
1293 | -- Mark_And_Set_Ghost_Completion -- | |
1294 | ----------------------------------- | |
241ebe89 | 1295 | |
d65a80fd HK |
1296 | procedure Mark_And_Set_Ghost_Completion |
1297 | (N : Node_Id; | |
f9a8f910 | 1298 | Prev_Id : Entity_Id) |
241ebe89 | 1299 | is |
d65a80fd HK |
1300 | Compl_Id : constant Entity_Id := Defining_Entity (N); |
1301 | Policy : Name_Id := No_Name; | |
1302 | ||
241ebe89 | 1303 | begin |
d65a80fd HK |
1304 | -- A completion elaborated in a Ghost region is automatically Ghost |
1305 | -- (SPARK RM 6.9(2)). | |
1306 | ||
1307 | if Ghost_Mode = Check then | |
1308 | Policy := Name_Check; | |
1309 | ||
1310 | elsif Ghost_Mode = Ignore then | |
1311 | Policy := Name_Ignore; | |
1312 | ||
1313 | -- The completion becomes Ghost when its initial declaration is also | |
1314 | -- Ghost. | |
1315 | ||
1316 | elsif Is_Checked_Ghost_Entity (Prev_Id) then | |
1317 | Policy := Name_Check; | |
241ebe89 | 1318 | |
d65a80fd HK |
1319 | elsif Is_Ignored_Ghost_Entity (Prev_Id) then |
1320 | Policy := Name_Ignore; | |
241ebe89 | 1321 | end if; |
241ebe89 | 1322 | |
d65a80fd HK |
1323 | -- The Ghost policy in effect at the point of declaration and at the |
1324 | -- point of completion must match (SPARK RM 6.9(14)). | |
1325 | ||
1326 | Check_Ghost_Completion | |
1327 | (Prev_Id => Prev_Id, | |
1328 | Compl_Id => Compl_Id); | |
1329 | ||
1330 | -- Mark the completion as Ghost | |
1331 | ||
1332 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1333 | ||
9057bd6a | 1334 | -- Install the appropriate Ghost region |
d65a80fd | 1335 | |
9057bd6a | 1336 | Install_Ghost_Region (Policy, N); |
d65a80fd | 1337 | end Mark_And_Set_Ghost_Completion; |
241ebe89 | 1338 | |
d65a80fd HK |
1339 | ------------------------------------ |
1340 | -- Mark_And_Set_Ghost_Declaration -- | |
1341 | ------------------------------------ | |
1342 | ||
f9a8f910 | 1343 | procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is |
d65a80fd HK |
1344 | Par_Id : Entity_Id; |
1345 | Policy : Name_Id := No_Name; | |
241ebe89 HK |
1346 | |
1347 | begin | |
d65a80fd HK |
1348 | -- A declaration becomes Ghost when it is subject to aspect or pragma |
1349 | -- Ghost. | |
1350 | ||
1351 | if Is_Subject_To_Ghost (N) then | |
1352 | Policy := Policy_In_Effect (Name_Ghost); | |
1353 | ||
1354 | -- A declaration elaborated in a Ghost region is automatically Ghost | |
1355 | -- (SPARK RM 6.9(2)). | |
1356 | ||
1357 | elsif Ghost_Mode = Check then | |
1358 | Policy := Name_Check; | |
1359 | ||
1360 | elsif Ghost_Mode = Ignore then | |
1361 | Policy := Name_Ignore; | |
1362 | ||
1363 | -- A child package or subprogram declaration becomes Ghost when its | |
1364 | -- parent is Ghost (SPARK RM 6.9(2)). | |
241ebe89 | 1365 | |
d65a80fd HK |
1366 | elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration, |
1367 | N_Generic_Package_Declaration, | |
1368 | N_Generic_Package_Renaming_Declaration, | |
1369 | N_Generic_Procedure_Renaming_Declaration, | |
1370 | N_Generic_Subprogram_Declaration, | |
1371 | N_Package_Declaration, | |
1372 | N_Package_Renaming_Declaration, | |
1373 | N_Subprogram_Declaration, | |
1374 | N_Subprogram_Renaming_Declaration) | |
1375 | and then Present (Parent_Spec (N)) | |
1376 | then | |
1377 | Par_Id := Defining_Entity (Unit (Parent_Spec (N))); | |
1378 | ||
1379 | if Is_Checked_Ghost_Entity (Par_Id) then | |
1380 | Policy := Name_Check; | |
1381 | ||
1382 | elsif Is_Ignored_Ghost_Entity (Par_Id) then | |
1383 | Policy := Name_Ignore; | |
1384 | end if; | |
1385 | end if; | |
1386 | ||
1387 | -- Mark the declaration and its formals as Ghost | |
1388 | ||
1389 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1390 | ||
9057bd6a | 1391 | -- Install the appropriate Ghost region |
d65a80fd | 1392 | |
9057bd6a | 1393 | Install_Ghost_Region (Policy, N); |
d65a80fd HK |
1394 | end Mark_And_Set_Ghost_Declaration; |
1395 | ||
1396 | -------------------------------------- | |
1397 | -- Mark_And_Set_Ghost_Instantiation -- | |
1398 | -------------------------------------- | |
1399 | ||
1400 | procedure Mark_And_Set_Ghost_Instantiation | |
1401 | (N : Node_Id; | |
f9a8f910 | 1402 | Gen_Id : Entity_Id) |
d65a80fd | 1403 | is |
fe683ef6 AC |
1404 | procedure Check_Ghost_Actuals; |
1405 | -- Check the context of ghost actuals | |
1406 | ||
1407 | ------------------------- | |
1408 | -- Check_Ghost_Actuals -- | |
1409 | ------------------------- | |
1410 | ||
1411 | procedure Check_Ghost_Actuals is | |
1412 | Assoc : Node_Id := First (Generic_Associations (N)); | |
1413 | Act : Node_Id; | |
1414 | ||
1415 | begin | |
1416 | while Present (Assoc) loop | |
1417 | if Nkind (Assoc) /= N_Others_Choice then | |
1418 | Act := Explicit_Generic_Actual_Parameter (Assoc); | |
1419 | ||
1420 | -- Within a nested instantiation, a defaulted actual is an | |
1421 | -- empty association, so nothing to check. | |
1422 | ||
1423 | if No (Act) then | |
1424 | null; | |
1425 | ||
1426 | elsif Comes_From_Source (Act) | |
1427 | and then Nkind (Act) in N_Has_Etype | |
1428 | and then Present (Etype (Act)) | |
1429 | and then Is_Ghost_Entity (Etype (Act)) | |
1430 | then | |
1431 | Check_Ghost_Context (Etype (Act), Act); | |
1432 | end if; | |
1433 | end if; | |
1434 | ||
1435 | Next (Assoc); | |
1436 | end loop; | |
1437 | end Check_Ghost_Actuals; | |
1438 | ||
1439 | -- Local variables | |
1440 | ||
d65a80fd HK |
1441 | Policy : Name_Id := No_Name; |
1442 | ||
1443 | begin | |
d65a80fd HK |
1444 | -- An instantiation becomes Ghost when it is subject to pragma Ghost |
1445 | ||
1446 | if Is_Subject_To_Ghost (N) then | |
1447 | Policy := Policy_In_Effect (Name_Ghost); | |
1448 | ||
1449 | -- An instantiation declaration within a Ghost region is automatically | |
1450 | -- Ghost (SPARK RM 6.9(2)). | |
1451 | ||
1452 | elsif Ghost_Mode = Check then | |
1453 | Policy := Name_Check; | |
1454 | ||
1455 | elsif Ghost_Mode = Ignore then | |
1456 | Policy := Name_Ignore; | |
1457 | ||
1458 | -- Inherit the "ghostness" of the generic unit | |
1459 | ||
1460 | elsif Is_Checked_Ghost_Entity (Gen_Id) then | |
1461 | Policy := Name_Check; | |
1462 | ||
1463 | elsif Is_Ignored_Ghost_Entity (Gen_Id) then | |
1464 | Policy := Name_Ignore; | |
1465 | end if; | |
1466 | ||
1467 | -- Mark the instantiation as Ghost | |
1468 | ||
1469 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1470 | ||
9057bd6a | 1471 | -- Install the appropriate Ghost region |
d65a80fd | 1472 | |
9057bd6a | 1473 | Install_Ghost_Region (Policy, N); |
fe683ef6 | 1474 | |
9057bd6a | 1475 | -- Check Ghost actuals. Given that this routine is unconditionally |
fe683ef6 AC |
1476 | -- invoked with subprogram and package instantiations, this check |
1477 | -- verifies the context of all the ghost entities passed in generic | |
1478 | -- instantiations. | |
1479 | ||
1480 | Check_Ghost_Actuals; | |
d65a80fd HK |
1481 | end Mark_And_Set_Ghost_Instantiation; |
1482 | ||
1483 | --------------------------------------- | |
1484 | -- Mark_And_Set_Ghost_Procedure_Call -- | |
1485 | --------------------------------------- | |
1486 | ||
f9a8f910 | 1487 | procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is |
d65a80fd HK |
1488 | Id : Entity_Id; |
1489 | ||
1490 | begin | |
d65a80fd HK |
1491 | -- A procedure call becomes Ghost when the procedure being invoked is |
1492 | -- Ghost. Install the Ghost mode of the procedure. | |
1493 | ||
1494 | Id := Ghost_Entity (Name (N)); | |
1495 | ||
1496 | if Present (Id) then | |
1497 | if Is_Checked_Ghost_Entity (Id) then | |
9057bd6a | 1498 | Install_Ghost_Region (Check, N); |
d65a80fd HK |
1499 | |
1500 | elsif Is_Ignored_Ghost_Entity (Id) then | |
9057bd6a | 1501 | Install_Ghost_Region (Ignore, N); |
d65a80fd HK |
1502 | |
1503 | Set_Is_Ignored_Ghost_Node (N); | |
980f94b7 | 1504 | Record_Ignored_Ghost_Node (N); |
d65a80fd HK |
1505 | end if; |
1506 | end if; | |
1507 | end Mark_And_Set_Ghost_Procedure_Call; | |
1508 | ||
980f94b7 HK |
1509 | ----------------------- |
1510 | -- Mark_Ghost_Clause -- | |
1511 | ----------------------- | |
1512 | ||
1513 | procedure Mark_Ghost_Clause (N : Node_Id) is | |
1514 | Nam : Node_Id := Empty; | |
1515 | ||
1516 | begin | |
1517 | if Nkind (N) = N_Use_Package_Clause then | |
1518 | Nam := Name (N); | |
1519 | ||
1520 | elsif Nkind (N) = N_Use_Type_Clause then | |
1521 | Nam := Subtype_Mark (N); | |
1522 | ||
1523 | elsif Nkind (N) = N_With_Clause then | |
1524 | Nam := Name (N); | |
1525 | end if; | |
1526 | ||
1527 | if Present (Nam) | |
1528 | and then Is_Entity_Name (Nam) | |
1529 | and then Present (Entity (Nam)) | |
1530 | and then Is_Ignored_Ghost_Entity (Entity (Nam)) | |
1531 | then | |
1532 | Set_Is_Ignored_Ghost_Node (N); | |
1533 | Record_Ignored_Ghost_Node (N); | |
1534 | end if; | |
1535 | end Mark_Ghost_Clause; | |
1536 | ||
d65a80fd HK |
1537 | ------------------------------------ |
1538 | -- Mark_Ghost_Declaration_Or_Body -- | |
1539 | ------------------------------------ | |
1540 | ||
1541 | procedure Mark_Ghost_Declaration_Or_Body | |
1542 | (N : Node_Id; | |
1543 | Mode : Name_Id) | |
1544 | is | |
1545 | Id : constant Entity_Id := Defining_Entity (N); | |
1546 | ||
1547 | Mark_Formals : Boolean := False; | |
1548 | Param : Node_Id; | |
1549 | Param_Id : Entity_Id; | |
1550 | ||
1551 | begin | |
1552 | -- Mark the related node and its entity | |
1553 | ||
1554 | if Mode = Name_Check then | |
1555 | Mark_Formals := True; | |
1556 | Set_Is_Checked_Ghost_Entity (Id); | |
1557 | ||
1558 | elsif Mode = Name_Ignore then | |
1559 | Mark_Formals := True; | |
1560 | Set_Is_Ignored_Ghost_Entity (Id); | |
1561 | Set_Is_Ignored_Ghost_Node (N); | |
980f94b7 | 1562 | Record_Ignored_Ghost_Node (N); |
d65a80fd HK |
1563 | end if; |
1564 | ||
1565 | -- Mark all formal parameters when the related node denotes a subprogram | |
1566 | -- or a body. The traversal is performed via the specification because | |
1567 | -- the related subprogram or body may be unanalyzed. | |
1568 | ||
1569 | -- ??? could extra formal parameters cause a Ghost leak? | |
1570 | ||
1571 | if Mark_Formals | |
1572 | and then Nkind_In (N, N_Abstract_Subprogram_Declaration, | |
1573 | N_Formal_Abstract_Subprogram_Declaration, | |
1574 | N_Formal_Concrete_Subprogram_Declaration, | |
1575 | N_Generic_Subprogram_Declaration, | |
1576 | N_Subprogram_Body, | |
1577 | N_Subprogram_Body_Stub, | |
1578 | N_Subprogram_Declaration, | |
1579 | N_Subprogram_Renaming_Declaration) | |
1580 | then | |
1581 | Param := First (Parameter_Specifications (Specification (N))); | |
1582 | while Present (Param) loop | |
1583 | Param_Id := Defining_Entity (Param); | |
1584 | ||
1585 | if Mode = Name_Check then | |
1586 | Set_Is_Checked_Ghost_Entity (Param_Id); | |
1587 | ||
1588 | elsif Mode = Name_Ignore then | |
1589 | Set_Is_Ignored_Ghost_Entity (Param_Id); | |
1590 | end if; | |
1591 | ||
1592 | Next (Param); | |
1593 | end loop; | |
1594 | end if; | |
1595 | end Mark_Ghost_Declaration_Or_Body; | |
1596 | ||
1597 | ----------------------- | |
1598 | -- Mark_Ghost_Pragma -- | |
1599 | ----------------------- | |
1600 | ||
1601 | procedure Mark_Ghost_Pragma | |
1602 | (N : Node_Id; | |
1603 | Id : Entity_Id) | |
1604 | is | |
1605 | begin | |
1606 | -- A pragma becomes Ghost when it encloses a Ghost entity or relates to | |
1607 | -- a Ghost entity. | |
1608 | ||
1609 | if Is_Checked_Ghost_Entity (Id) then | |
1610 | Set_Is_Checked_Ghost_Pragma (N); | |
1611 | ||
1612 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1613 | Set_Is_Ignored_Ghost_Pragma (N); | |
1614 | Set_Is_Ignored_Ghost_Node (N); | |
980f94b7 | 1615 | Record_Ignored_Ghost_Node (N); |
d65a80fd HK |
1616 | end if; |
1617 | end Mark_Ghost_Pragma; | |
1618 | ||
1619 | ------------------------- | |
1620 | -- Mark_Ghost_Renaming -- | |
1621 | ------------------------- | |
1622 | ||
1623 | procedure Mark_Ghost_Renaming | |
1624 | (N : Node_Id; | |
1625 | Id : Entity_Id) | |
1626 | is | |
1627 | Policy : Name_Id := No_Name; | |
1628 | ||
1629 | begin | |
1630 | -- A renaming becomes Ghost when it renames a Ghost entity | |
1631 | ||
1632 | if Is_Checked_Ghost_Entity (Id) then | |
1633 | Policy := Name_Check; | |
1634 | ||
1635 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1636 | Policy := Name_Ignore; | |
241ebe89 | 1637 | end if; |
d65a80fd HK |
1638 | |
1639 | Mark_Ghost_Declaration_Or_Body (N, Policy); | |
1640 | end Mark_Ghost_Renaming; | |
241ebe89 | 1641 | |
9057bd6a HK |
1642 | ------------------------ |
1643 | -- Name_To_Ghost_Mode -- | |
1644 | ------------------------ | |
1645 | ||
1646 | function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is | |
1647 | begin | |
1648 | if Mode = Name_Check then | |
1649 | return Check; | |
1650 | ||
1651 | elsif Mode = Name_Ignore then | |
1652 | return Ignore; | |
1653 | ||
1654 | -- Otherwise the mode must denote one of the following: | |
1655 | -- | |
1656 | -- * Disable indicates that the Ghost policy in effect is Disable | |
1657 | -- | |
1658 | -- * None or No_Name indicates that the associated construct is not | |
1659 | -- subject to any Ghost annotation. | |
1660 | ||
1661 | else | |
1662 | pragma Assert (Nam_In (Mode, Name_Disable, Name_None, No_Name)); | |
1663 | return None; | |
1664 | end if; | |
1665 | end Name_To_Ghost_Mode; | |
1666 | ||
980f94b7 HK |
1667 | ------------------------------- |
1668 | -- Record_Ignored_Ghost_Node -- | |
1669 | ------------------------------- | |
8636f52f | 1670 | |
980f94b7 | 1671 | procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id) is |
8636f52f | 1672 | begin |
980f94b7 HK |
1673 | -- Save all "top level" ignored Ghost nodes which can be safely replaced |
1674 | -- with a null statement. Note that there is need to save other kinds of | |
1675 | -- nodes because those will always be enclosed by some top level ignored | |
1676 | -- Ghost node. | |
1677 | ||
1678 | if Is_Body (N) | |
1679 | or else Is_Declaration (N) | |
1680 | or else Nkind (N) in N_Generic_Instantiation | |
1681 | or else Nkind (N) in N_Push_Pop_xxx_Label | |
1682 | or else Nkind (N) in N_Raise_xxx_Error | |
1683 | or else Nkind (N) in N_Representation_Clause | |
923ecd0e HK |
1684 | or else Nkind (N) in N_Statement_Other_Than_Procedure_Call |
1685 | or else Nkind_In (N, N_Call_Marker, | |
980f94b7 HK |
1686 | N_Freeze_Entity, |
1687 | N_Freeze_Generic_Entity, | |
1688 | N_Itype_Reference, | |
1689 | N_Pragma, | |
1690 | N_Procedure_Call_Statement, | |
1691 | N_Use_Package_Clause, | |
1692 | N_Use_Type_Clause, | |
1693 | N_Variable_Reference_Marker, | |
1694 | N_With_Clause) | |
1695 | then | |
1696 | -- Only ignored Ghost nodes must be recorded in the table | |
8636f52f | 1697 | |
980f94b7 HK |
1698 | pragma Assert (Is_Ignored_Ghost_Node (N)); |
1699 | Ignored_Ghost_Nodes.Append (N); | |
1700 | end if; | |
1701 | end Record_Ignored_Ghost_Node; | |
8636f52f HK |
1702 | |
1703 | ------------------------------- | |
1704 | -- Remove_Ignored_Ghost_Code -- | |
1705 | ------------------------------- | |
1706 | ||
1707 | procedure Remove_Ignored_Ghost_Code is | |
980f94b7 HK |
1708 | procedure Remove_Ignored_Ghost_Node (N : Node_Id); |
1709 | -- Eliminate ignored Ghost node N from the tree | |
6e9e35e1 | 1710 | |
980f94b7 HK |
1711 | ------------------------------- |
1712 | -- Remove_Ignored_Ghost_Node -- | |
1713 | ------------------------------- | |
6e9e35e1 | 1714 | |
980f94b7 HK |
1715 | procedure Remove_Ignored_Ghost_Node (N : Node_Id) is |
1716 | begin | |
1717 | -- The generation and processing of ignored Ghost nodes may cause the | |
1718 | -- same node to be saved multiple times. Reducing the number of saves | |
1719 | -- to one involves costly solutions such as a hash table or the use | |
1720 | -- of a flag shared by all nodes. To solve this problem, the removal | |
1721 | -- machinery allows for multiple saves, but does not eliminate a node | |
1722 | -- which has already been eliminated. | |
8636f52f | 1723 | |
980f94b7 HK |
1724 | if Nkind (N) = N_Null_Statement then |
1725 | null; | |
8636f52f | 1726 | |
980f94b7 | 1727 | -- Otherwise the ignored Ghost node must be eliminated |
8636f52f | 1728 | |
980f94b7 HK |
1729 | else |
1730 | -- Only ignored Ghost nodes must be eliminated from the tree | |
8636f52f | 1731 | |
980f94b7 | 1732 | pragma Assert (Is_Ignored_Ghost_Node (N)); |
8636f52f | 1733 | |
980f94b7 HK |
1734 | -- Eliminate the node by rewriting it into null. Another option |
1735 | -- is to remove it from the tree, however multiple corner cases | |
1736 | -- emerge which have be dealt individually. | |
8636f52f | 1737 | |
980f94b7 | 1738 | Rewrite (N, Make_Null_Statement (Sloc (N))); |
8636f52f | 1739 | |
980f94b7 | 1740 | -- Eliminate any aspects hanging off the ignored Ghost node |
8636f52f | 1741 | |
980f94b7 HK |
1742 | Remove_Aspects (N); |
1743 | end if; | |
1744 | end Remove_Ignored_Ghost_Node; | |
8636f52f HK |
1745 | |
1746 | -- Start of processing for Remove_Ignored_Ghost_Code | |
1747 | ||
1748 | begin | |
980f94b7 HK |
1749 | for Index in Ignored_Ghost_Nodes.First .. Ignored_Ghost_Nodes.Last loop |
1750 | Remove_Ignored_Ghost_Node (Ignored_Ghost_Nodes.Table (Index)); | |
8636f52f HK |
1751 | end loop; |
1752 | end Remove_Ignored_Ghost_Code; | |
1753 | ||
9057bd6a HK |
1754 | -------------------------- |
1755 | -- Restore_Ghost_Region -- | |
1756 | -------------------------- | |
d65a80fd | 1757 | |
9057bd6a | 1758 | procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is |
d65a80fd | 1759 | begin |
9057bd6a HK |
1760 | Ghost_Mode := Mode; |
1761 | Ignored_Ghost_Region := N; | |
1762 | end Restore_Ghost_Region; | |
d65a80fd | 1763 | |
8636f52f HK |
1764 | -------------------- |
1765 | -- Set_Ghost_Mode -- | |
1766 | -------------------- | |
1767 | ||
f9a8f910 | 1768 | procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is |
d65a80fd HK |
1769 | procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); |
1770 | -- Install the Ghost mode of entity Id | |
8636f52f | 1771 | |
d65a80fd HK |
1772 | -------------------------------- |
1773 | -- Set_Ghost_Mode_From_Entity -- | |
1774 | -------------------------------- | |
8636f52f | 1775 | |
d65a80fd | 1776 | procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is |
8636f52f | 1777 | begin |
d65a80fd HK |
1778 | if Is_Checked_Ghost_Entity (Id) then |
1779 | Install_Ghost_Mode (Check); | |
1780 | elsif Is_Ignored_Ghost_Entity (Id) then | |
1781 | Install_Ghost_Mode (Ignore); | |
1782 | else | |
1783 | Install_Ghost_Mode (None); | |
8636f52f | 1784 | end if; |
d65a80fd | 1785 | end Set_Ghost_Mode_From_Entity; |
8636f52f HK |
1786 | |
1787 | -- Local variables | |
1788 | ||
d65a80fd | 1789 | Id : Entity_Id; |
8636f52f HK |
1790 | |
1791 | -- Start of processing for Set_Ghost_Mode | |
1792 | ||
1793 | begin | |
d65a80fd HK |
1794 | -- The Ghost mode of an assignment statement depends on the Ghost mode |
1795 | -- of the target. | |
8636f52f | 1796 | |
d65a80fd HK |
1797 | if Nkind (N) = N_Assignment_Statement then |
1798 | Id := Ghost_Entity (Name (N)); | |
8636f52f | 1799 | |
d65a80fd HK |
1800 | if Present (Id) then |
1801 | Set_Ghost_Mode_From_Entity (Id); | |
8636f52f HK |
1802 | end if; |
1803 | ||
d65a80fd HK |
1804 | -- The Ghost mode of a body or a declaration depends on the Ghost mode |
1805 | -- of its defining entity. | |
8636f52f | 1806 | |
d65a80fd HK |
1807 | elsif Is_Body (N) or else Is_Declaration (N) then |
1808 | Set_Ghost_Mode_From_Entity (Defining_Entity (N)); | |
8636f52f | 1809 | |
d65a80fd | 1810 | -- The Ghost mode of an entity depends on the entity itself |
8636f52f | 1811 | |
d65a80fd HK |
1812 | elsif Nkind (N) in N_Entity then |
1813 | Set_Ghost_Mode_From_Entity (N); | |
8636f52f | 1814 | |
d65a80fd HK |
1815 | -- The Ghost mode of a [generic] freeze node depends on the Ghost mode |
1816 | -- of the entity being frozen. | |
1817 | ||
1818 | elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then | |
1819 | Set_Ghost_Mode_From_Entity (Entity (N)); | |
241ebe89 | 1820 | |
d65a80fd HK |
1821 | -- The Ghost mode of a pragma depends on the associated entity. The |
1822 | -- property is encoded in the pragma itself. | |
241ebe89 | 1823 | |
d65a80fd HK |
1824 | elsif Nkind (N) = N_Pragma then |
1825 | if Is_Checked_Ghost_Pragma (N) then | |
1826 | Install_Ghost_Mode (Check); | |
1827 | elsif Is_Ignored_Ghost_Pragma (N) then | |
1828 | Install_Ghost_Mode (Ignore); | |
241ebe89 | 1829 | else |
d65a80fd | 1830 | Install_Ghost_Mode (None); |
8636f52f | 1831 | end if; |
241ebe89 | 1832 | |
d65a80fd HK |
1833 | -- The Ghost mode of a procedure call depends on the Ghost mode of the |
1834 | -- procedure being invoked. | |
241ebe89 | 1835 | |
d65a80fd HK |
1836 | elsif Nkind (N) = N_Procedure_Call_Statement then |
1837 | Id := Ghost_Entity (Name (N)); | |
8636f52f | 1838 | |
d65a80fd HK |
1839 | if Present (Id) then |
1840 | Set_Ghost_Mode_From_Entity (Id); | |
1841 | end if; | |
8636f52f | 1842 | end if; |
d65a80fd | 1843 | end Set_Ghost_Mode; |
8636f52f HK |
1844 | |
1845 | ------------------------- | |
1846 | -- Set_Is_Ghost_Entity -- | |
1847 | ------------------------- | |
1848 | ||
1849 | procedure Set_Is_Ghost_Entity (Id : Entity_Id) is | |
1850 | Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); | |
8636f52f HK |
1851 | begin |
1852 | if Policy = Name_Check then | |
1853 | Set_Is_Checked_Ghost_Entity (Id); | |
8636f52f HK |
1854 | elsif Policy = Name_Ignore then |
1855 | Set_Is_Ignored_Ghost_Entity (Id); | |
1856 | end if; | |
1857 | end Set_Is_Ghost_Entity; | |
1858 | ||
1859 | end Ghost; |