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