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