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