1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- G H O S T -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2014-2015, 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; use Alloc; 27with Aspects; use Aspects; 28with Atree; use Atree; 29with Einfo; use Einfo; 30with Elists; use Elists; 31with Errout; use Errout; 32with Lib; use Lib; 33with Namet; use Namet; 34with Nlists; use Nlists; 35with Nmake; use Nmake; 36with Opt; use Opt; 37with Sem; use Sem; 38with Sem_Aux; use Sem_Aux; 39with Sem_Eval; use Sem_Eval; 40with Sem_Res; use Sem_Res; 41with Sem_Util; use Sem_Util; 42with Sinfo; use Sinfo; 43with Snames; use Snames; 44with Table; 45 46package body Ghost is 47 48 -- The following table contains the N_Compilation_Unit node for a unit that 49 -- is either subject to pragma Ghost with policy Ignore or contains ignored 50 -- Ghost code. The table is used in the removal of ignored Ghost code from 51 -- units. 52 53 package Ignored_Ghost_Units is new Table.Table ( 54 Table_Component_Type => Node_Id, 55 Table_Index_Type => Int, 56 Table_Low_Bound => 0, 57 Table_Initial => Alloc.Ignored_Ghost_Units_Initial, 58 Table_Increment => Alloc.Ignored_Ghost_Units_Increment, 59 Table_Name => "Ignored_Ghost_Units"); 60 61 ----------------------- 62 -- Local Subprograms -- 63 ----------------------- 64 65 procedure Propagate_Ignored_Ghost_Code (N : Node_Id); 66 -- Subsidiary to Set_Ghost_Mode_xxx. Signal all enclosing scopes that they 67 -- now contain ignored Ghost code. Add the compilation unit containing N to 68 -- table Ignored_Ghost_Units for post processing. 69 70 ---------------------------- 71 -- Add_Ignored_Ghost_Unit -- 72 ---------------------------- 73 74 procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is 75 begin 76 pragma Assert (Nkind (Unit) = N_Compilation_Unit); 77 78 -- Avoid duplicates in the table as pruning the same unit more than once 79 -- is wasteful. Since ignored Ghost code tends to be grouped up, check 80 -- the contents of the table in reverse. 81 82 for Index in reverse Ignored_Ghost_Units.First .. 83 Ignored_Ghost_Units.Last 84 loop 85 -- If the unit is already present in the table, do not add it again 86 87 if Unit = Ignored_Ghost_Units.Table (Index) then 88 return; 89 end if; 90 end loop; 91 92 -- If we get here, then this is the first time the unit is being added 93 94 Ignored_Ghost_Units.Append (Unit); 95 end Add_Ignored_Ghost_Unit; 96 97 ---------------------------- 98 -- Check_Ghost_Completion -- 99 ---------------------------- 100 101 procedure Check_Ghost_Completion 102 (Partial_View : Entity_Id; 103 Full_View : Entity_Id) 104 is 105 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 106 107 begin 108 -- The Ghost policy in effect at the point of declaration and at the 109 -- point of completion must match (SPARK RM 6.9(15)). 110 111 if Is_Checked_Ghost_Entity (Partial_View) 112 and then Policy = Name_Ignore 113 then 114 Error_Msg_Sloc := Sloc (Full_View); 115 116 Error_Msg_N ("incompatible ghost policies in effect", Partial_View); 117 Error_Msg_N ("\& declared with ghost policy Check", Partial_View); 118 Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); 119 120 elsif Is_Ignored_Ghost_Entity (Partial_View) 121 and then Policy = Name_Check 122 then 123 Error_Msg_Sloc := Sloc (Full_View); 124 125 Error_Msg_N ("incompatible ghost policies in effect", Partial_View); 126 Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View); 127 Error_Msg_N ("\& completed # with ghost policy Check", Partial_View); 128 end if; 129 end Check_Ghost_Completion; 130 131 ------------------------- 132 -- Check_Ghost_Context -- 133 ------------------------- 134 135 procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is 136 procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id); 137 -- Verify that the Ghost policy at the point of declaration of entity Id 138 -- matches the policy at the point of reference. If this is not the case 139 -- emit an error at Err_N. 140 141 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; 142 -- Determine whether node Context denotes a Ghost-friendly context where 143 -- a Ghost entity can safely reside. 144 145 ------------------------- 146 -- Is_OK_Ghost_Context -- 147 ------------------------- 148 149 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is 150 function Is_Ghost_Declaration (Decl : Node_Id) return Boolean; 151 -- Determine whether node Decl is a Ghost declaration or appears 152 -- within a Ghost declaration. 153 154 function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean; 155 -- Determine whether statement or pragma N is Ghost or appears within 156 -- a Ghost statement or pragma. To qualify as such, N must either 157 -- 1) Occur within a ghost subprogram or package 158 -- 2) Denote a call to a ghost procedure 159 -- 3) Denote an assignment statement whose target is a ghost 160 -- variable. 161 -- 4) Denote a pragma that mentions a ghost entity 162 163 -------------------------- 164 -- Is_Ghost_Declaration -- 165 -------------------------- 166 167 function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is 168 Par : Node_Id; 169 Subp_Decl : Node_Id; 170 Subp_Id : Entity_Id; 171 172 begin 173 -- Climb the parent chain looking for an object declaration 174 175 Par := Decl; 176 while Present (Par) loop 177 if Is_Declaration (Par) then 178 179 -- A declaration is Ghost when it appears within a Ghost 180 -- package or subprogram. 181 182 if Ghost_Mode > None then 183 return True; 184 185 -- Otherwise the declaration may not have been analyzed yet, 186 -- determine whether it is subject to aspect/pragma Ghost. 187 188 else 189 return Is_Subject_To_Ghost (Par); 190 end if; 191 192 -- Special cases 193 194 -- A reference to a Ghost entity may appear as the default 195 -- expression of a formal parameter of a subprogram body. This 196 -- context must be treated as suitable because the relation 197 -- between the spec and the body has not been established and 198 -- the body is not marked as Ghost yet. The real check was 199 -- performed on the spec. 200 201 elsif Nkind (Par) = N_Parameter_Specification 202 and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body 203 then 204 return True; 205 206 -- References to Ghost entities may be relocated in internally 207 -- generated bodies. 208 209 elsif Nkind (Par) = N_Subprogram_Body 210 and then not Comes_From_Source (Par) 211 then 212 Subp_Id := Corresponding_Spec (Par); 213 214 -- The original context is an expression function that has 215 -- been split into a spec and a body. The context is OK as 216 -- long as the the initial declaration is Ghost. 217 218 if Present (Subp_Id) then 219 Subp_Decl := 220 Original_Node (Unit_Declaration_Node (Subp_Id)); 221 222 if Nkind (Subp_Decl) = N_Expression_Function then 223 return Is_Subject_To_Ghost (Subp_Decl); 224 end if; 225 end if; 226 227 -- Otherwise this is either an internal body or an internal 228 -- completion. Both are OK because the real check was done 229 -- before expansion activities. 230 231 return True; 232 end if; 233 234 -- Prevent the search from going too far 235 236 if Is_Body_Or_Package_Declaration (Par) then 237 return False; 238 end if; 239 240 Par := Parent (Par); 241 end loop; 242 243 return False; 244 end Is_Ghost_Declaration; 245 246 ---------------------------------- 247 -- Is_Ghost_Statement_Or_Pragma -- 248 ---------------------------------- 249 250 function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is 251 function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean; 252 -- Determine whether an arbitrary node denotes a reference to a 253 -- Ghost entity. 254 255 ------------------------------- 256 -- Is_Ghost_Entity_Reference -- 257 ------------------------------- 258 259 function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is 260 Ref : Node_Id; 261 262 begin 263 -- When the reference extracts a subcomponent, recover the 264 -- related object (SPARK RM 6.9(1)). 265 266 Ref := N; 267 while Nkind_In (Ref, N_Explicit_Dereference, 268 N_Indexed_Component, 269 N_Selected_Component, 270 N_Slice) 271 loop 272 Ref := Prefix (Ref); 273 end loop; 274 275 return 276 Is_Entity_Name (Ref) 277 and then Present (Entity (Ref)) 278 and then Is_Ghost_Entity (Entity (Ref)); 279 end Is_Ghost_Entity_Reference; 280 281 -- Local variables 282 283 Arg : Node_Id; 284 Stmt : Node_Id; 285 286 -- Start of processing for Is_Ghost_Statement_Or_Pragma 287 288 begin 289 if Nkind (N) = N_Pragma then 290 291 -- A pragma is Ghost when it appears within a Ghost package or 292 -- subprogram. 293 294 if Ghost_Mode > None then 295 return True; 296 end if; 297 298 -- A pragma is Ghost when it mentions a Ghost entity 299 300 Arg := First (Pragma_Argument_Associations (N)); 301 while Present (Arg) loop 302 if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then 303 return True; 304 end if; 305 306 Next (Arg); 307 end loop; 308 end if; 309 310 Stmt := N; 311 while Present (Stmt) loop 312 if Is_Statement (Stmt) then 313 314 -- A statement is Ghost when it appears within a Ghost 315 -- package or subprogram. 316 317 if Ghost_Mode > None then 318 return True; 319 320 -- An assignment statement or a procedure call is Ghost when 321 -- the name denotes a Ghost entity. 322 323 elsif Nkind_In (Stmt, N_Assignment_Statement, 324 N_Procedure_Call_Statement) 325 then 326 return Is_Ghost_Entity_Reference (Name (Stmt)); 327 end if; 328 329 -- Prevent the search from going too far 330 331 elsif Is_Body_Or_Package_Declaration (Stmt) then 332 return False; 333 end if; 334 335 Stmt := Parent (Stmt); 336 end loop; 337 338 return False; 339 end Is_Ghost_Statement_Or_Pragma; 340 341 -- Start of processing for Is_OK_Ghost_Context 342 343 begin 344 -- The Ghost entity appears within an assertion expression 345 346 if In_Assertion_Expr > 0 then 347 return True; 348 349 -- The Ghost entity is part of a declaration or its completion 350 351 elsif Is_Ghost_Declaration (Context) then 352 return True; 353 354 -- The Ghost entity is referenced within a Ghost statement 355 356 elsif Is_Ghost_Statement_Or_Pragma (Context) then 357 return True; 358 359 -- Routine Expand_Record_Extension creates a parent subtype without 360 -- inserting it into the tree. There is no good way of recognizing 361 -- this special case as there is no parent. Try to approximate the 362 -- context. 363 364 elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then 365 return True; 366 367 else 368 return False; 369 end if; 370 end Is_OK_Ghost_Context; 371 372 ------------------------ 373 -- Check_Ghost_Policy -- 374 ------------------------ 375 376 procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is 377 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 378 379 begin 380 -- The Ghost policy in effect a the point of declaration and at the 381 -- point of use must match (SPARK RM 6.9(14)). 382 383 if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then 384 Error_Msg_Sloc := Sloc (Err_N); 385 386 Error_Msg_N ("incompatible ghost policies in effect", Err_N); 387 Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); 388 Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); 389 390 elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then 391 Error_Msg_Sloc := Sloc (Err_N); 392 393 Error_Msg_N ("incompatible ghost policies in effect", Err_N); 394 Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); 395 Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); 396 end if; 397 end Check_Ghost_Policy; 398 399 -- Start of processing for Check_Ghost_Context 400 401 begin 402 -- Once it has been established that the reference to the Ghost entity 403 -- is within a suitable context, ensure that the policy at the point of 404 -- declaration and at the point of use match. 405 406 if Is_OK_Ghost_Context (Ghost_Ref) then 407 Check_Ghost_Policy (Ghost_Id, Ghost_Ref); 408 409 -- Otherwise the Ghost entity appears in a non-Ghost context and affects 410 -- its behavior or value. 411 412 else 413 Error_Msg_N 414 ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", 415 Ghost_Ref); 416 end if; 417 end Check_Ghost_Context; 418 419 ---------------------------- 420 -- Check_Ghost_Derivation -- 421 ---------------------------- 422 423 procedure Check_Ghost_Derivation (Typ : Entity_Id) is 424 Parent_Typ : constant Entity_Id := Etype (Typ); 425 Iface : Entity_Id; 426 Iface_Elmt : Elmt_Id; 427 428 begin 429 -- Allow untagged derivations from predefined types such as Integer as 430 -- those are not Ghost by definition. 431 432 if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then 433 null; 434 435 -- The parent type of a Ghost type extension must be Ghost 436 437 elsif not Is_Ghost_Entity (Parent_Typ) then 438 Error_Msg_N ("type extension & cannot be ghost", Typ); 439 Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ); 440 return; 441 end if; 442 443 -- All progenitors (if any) must be Ghost as well 444 445 if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then 446 Iface_Elmt := First_Elmt (Interfaces (Typ)); 447 while Present (Iface_Elmt) loop 448 Iface := Node (Iface_Elmt); 449 450 if not Is_Ghost_Entity (Iface) then 451 Error_Msg_N ("type extension & cannot be ghost", Typ); 452 Error_Msg_NE ("\interface type & is not ghost", Typ, Iface); 453 return; 454 end if; 455 456 Next_Elmt (Iface_Elmt); 457 end loop; 458 end if; 459 end Check_Ghost_Derivation; 460 461 -------------------------------- 462 -- Implements_Ghost_Interface -- 463 -------------------------------- 464 465 function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is 466 Iface_Elmt : Elmt_Id; 467 468 begin 469 -- Traverse the list of interfaces looking for a Ghost interface 470 471 if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then 472 Iface_Elmt := First_Elmt (Interfaces (Typ)); 473 while Present (Iface_Elmt) loop 474 if Is_Ghost_Entity (Node (Iface_Elmt)) then 475 return True; 476 end if; 477 478 Next_Elmt (Iface_Elmt); 479 end loop; 480 end if; 481 482 return False; 483 end Implements_Ghost_Interface; 484 485 ---------------- 486 -- Initialize -- 487 ---------------- 488 489 procedure Initialize is 490 begin 491 Ignored_Ghost_Units.Init; 492 end Initialize; 493 494 --------------------- 495 -- Is_Ghost_Entity -- 496 --------------------- 497 498 function Is_Ghost_Entity (Id : Entity_Id) return Boolean is 499 begin 500 return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id); 501 end Is_Ghost_Entity; 502 503 ------------------------- 504 -- Is_Subject_To_Ghost -- 505 ------------------------- 506 507 function Is_Subject_To_Ghost (N : Node_Id) return Boolean is 508 function Enables_Ghostness (Arg : Node_Id) return Boolean; 509 -- Determine whether aspect or pragma argument Arg enables "ghostness" 510 511 ----------------------- 512 -- Enables_Ghostness -- 513 ----------------------- 514 515 function Enables_Ghostness (Arg : Node_Id) return Boolean is 516 Expr : Node_Id; 517 518 begin 519 Expr := Arg; 520 521 if Nkind (Expr) = N_Pragma_Argument_Association then 522 Expr := Get_Pragma_Arg (Expr); 523 end if; 524 525 -- Determine whether the expression of the aspect is static and 526 -- denotes True. 527 528 if Present (Expr) then 529 Preanalyze_And_Resolve (Expr); 530 531 return 532 Is_OK_Static_Expression (Expr) 533 and then Is_True (Expr_Value (Expr)); 534 535 -- Otherwise Ghost defaults to True 536 537 else 538 return True; 539 end if; 540 end Enables_Ghostness; 541 542 -- Local variables 543 544 Id : constant Entity_Id := Defining_Entity (N); 545 Asp : Node_Id; 546 Decl : Node_Id; 547 Prev_Id : Entity_Id; 548 549 -- Start of processing for Is_Subject_To_Ghost 550 551 begin 552 -- The related entity of the declaration has not been analyzed yet, do 553 -- not inspect its attributes. 554 555 if Ekind (Id) = E_Void then 556 null; 557 558 elsif Is_Ghost_Entity (Id) then 559 return True; 560 561 -- The completion of a type or a constant is not fully analyzed when the 562 -- reference to the Ghost entity is resolved. Because the completion is 563 -- not marked as Ghost yet, inspect the partial view. 564 565 elsif Is_Record_Type (Id) 566 or else Ekind (Id) = E_Constant 567 or else (Nkind (N) = N_Object_Declaration 568 and then Constant_Present (N)) 569 then 570 Prev_Id := Incomplete_Or_Partial_View (Id); 571 572 if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then 573 return True; 574 end if; 575 end if; 576 577 -- Examine the aspect specifications (if any) looking for aspect Ghost 578 579 if Permits_Aspect_Specifications (N) then 580 Asp := First (Aspect_Specifications (N)); 581 while Present (Asp) loop 582 if Chars (Identifier (Asp)) = Name_Ghost then 583 return Enables_Ghostness (Expression (Asp)); 584 end if; 585 586 Next (Asp); 587 end loop; 588 end if; 589 590 Decl := Empty; 591 592 -- When the context is a [generic] package declaration, pragma Ghost 593 -- resides in the visible declarations. 594 595 if Nkind_In (N, N_Generic_Package_Declaration, 596 N_Package_Declaration) 597 then 598 Decl := First (Visible_Declarations (Specification (N))); 599 600 -- When the context is a package or a subprogram body, pragma Ghost 601 -- resides in the declarative part. 602 603 elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then 604 Decl := First (Declarations (N)); 605 606 -- Otherwise pragma Ghost appears in the declarations following N 607 608 elsif Is_List_Member (N) then 609 Decl := Next (N); 610 end if; 611 612 while Present (Decl) loop 613 if Nkind (Decl) = N_Pragma 614 and then Pragma_Name (Decl) = Name_Ghost 615 then 616 return 617 Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); 618 619 -- A source construct ends the region where pragma Ghost may appear, 620 -- stop the traversal. 621 622 elsif Comes_From_Source (Decl) then 623 exit; 624 end if; 625 626 Next (Decl); 627 end loop; 628 629 return False; 630 end Is_Subject_To_Ghost; 631 632 ---------- 633 -- Lock -- 634 ---------- 635 636 procedure Lock is 637 begin 638 Ignored_Ghost_Units.Locked := True; 639 Ignored_Ghost_Units.Release; 640 end Lock; 641 642 ---------------------------------- 643 -- Propagate_Ignored_Ghost_Code -- 644 ---------------------------------- 645 646 procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is 647 Nod : Node_Id; 648 Scop : Entity_Id; 649 650 begin 651 -- Traverse the parent chain looking for blocks, packages and 652 -- subprograms or their respective bodies. 653 654 Nod := Parent (N); 655 while Present (Nod) loop 656 Scop := Empty; 657 658 if Nkind (Nod) = N_Block_Statement then 659 Scop := Entity (Identifier (Nod)); 660 661 elsif Nkind_In (Nod, N_Package_Body, 662 N_Package_Declaration, 663 N_Subprogram_Body, 664 N_Subprogram_Declaration) 665 then 666 Scop := Defining_Entity (Nod); 667 end if; 668 669 -- The current node denotes a scoping construct 670 671 if Present (Scop) then 672 673 -- Stop the traversal when the scope already contains ignored 674 -- Ghost code as all enclosing scopes have already been marked. 675 676 if Contains_Ignored_Ghost_Code (Scop) then 677 exit; 678 679 -- Otherwise mark this scope and keep climbing 680 681 else 682 Set_Contains_Ignored_Ghost_Code (Scop); 683 end if; 684 end if; 685 686 Nod := Parent (Nod); 687 end loop; 688 689 -- The unit containing the ignored Ghost code must be post processed 690 -- before invoking the back end. 691 692 Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N))); 693 end Propagate_Ignored_Ghost_Code; 694 695 ------------------------------- 696 -- Remove_Ignored_Ghost_Code -- 697 ------------------------------- 698 699 procedure Remove_Ignored_Ghost_Code is 700 procedure Prune_Tree (Root : Node_Id); 701 -- Remove all code marked as ignored Ghost from the tree of denoted by 702 -- Root. 703 704 ---------------- 705 -- Prune_Tree -- 706 ---------------- 707 708 procedure Prune_Tree (Root : Node_Id) is 709 procedure Prune (N : Node_Id); 710 -- Remove a given node from the tree by rewriting it into null 711 712 function Prune_Node (N : Node_Id) return Traverse_Result; 713 -- Determine whether node N denotes an ignored Ghost construct. If 714 -- this is the case, rewrite N as a null statement. See the body for 715 -- special cases. 716 717 ----------- 718 -- Prune -- 719 ----------- 720 721 procedure Prune (N : Node_Id) is 722 begin 723 -- Destroy any aspects that may be associated with the node 724 725 if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then 726 Remove_Aspects (N); 727 end if; 728 729 Rewrite (N, Make_Null_Statement (Sloc (N))); 730 end Prune; 731 732 ---------------- 733 -- Prune_Node -- 734 ---------------- 735 736 function Prune_Node (N : Node_Id) return Traverse_Result is 737 Id : Entity_Id; 738 739 begin 740 -- The node is either declared as ignored Ghost or is a byproduct 741 -- of expansion. Destroy it and stop the traversal on this branch. 742 743 if Is_Ignored_Ghost_Node (N) then 744 Prune (N); 745 return Skip; 746 747 -- Scoping constructs such as blocks, packages, subprograms and 748 -- bodies offer some flexibility with respect to pruning. 749 750 elsif Nkind_In (N, N_Block_Statement, 751 N_Package_Body, 752 N_Package_Declaration, 753 N_Subprogram_Body, 754 N_Subprogram_Declaration) 755 then 756 if Nkind (N) = N_Block_Statement then 757 Id := Entity (Identifier (N)); 758 else 759 Id := Defining_Entity (N); 760 end if; 761 762 -- The scoping construct contains both living and ignored Ghost 763 -- code, let the traversal prune all relevant nodes. 764 765 if Contains_Ignored_Ghost_Code (Id) then 766 return OK; 767 768 -- Otherwise the construct contains only living code and should 769 -- not be pruned. 770 771 else 772 return Skip; 773 end if; 774 775 -- Otherwise keep searching for ignored Ghost nodes 776 777 else 778 return OK; 779 end if; 780 end Prune_Node; 781 782 procedure Prune_Nodes is new Traverse_Proc (Prune_Node); 783 784 -- Start of processing for Prune_Tree 785 786 begin 787 Prune_Nodes (Root); 788 end Prune_Tree; 789 790 -- Start of processing for Remove_Ignored_Ghost_Code 791 792 begin 793 for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop 794 Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index))); 795 end loop; 796 end Remove_Ignored_Ghost_Code; 797 798 -------------------- 799 -- Set_Ghost_Mode -- 800 -------------------- 801 802 procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is 803 procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); 804 -- Set the value of global variable Ghost_Mode depending on the mode of 805 -- entity Id. 806 807 procedure Set_Ghost_Mode_From_Policy; 808 -- Set the value of global variable Ghost_Mode depending on the current 809 -- Ghost policy in effect. 810 811 -------------------------------- 812 -- Set_Ghost_Mode_From_Entity -- 813 -------------------------------- 814 815 procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is 816 begin 817 if Is_Checked_Ghost_Entity (Id) then 818 Ghost_Mode := Check; 819 820 elsif Is_Ignored_Ghost_Entity (Id) then 821 Ghost_Mode := Ignore; 822 823 Set_Is_Ignored_Ghost_Node (N); 824 Propagate_Ignored_Ghost_Code (N); 825 end if; 826 end Set_Ghost_Mode_From_Entity; 827 828 -------------------------------- 829 -- Set_Ghost_Mode_From_Policy -- 830 -------------------------------- 831 832 procedure Set_Ghost_Mode_From_Policy is 833 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 834 835 begin 836 if Policy = Name_Check then 837 Ghost_Mode := Check; 838 839 elsif Policy = Name_Ignore then 840 Ghost_Mode := Ignore; 841 842 Set_Is_Ignored_Ghost_Node (N); 843 Propagate_Ignored_Ghost_Code (N); 844 end if; 845 end Set_Ghost_Mode_From_Policy; 846 847 -- Local variables 848 849 Nam : Node_Id; 850 851 -- Start of processing for Set_Ghost_Mode 852 853 begin 854 -- The input node denotes one of the many declaration kinds that may be 855 -- subject to pragma Ghost. 856 857 if Is_Declaration (N) then 858 if Is_Subject_To_Ghost (N) then 859 Set_Ghost_Mode_From_Policy; 860 861 -- The declaration denotes the completion of a deferred constant, 862 -- pragma Ghost appears on the partial declaration. 863 864 elsif Nkind (N) = N_Object_Declaration 865 and then Constant_Present (N) 866 and then Present (Prev_Id) 867 then 868 Set_Ghost_Mode_From_Entity (Prev_Id); 869 870 -- The declaration denotes the full view of a private type, pragma 871 -- Ghost appears on the partial declaration. 872 873 elsif Nkind (N) = N_Full_Type_Declaration 874 and then Is_Private_Type (Defining_Entity (N)) 875 and then Present (Prev_Id) 876 then 877 Set_Ghost_Mode_From_Entity (Prev_Id); 878 end if; 879 880 -- The input denotes an assignment or a procedure call. In this case 881 -- the Ghost mode is dictated by the name of the construct. 882 883 elsif Nkind_In (N, N_Assignment_Statement, 884 N_Procedure_Call_Statement) 885 then 886 -- When the reference extracts a subcomponent, recover the related 887 -- object (SPARK RM 6.9(1)). 888 889 Nam := Name (N); 890 while Nkind_In (Nam, N_Explicit_Dereference, 891 N_Indexed_Component, 892 N_Selected_Component, 893 N_Slice) 894 loop 895 Nam := Prefix (Nam); 896 end loop; 897 898 if Is_Entity_Name (Nam) 899 and then Present (Entity (Nam)) 900 then 901 Set_Ghost_Mode_From_Entity (Entity (Nam)); 902 end if; 903 904 -- The input denotes a package or subprogram body 905 906 elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then 907 if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id)) 908 or else Is_Subject_To_Ghost (N) 909 then 910 Set_Ghost_Mode_From_Policy; 911 end if; 912 end if; 913 end Set_Ghost_Mode; 914 915 ------------------------------- 916 -- Set_Ghost_Mode_For_Freeze -- 917 ------------------------------- 918 919 procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is 920 begin 921 if Is_Checked_Ghost_Entity (Id) then 922 Ghost_Mode := Check; 923 elsif Is_Ignored_Ghost_Entity (Id) then 924 Ghost_Mode := Ignore; 925 Propagate_Ignored_Ghost_Code (N); 926 end if; 927 end Set_Ghost_Mode_For_Freeze; 928 929 ------------------------- 930 -- Set_Is_Ghost_Entity -- 931 ------------------------- 932 933 procedure Set_Is_Ghost_Entity (Id : Entity_Id) is 934 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 935 begin 936 if Policy = Name_Check then 937 Set_Is_Checked_Ghost_Entity (Id); 938 elsif Policy = Name_Ignore then 939 Set_Is_Ignored_Ghost_Entity (Id); 940 end if; 941 end Set_Is_Ghost_Entity; 942 943end Ghost; 944