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