1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- C O N T R A C T S -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2015-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 Aspects; use Aspects; 27with Atree; use Atree; 28with Einfo; use Einfo; 29with Elists; use Elists; 30with Errout; use Errout; 31with Exp_Prag; use Exp_Prag; 32with Exp_Tss; use Exp_Tss; 33with Exp_Util; use Exp_Util; 34with Freeze; use Freeze; 35with Lib; use Lib; 36with Namet; use Namet; 37with Nlists; use Nlists; 38with Nmake; use Nmake; 39with Opt; use Opt; 40with Sem; use Sem; 41with Sem_Aux; use Sem_Aux; 42with Sem_Ch6; use Sem_Ch6; 43with Sem_Ch8; use Sem_Ch8; 44with Sem_Ch12; use Sem_Ch12; 45with Sem_Ch13; use Sem_Ch13; 46with Sem_Disp; use Sem_Disp; 47with Sem_Prag; use Sem_Prag; 48with Sem_Util; use Sem_Util; 49with Sinfo; use Sinfo; 50with Snames; use Snames; 51with Stand; use Stand; 52with Stringt; use Stringt; 53with Tbuild; use Tbuild; 54 55package body Contracts is 56 57 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id); 58 -- Analyze all delayed pragmas chained on the contract of package 59 -- instantiation Inst_Id as if they appear at the end of a declarative 60 -- region. The pragmas in question are: 61 -- 62 -- Part_Of 63 64 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); 65 -- Expand the contracts of a subprogram body and its correspoding spec (if 66 -- any). This routine processes all [refined] pre- and postconditions as 67 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the 68 -- entity of the subprogram body. 69 70 ----------------------- 71 -- Add_Contract_Item -- 72 ----------------------- 73 74 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is 75 Items : Node_Id := Contract (Id); 76 77 procedure Add_Classification; 78 -- Prepend Prag to the list of classifications 79 80 procedure Add_Contract_Test_Case; 81 -- Prepend Prag to the list of contract and test cases 82 83 procedure Add_Pre_Post_Condition; 84 -- Prepend Prag to the list of pre- and postconditions 85 86 ------------------------ 87 -- Add_Classification -- 88 ------------------------ 89 90 procedure Add_Classification is 91 begin 92 Set_Next_Pragma (Prag, Classifications (Items)); 93 Set_Classifications (Items, Prag); 94 end Add_Classification; 95 96 ---------------------------- 97 -- Add_Contract_Test_Case -- 98 ---------------------------- 99 100 procedure Add_Contract_Test_Case is 101 begin 102 Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); 103 Set_Contract_Test_Cases (Items, Prag); 104 end Add_Contract_Test_Case; 105 106 ---------------------------- 107 -- Add_Pre_Post_Condition -- 108 ---------------------------- 109 110 procedure Add_Pre_Post_Condition is 111 begin 112 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); 113 Set_Pre_Post_Conditions (Items, Prag); 114 end Add_Pre_Post_Condition; 115 116 -- Local variables 117 118 -- A contract must contain only pragmas 119 120 pragma Assert (Nkind (Prag) = N_Pragma); 121 Prag_Nam : constant Name_Id := Pragma_Name (Prag); 122 123 -- Start of processing for Add_Contract_Item 124 125 begin 126 -- Create a new contract when adding the first item 127 128 if No (Items) then 129 Items := Make_Contract (Sloc (Id)); 130 Set_Contract (Id, Items); 131 end if; 132 133 -- Constants, the applicable pragmas are: 134 -- Part_Of 135 136 if Ekind (Id) = E_Constant then 137 if Prag_Nam = Name_Part_Of then 138 Add_Classification; 139 140 -- The pragma is not a proper contract item 141 142 else 143 raise Program_Error; 144 end if; 145 146 -- Entry bodies, the applicable pragmas are: 147 -- Refined_Depends 148 -- Refined_Global 149 -- Refined_Post 150 151 elsif Is_Entry_Body (Id) then 152 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then 153 Add_Classification; 154 155 elsif Prag_Nam = Name_Refined_Post then 156 Add_Pre_Post_Condition; 157 158 -- The pragma is not a proper contract item 159 160 else 161 raise Program_Error; 162 end if; 163 164 -- Entry or subprogram declarations, the applicable pragmas are: 165 -- Attach_Handler 166 -- Contract_Cases 167 -- Depends 168 -- Extensions_Visible 169 -- Global 170 -- Interrupt_Handler 171 -- Postcondition 172 -- Precondition 173 -- Test_Case 174 -- Volatile_Function 175 176 elsif Is_Entry_Declaration (Id) 177 or else Ekind_In (Id, E_Function, 178 E_Generic_Function, 179 E_Generic_Procedure, 180 E_Procedure) 181 then 182 if Nam_In (Prag_Nam, Name_Attach_Handler, Name_Interrupt_Handler) 183 and then Ekind_In (Id, E_Generic_Procedure, E_Procedure) 184 then 185 Add_Classification; 186 187 elsif Nam_In (Prag_Nam, Name_Depends, 188 Name_Extensions_Visible, 189 Name_Global) 190 then 191 Add_Classification; 192 193 elsif Prag_Nam = Name_Volatile_Function 194 and then Ekind_In (Id, E_Function, E_Generic_Function) 195 then 196 Add_Classification; 197 198 elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then 199 Add_Contract_Test_Case; 200 201 elsif Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then 202 Add_Pre_Post_Condition; 203 204 -- The pragma is not a proper contract item 205 206 else 207 raise Program_Error; 208 end if; 209 210 -- Packages or instantiations, the applicable pragmas are: 211 -- Abstract_States 212 -- Initial_Condition 213 -- Initializes 214 -- Part_Of (instantiation only) 215 216 elsif Ekind_In (Id, E_Generic_Package, E_Package) then 217 if Nam_In (Prag_Nam, Name_Abstract_State, 218 Name_Initial_Condition, 219 Name_Initializes) 220 then 221 Add_Classification; 222 223 -- Indicator Part_Of must be associated with a package instantiation 224 225 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then 226 Add_Classification; 227 228 -- The pragma is not a proper contract item 229 230 else 231 raise Program_Error; 232 end if; 233 234 -- Package bodies, the applicable pragmas are: 235 -- Refined_States 236 237 elsif Ekind (Id) = E_Package_Body then 238 if Prag_Nam = Name_Refined_State then 239 Add_Classification; 240 241 -- The pragma is not a proper contract item 242 243 else 244 raise Program_Error; 245 end if; 246 247 -- Protected units, the applicable pragmas are: 248 -- Part_Of 249 250 elsif Ekind (Id) = E_Protected_Type then 251 if Prag_Nam = Name_Part_Of then 252 Add_Classification; 253 254 -- The pragma is not a proper contract item 255 256 else 257 raise Program_Error; 258 end if; 259 260 -- Subprogram bodies, the applicable pragmas are: 261 -- Postcondition 262 -- Precondition 263 -- Refined_Depends 264 -- Refined_Global 265 -- Refined_Post 266 267 elsif Ekind (Id) = E_Subprogram_Body then 268 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then 269 Add_Classification; 270 271 elsif Nam_In (Prag_Nam, Name_Postcondition, 272 Name_Precondition, 273 Name_Refined_Post) 274 then 275 Add_Pre_Post_Condition; 276 277 -- The pragma is not a proper contract item 278 279 else 280 raise Program_Error; 281 end if; 282 283 -- Task bodies, the applicable pragmas are: 284 -- Refined_Depends 285 -- Refined_Global 286 287 elsif Ekind (Id) = E_Task_Body then 288 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then 289 Add_Classification; 290 291 -- The pragma is not a proper contract item 292 293 else 294 raise Program_Error; 295 end if; 296 297 -- Task units, the applicable pragmas are: 298 -- Depends 299 -- Global 300 -- Part_Of 301 302 elsif Ekind (Id) = E_Task_Type then 303 if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then 304 Add_Classification; 305 306 -- The pragma is not a proper contract item 307 308 else 309 raise Program_Error; 310 end if; 311 312 -- Variables, the applicable pragmas are: 313 -- Async_Readers 314 -- Async_Writers 315 -- Constant_After_Elaboration 316 -- Depends 317 -- Effective_Reads 318 -- Effective_Writes 319 -- Global 320 -- No_Caching 321 -- Part_Of 322 323 elsif Ekind (Id) = E_Variable then 324 if Nam_In (Prag_Nam, Name_Async_Readers, 325 Name_Async_Writers, 326 Name_Constant_After_Elaboration, 327 Name_Depends, 328 Name_Effective_Reads, 329 Name_Effective_Writes, 330 Name_Global, 331 Name_No_Caching, 332 Name_Part_Of) 333 then 334 Add_Classification; 335 336 -- The pragma is not a proper contract item 337 338 else 339 raise Program_Error; 340 end if; 341 end if; 342 end Add_Contract_Item; 343 344 ----------------------- 345 -- Analyze_Contracts -- 346 ----------------------- 347 348 procedure Analyze_Contracts (L : List_Id) is 349 Decl : Node_Id; 350 351 begin 352 Decl := First (L); 353 while Present (Decl) loop 354 355 -- Entry or subprogram declarations 356 357 if Nkind_In (Decl, N_Abstract_Subprogram_Declaration, 358 N_Entry_Declaration, 359 N_Generic_Subprogram_Declaration, 360 N_Subprogram_Declaration) 361 then 362 declare 363 Subp_Id : constant Entity_Id := Defining_Entity (Decl); 364 365 begin 366 Analyze_Entry_Or_Subprogram_Contract (Subp_Id); 367 368 -- If analysis of a class-wide pre/postcondition indicates 369 -- that a class-wide clone is needed, analyze its declaration 370 -- now. Its body is created when the body of the original 371 -- operation is analyzed (and rewritten). 372 373 if Is_Subprogram (Subp_Id) 374 and then Present (Class_Wide_Clone (Subp_Id)) 375 then 376 Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id))); 377 end if; 378 end; 379 380 -- Entry or subprogram bodies 381 382 elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then 383 Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl)); 384 385 -- Objects 386 387 elsif Nkind (Decl) = N_Object_Declaration then 388 Analyze_Object_Contract (Defining_Entity (Decl)); 389 390 -- Package instantiation 391 392 elsif Nkind (Decl) = N_Package_Instantiation then 393 Analyze_Package_Instantiation_Contract (Defining_Entity (Decl)); 394 395 -- Protected units 396 397 elsif Nkind_In (Decl, N_Protected_Type_Declaration, 398 N_Single_Protected_Declaration) 399 then 400 Analyze_Protected_Contract (Defining_Entity (Decl)); 401 402 -- Subprogram body stubs 403 404 elsif Nkind (Decl) = N_Subprogram_Body_Stub then 405 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); 406 407 -- Task units 408 409 elsif Nkind_In (Decl, N_Single_Task_Declaration, 410 N_Task_Type_Declaration) 411 then 412 Analyze_Task_Contract (Defining_Entity (Decl)); 413 414 -- For type declarations, we need to do the preanalysis of Iterable 415 -- aspect specifications. 416 417 -- Other type aspects need to be resolved here??? 418 419 elsif Nkind (Decl) = N_Private_Type_Declaration 420 and then Present (Aspect_Specifications (Decl)) 421 then 422 declare 423 E : constant Entity_Id := Defining_Identifier (Decl); 424 It : constant Node_Id := Find_Aspect (E, Aspect_Iterable); 425 426 begin 427 if Present (It) then 428 Validate_Iterable_Aspect (E, It); 429 end if; 430 end; 431 end if; 432 433 Next (Decl); 434 end loop; 435 end Analyze_Contracts; 436 437 ----------------------------------------------- 438 -- Analyze_Entry_Or_Subprogram_Body_Contract -- 439 ----------------------------------------------- 440 441 -- WARNING: This routine manages SPARK regions. Return statements must be 442 -- replaced by gotos which jump to the end of the routine and restore the 443 -- SPARK mode. 444 445 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is 446 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 447 Items : constant Node_Id := Contract (Body_Id); 448 Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); 449 450 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 451 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 452 -- Save the SPARK_Mode-related data to restore on exit 453 454 begin 455 -- When a subprogram body declaration is illegal, its defining entity is 456 -- left unanalyzed. There is nothing left to do in this case because the 457 -- body lacks a contract, or even a proper Ekind. 458 459 if Ekind (Body_Id) = E_Void then 460 return; 461 462 -- Do not analyze a contract multiple times 463 464 elsif Present (Items) then 465 if Analyzed (Items) then 466 return; 467 else 468 Set_Analyzed (Items); 469 end if; 470 end if; 471 472 -- Due to the timing of contract analysis, delayed pragmas may be 473 -- subject to the wrong SPARK_Mode, usually that of the enclosing 474 -- context. To remedy this, restore the original SPARK_Mode of the 475 -- related subprogram body. 476 477 Set_SPARK_Mode (Body_Id); 478 479 -- Ensure that the contract cases or postconditions mention 'Result or 480 -- define a post-state. 481 482 Check_Result_And_Post_State (Body_Id); 483 484 -- A stand-alone nonvolatile function body cannot have an effectively 485 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This 486 -- check is relevant only when SPARK_Mode is on, as it is not a standard 487 -- legality rule. The check is performed here because Volatile_Function 488 -- is processed after the analysis of the related subprogram body. The 489 -- check only applies to source subprograms and not to generated TSS 490 -- subprograms. 491 492 if SPARK_Mode = On 493 and then Ekind_In (Body_Id, E_Function, E_Generic_Function) 494 and then Comes_From_Source (Spec_Id) 495 and then not Is_Volatile_Function (Body_Id) 496 then 497 Check_Nonvolatile_Function_Profile (Body_Id); 498 end if; 499 500 -- Restore the SPARK_Mode of the enclosing context after all delayed 501 -- pragmas have been analyzed. 502 503 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 504 505 -- Capture all global references in a generic subprogram body now that 506 -- the contract has been analyzed. 507 508 if Is_Generic_Declaration_Or_Body (Body_Decl) then 509 Save_Global_References_In_Contract 510 (Templ => Original_Node (Body_Decl), 511 Gen_Id => Spec_Id); 512 end if; 513 514 -- Deal with preconditions, [refined] postconditions, Contract_Cases, 515 -- invariants and predicates associated with body and its spec. Do not 516 -- expand the contract of subprogram body stubs. 517 518 if Nkind (Body_Decl) = N_Subprogram_Body then 519 Expand_Subprogram_Contract (Body_Id); 520 end if; 521 end Analyze_Entry_Or_Subprogram_Body_Contract; 522 523 ------------------------------------------ 524 -- Analyze_Entry_Or_Subprogram_Contract -- 525 ------------------------------------------ 526 527 -- WARNING: This routine manages SPARK regions. Return statements must be 528 -- replaced by gotos which jump to the end of the routine and restore the 529 -- SPARK mode. 530 531 procedure Analyze_Entry_Or_Subprogram_Contract 532 (Subp_Id : Entity_Id; 533 Freeze_Id : Entity_Id := Empty) 534 is 535 Items : constant Node_Id := Contract (Subp_Id); 536 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 537 538 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 539 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 540 -- Save the SPARK_Mode-related data to restore on exit 541 542 Skip_Assert_Exprs : constant Boolean := 543 Ekind_In (Subp_Id, E_Entry, E_Entry_Family) 544 and then not ASIS_Mode 545 and then not GNATprove_Mode; 546 547 Depends : Node_Id := Empty; 548 Global : Node_Id := Empty; 549 Prag : Node_Id; 550 Prag_Nam : Name_Id; 551 552 begin 553 -- Do not analyze a contract multiple times 554 555 if Present (Items) then 556 if Analyzed (Items) then 557 return; 558 else 559 Set_Analyzed (Items); 560 end if; 561 end if; 562 563 -- Due to the timing of contract analysis, delayed pragmas may be 564 -- subject to the wrong SPARK_Mode, usually that of the enclosing 565 -- context. To remedy this, restore the original SPARK_Mode of the 566 -- related subprogram body. 567 568 Set_SPARK_Mode (Subp_Id); 569 570 -- All subprograms carry a contract, but for some it is not significant 571 -- and should not be processed. 572 573 if not Has_Significant_Contract (Subp_Id) then 574 null; 575 576 elsif Present (Items) then 577 578 -- Do not analyze the pre/postconditions of an entry declaration 579 -- unless annotating the original tree for ASIS or GNATprove. The 580 -- real analysis occurs when the pre/postconditons are relocated to 581 -- the contract wrapper procedure (see Build_Contract_Wrapper). 582 583 if Skip_Assert_Exprs then 584 null; 585 586 -- Otherwise analyze the pre/postconditions. 587 -- If these come from an aspect specification, their expressions 588 -- might include references to types that are not frozen yet, in the 589 -- case where the body is a rewritten expression function that is a 590 -- completion, so freeze all types within before constructing the 591 -- contract code. 592 593 else 594 declare 595 Bod : Node_Id; 596 Freeze_Types : Boolean := False; 597 598 begin 599 if Present (Freeze_Id) then 600 Bod := Unit_Declaration_Node (Freeze_Id); 601 602 if Nkind (Bod) = N_Subprogram_Body 603 and then Was_Expression_Function (Bod) 604 and then Ekind (Subp_Id) = E_Function 605 and then Chars (Subp_Id) = Chars (Freeze_Id) 606 and then Subp_Id /= Freeze_Id 607 then 608 Freeze_Types := True; 609 end if; 610 end if; 611 612 Prag := Pre_Post_Conditions (Items); 613 while Present (Prag) loop 614 if Freeze_Types 615 and then Present (Corresponding_Aspect (Prag)) 616 then 617 Freeze_Expr_Types 618 (Def_Id => Subp_Id, 619 Typ => Standard_Boolean, 620 Expr => Expression (Corresponding_Aspect (Prag)), 621 N => Bod); 622 end if; 623 624 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id); 625 Prag := Next_Pragma (Prag); 626 end loop; 627 end; 628 end if; 629 630 -- Analyze contract-cases and test-cases 631 632 Prag := Contract_Test_Cases (Items); 633 while Present (Prag) loop 634 Prag_Nam := Pragma_Name (Prag); 635 636 if Prag_Nam = Name_Contract_Cases then 637 638 -- Do not analyze the contract cases of an entry declaration 639 -- unless annotating the original tree for ASIS or GNATprove. 640 -- The real analysis occurs when the contract cases are moved 641 -- to the contract wrapper procedure (Build_Contract_Wrapper). 642 643 if Skip_Assert_Exprs then 644 null; 645 646 -- Otherwise analyze the contract cases 647 648 else 649 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id); 650 end if; 651 else 652 pragma Assert (Prag_Nam = Name_Test_Case); 653 Analyze_Test_Case_In_Decl_Part (Prag); 654 end if; 655 656 Prag := Next_Pragma (Prag); 657 end loop; 658 659 -- Analyze classification pragmas 660 661 Prag := Classifications (Items); 662 while Present (Prag) loop 663 Prag_Nam := Pragma_Name (Prag); 664 665 if Prag_Nam = Name_Depends then 666 Depends := Prag; 667 668 elsif Prag_Nam = Name_Global then 669 Global := Prag; 670 end if; 671 672 Prag := Next_Pragma (Prag); 673 end loop; 674 675 -- Analyze Global first, as Depends may mention items classified in 676 -- the global categorization. 677 678 if Present (Global) then 679 Analyze_Global_In_Decl_Part (Global); 680 end if; 681 682 -- Depends must be analyzed after Global in order to see the modes of 683 -- all global items. 684 685 if Present (Depends) then 686 Analyze_Depends_In_Decl_Part (Depends); 687 end if; 688 689 -- Ensure that the contract cases or postconditions mention 'Result 690 -- or define a post-state. 691 692 Check_Result_And_Post_State (Subp_Id); 693 end if; 694 695 -- A nonvolatile function cannot have an effectively volatile formal 696 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant 697 -- only when SPARK_Mode is on, as it is not a standard legality rule. 698 -- The check is performed here because pragma Volatile_Function is 699 -- processed after the analysis of the related subprogram declaration. 700 701 if SPARK_Mode = On 702 and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) 703 and then Comes_From_Source (Subp_Id) 704 and then not Is_Volatile_Function (Subp_Id) 705 then 706 Check_Nonvolatile_Function_Profile (Subp_Id); 707 end if; 708 709 -- Restore the SPARK_Mode of the enclosing context after all delayed 710 -- pragmas have been analyzed. 711 712 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 713 714 -- Capture all global references in a generic subprogram now that the 715 -- contract has been analyzed. 716 717 if Is_Generic_Declaration_Or_Body (Subp_Decl) then 718 Save_Global_References_In_Contract 719 (Templ => Original_Node (Subp_Decl), 720 Gen_Id => Subp_Id); 721 end if; 722 end Analyze_Entry_Or_Subprogram_Contract; 723 724 ----------------------------- 725 -- Analyze_Object_Contract -- 726 ----------------------------- 727 728 -- WARNING: This routine manages SPARK regions. Return statements must be 729 -- replaced by gotos which jump to the end of the routine and restore the 730 -- SPARK mode. 731 732 procedure Analyze_Object_Contract 733 (Obj_Id : Entity_Id; 734 Freeze_Id : Entity_Id := Empty) 735 is 736 Obj_Typ : constant Entity_Id := Etype (Obj_Id); 737 738 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 739 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 740 -- Save the SPARK_Mode-related data to restore on exit 741 742 AR_Val : Boolean := False; 743 AW_Val : Boolean := False; 744 ER_Val : Boolean := False; 745 EW_Val : Boolean := False; 746 NC_Val : Boolean := False; 747 Items : Node_Id; 748 Prag : Node_Id; 749 Ref_Elmt : Elmt_Id; 750 Seen : Boolean := False; 751 752 begin 753 -- The loop parameter in an element iterator over a formal container 754 -- is declared with an object declaration, but no contracts apply. 755 756 if Ekind (Obj_Id) = E_Loop_Parameter then 757 return; 758 end if; 759 760 -- Do not analyze a contract multiple times 761 762 Items := Contract (Obj_Id); 763 764 if Present (Items) then 765 if Analyzed (Items) then 766 return; 767 else 768 Set_Analyzed (Items); 769 end if; 770 end if; 771 772 -- The anonymous object created for a single concurrent type inherits 773 -- the SPARK_Mode from the type. Due to the timing of contract analysis, 774 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that 775 -- of the enclosing context. To remedy this, restore the original mode 776 -- of the related anonymous object. 777 778 if Is_Single_Concurrent_Object (Obj_Id) 779 and then Present (SPARK_Pragma (Obj_Id)) 780 then 781 Set_SPARK_Mode (Obj_Id); 782 end if; 783 784 -- Constant-related checks 785 786 if Ekind (Obj_Id) = E_Constant then 787 788 -- Analyze indicator Part_Of 789 790 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); 791 792 -- Check whether the lack of indicator Part_Of agrees with the 793 -- placement of the constant with respect to the state space. 794 795 if No (Prag) then 796 Check_Missing_Part_Of (Obj_Id); 797 end if; 798 799 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). 800 -- This check is relevant only when SPARK_Mode is on, as it is not 801 -- a standard Ada legality rule. Internally-generated constants that 802 -- map generic formals to actuals in instantiations are allowed to 803 -- be volatile. 804 805 if SPARK_Mode = On 806 and then Comes_From_Source (Obj_Id) 807 and then Is_Effectively_Volatile (Obj_Id) 808 and then No (Corresponding_Generic_Association (Parent (Obj_Id))) 809 then 810 Error_Msg_N ("constant cannot be volatile", Obj_Id); 811 end if; 812 813 -- Variable-related checks 814 815 else pragma Assert (Ekind (Obj_Id) = E_Variable); 816 817 -- Analyze all external properties 818 819 Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); 820 821 if Present (Prag) then 822 Analyze_External_Property_In_Decl_Part (Prag, AR_Val); 823 Seen := True; 824 end if; 825 826 Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); 827 828 if Present (Prag) then 829 Analyze_External_Property_In_Decl_Part (Prag, AW_Val); 830 Seen := True; 831 end if; 832 833 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); 834 835 if Present (Prag) then 836 Analyze_External_Property_In_Decl_Part (Prag, ER_Val); 837 Seen := True; 838 end if; 839 840 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); 841 842 if Present (Prag) then 843 Analyze_External_Property_In_Decl_Part (Prag, EW_Val); 844 Seen := True; 845 end if; 846 847 -- Verify the mutual interaction of the various external properties 848 849 if Seen then 850 Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); 851 end if; 852 853 -- Analyze the non-external volatility property No_Caching 854 855 Prag := Get_Pragma (Obj_Id, Pragma_No_Caching); 856 857 if Present (Prag) then 858 Analyze_External_Property_In_Decl_Part (Prag, NC_Val); 859 end if; 860 861 -- The anonymous object created for a single concurrent type carries 862 -- pragmas Depends and Globat of the type. 863 864 if Is_Single_Concurrent_Object (Obj_Id) then 865 866 -- Analyze Global first, as Depends may mention items classified 867 -- in the global categorization. 868 869 Prag := Get_Pragma (Obj_Id, Pragma_Global); 870 871 if Present (Prag) then 872 Analyze_Global_In_Decl_Part (Prag); 873 end if; 874 875 -- Depends must be analyzed after Global in order to see the modes 876 -- of all global items. 877 878 Prag := Get_Pragma (Obj_Id, Pragma_Depends); 879 880 if Present (Prag) then 881 Analyze_Depends_In_Decl_Part (Prag); 882 end if; 883 end if; 884 885 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); 886 887 -- Analyze indicator Part_Of 888 889 if Present (Prag) then 890 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id); 891 892 -- The variable is a constituent of a single protected/task type 893 -- and behaves as a component of the type. Verify that references 894 -- to the variable occur within the definition or body of the type 895 -- (SPARK RM 9.3). 896 897 if Present (Encapsulating_State (Obj_Id)) 898 and then Is_Single_Concurrent_Object 899 (Encapsulating_State (Obj_Id)) 900 and then Present (Part_Of_References (Obj_Id)) 901 then 902 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id)); 903 while Present (Ref_Elmt) loop 904 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt)); 905 Next_Elmt (Ref_Elmt); 906 end loop; 907 end if; 908 909 -- Otherwise check whether the lack of indicator Part_Of agrees with 910 -- the placement of the variable with respect to the state space. 911 912 else 913 Check_Missing_Part_Of (Obj_Id); 914 end if; 915 916 -- The following checks are relevant only when SPARK_Mode is on, as 917 -- they are not standard Ada legality rules. Internally generated 918 -- temporaries are ignored. 919 920 if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then 921 if Is_Effectively_Volatile (Obj_Id) then 922 923 -- The declaration of an effectively volatile object must 924 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). 925 926 if not Is_Library_Level_Entity (Obj_Id) then 927 Error_Msg_N 928 ("volatile variable & must be declared at library level " 929 & "(SPARK RM 7.1.3(3))", Obj_Id); 930 931 -- An object of a discriminated type cannot be effectively 932 -- volatile except for protected objects (SPARK RM 7.1.3(5)). 933 934 elsif Has_Discriminants (Obj_Typ) 935 and then not Is_Protected_Type (Obj_Typ) 936 then 937 Error_Msg_N 938 ("discriminated object & cannot be volatile", Obj_Id); 939 end if; 940 941 -- The object is not effectively volatile 942 943 else 944 -- A non-effectively volatile object cannot have effectively 945 -- volatile components (SPARK RM 7.1.3(6)). 946 947 if not Is_Effectively_Volatile (Obj_Id) 948 and then Has_Volatile_Component (Obj_Typ) 949 then 950 Error_Msg_N 951 ("non-volatile object & cannot have volatile components", 952 Obj_Id); 953 end if; 954 end if; 955 end if; 956 end if; 957 958 -- Common checks 959 960 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then 961 962 -- A Ghost object cannot be of a type that yields a synchronized 963 -- object (SPARK RM 6.9(19)). 964 965 if Yields_Synchronized_Object (Obj_Typ) then 966 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); 967 968 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and 969 -- SPARK RM 6.9(19)). 970 971 elsif Is_Effectively_Volatile (Obj_Id) then 972 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); 973 974 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). 975 -- One exception to this is the object that represents the dispatch 976 -- table of a Ghost tagged type, as the symbol needs to be exported. 977 978 elsif Is_Exported (Obj_Id) then 979 Error_Msg_N ("ghost object & cannot be exported", Obj_Id); 980 981 elsif Is_Imported (Obj_Id) then 982 Error_Msg_N ("ghost object & cannot be imported", Obj_Id); 983 end if; 984 end if; 985 986 -- Restore the SPARK_Mode of the enclosing context after all delayed 987 -- pragmas have been analyzed. 988 989 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 990 end Analyze_Object_Contract; 991 992 ----------------------------------- 993 -- Analyze_Package_Body_Contract -- 994 ----------------------------------- 995 996 -- WARNING: This routine manages SPARK regions. Return statements must be 997 -- replaced by gotos which jump to the end of the routine and restore the 998 -- SPARK mode. 999 1000 procedure Analyze_Package_Body_Contract 1001 (Body_Id : Entity_Id; 1002 Freeze_Id : Entity_Id := Empty) 1003 is 1004 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 1005 Items : constant Node_Id := Contract (Body_Id); 1006 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); 1007 1008 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1009 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1010 -- Save the SPARK_Mode-related data to restore on exit 1011 1012 Ref_State : Node_Id; 1013 1014 begin 1015 -- Do not analyze a contract multiple times 1016 1017 if Present (Items) then 1018 if Analyzed (Items) then 1019 return; 1020 else 1021 Set_Analyzed (Items); 1022 end if; 1023 end if; 1024 1025 -- Due to the timing of contract analysis, delayed pragmas may be 1026 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1027 -- context. To remedy this, restore the original SPARK_Mode of the 1028 -- related package body. 1029 1030 Set_SPARK_Mode (Body_Id); 1031 1032 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); 1033 1034 -- The analysis of pragma Refined_State detects whether the spec has 1035 -- abstract states available for refinement. 1036 1037 if Present (Ref_State) then 1038 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); 1039 end if; 1040 1041 -- Restore the SPARK_Mode of the enclosing context after all delayed 1042 -- pragmas have been analyzed. 1043 1044 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1045 1046 -- Capture all global references in a generic package body now that the 1047 -- contract has been analyzed. 1048 1049 if Is_Generic_Declaration_Or_Body (Body_Decl) then 1050 Save_Global_References_In_Contract 1051 (Templ => Original_Node (Body_Decl), 1052 Gen_Id => Spec_Id); 1053 end if; 1054 end Analyze_Package_Body_Contract; 1055 1056 ------------------------------ 1057 -- Analyze_Package_Contract -- 1058 ------------------------------ 1059 1060 -- WARNING: This routine manages SPARK regions. Return statements must be 1061 -- replaced by gotos which jump to the end of the routine and restore the 1062 -- SPARK mode. 1063 1064 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is 1065 Items : constant Node_Id := Contract (Pack_Id); 1066 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); 1067 1068 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1069 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1070 -- Save the SPARK_Mode-related data to restore on exit 1071 1072 Init : Node_Id := Empty; 1073 Init_Cond : Node_Id := Empty; 1074 Prag : Node_Id; 1075 Prag_Nam : Name_Id; 1076 1077 begin 1078 -- Do not analyze a contract multiple times 1079 1080 if Present (Items) then 1081 if Analyzed (Items) then 1082 return; 1083 else 1084 Set_Analyzed (Items); 1085 end if; 1086 end if; 1087 1088 -- Due to the timing of contract analysis, delayed pragmas may be 1089 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1090 -- context. To remedy this, restore the original SPARK_Mode of the 1091 -- related package. 1092 1093 Set_SPARK_Mode (Pack_Id); 1094 1095 if Present (Items) then 1096 1097 -- Locate and store pragmas Initial_Condition and Initializes, since 1098 -- their order of analysis matters. 1099 1100 Prag := Classifications (Items); 1101 while Present (Prag) loop 1102 Prag_Nam := Pragma_Name (Prag); 1103 1104 if Prag_Nam = Name_Initial_Condition then 1105 Init_Cond := Prag; 1106 1107 elsif Prag_Nam = Name_Initializes then 1108 Init := Prag; 1109 end if; 1110 1111 Prag := Next_Pragma (Prag); 1112 end loop; 1113 1114 -- Analyze the initialization-related pragmas. Initializes must come 1115 -- before Initial_Condition due to item dependencies. 1116 1117 if Present (Init) then 1118 Analyze_Initializes_In_Decl_Part (Init); 1119 end if; 1120 1121 if Present (Init_Cond) then 1122 Analyze_Initial_Condition_In_Decl_Part (Init_Cond); 1123 end if; 1124 end if; 1125 1126 -- Restore the SPARK_Mode of the enclosing context after all delayed 1127 -- pragmas have been analyzed. 1128 1129 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1130 1131 -- Capture all global references in a generic package now that the 1132 -- contract has been analyzed. 1133 1134 if Is_Generic_Declaration_Or_Body (Pack_Decl) then 1135 Save_Global_References_In_Contract 1136 (Templ => Original_Node (Pack_Decl), 1137 Gen_Id => Pack_Id); 1138 end if; 1139 end Analyze_Package_Contract; 1140 1141 -------------------------------------------- 1142 -- Analyze_Package_Instantiation_Contract -- 1143 -------------------------------------------- 1144 1145 -- WARNING: This routine manages SPARK regions. Return statements must be 1146 -- replaced by gotos which jump to the end of the routine and restore the 1147 -- SPARK mode. 1148 1149 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is 1150 Inst_Spec : constant Node_Id := 1151 Instance_Spec (Unit_Declaration_Node (Inst_Id)); 1152 1153 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1154 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1155 -- Save the SPARK_Mode-related data to restore on exit 1156 1157 Pack_Id : Entity_Id; 1158 Prag : Node_Id; 1159 1160 begin 1161 -- Nothing to do when the package instantiation is erroneous or left 1162 -- partially decorated. 1163 1164 if No (Inst_Spec) then 1165 return; 1166 end if; 1167 1168 Pack_Id := Defining_Entity (Inst_Spec); 1169 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); 1170 1171 -- Due to the timing of contract analysis, delayed pragmas may be 1172 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1173 -- context. To remedy this, restore the original SPARK_Mode of the 1174 -- related package. 1175 1176 Set_SPARK_Mode (Pack_Id); 1177 1178 -- Check whether the lack of indicator Part_Of agrees with the placement 1179 -- of the package instantiation with respect to the state space. Nested 1180 -- package instantiations do not need to be checked because they inherit 1181 -- Part_Of indicator of the outermost package instantiation (see routine 1182 -- Propagate_Part_Of in Sem_Prag). 1183 1184 if In_Instance then 1185 null; 1186 1187 elsif No (Prag) then 1188 Check_Missing_Part_Of (Pack_Id); 1189 end if; 1190 1191 -- Restore the SPARK_Mode of the enclosing context after all delayed 1192 -- pragmas have been analyzed. 1193 1194 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1195 end Analyze_Package_Instantiation_Contract; 1196 1197 -------------------------------- 1198 -- Analyze_Protected_Contract -- 1199 -------------------------------- 1200 1201 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is 1202 Items : constant Node_Id := Contract (Prot_Id); 1203 1204 begin 1205 -- Do not analyze a contract multiple times 1206 1207 if Present (Items) then 1208 if Analyzed (Items) then 1209 return; 1210 else 1211 Set_Analyzed (Items); 1212 end if; 1213 end if; 1214 end Analyze_Protected_Contract; 1215 1216 ------------------------------------------- 1217 -- Analyze_Subprogram_Body_Stub_Contract -- 1218 ------------------------------------------- 1219 1220 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is 1221 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); 1222 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); 1223 1224 begin 1225 -- A subprogram body stub may act as its own spec or as the completion 1226 -- of a previous declaration. Depending on the context, the contract of 1227 -- the stub may contain two sets of pragmas. 1228 1229 -- The stub is a completion, the applicable pragmas are: 1230 -- Refined_Depends 1231 -- Refined_Global 1232 1233 if Present (Spec_Id) then 1234 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); 1235 1236 -- The stub acts as its own spec, the applicable pragmas are: 1237 -- Contract_Cases 1238 -- Depends 1239 -- Global 1240 -- Postcondition 1241 -- Precondition 1242 -- Test_Case 1243 1244 else 1245 Analyze_Entry_Or_Subprogram_Contract (Stub_Id); 1246 end if; 1247 end Analyze_Subprogram_Body_Stub_Contract; 1248 1249 --------------------------- 1250 -- Analyze_Task_Contract -- 1251 --------------------------- 1252 1253 -- WARNING: This routine manages SPARK regions. Return statements must be 1254 -- replaced by gotos which jump to the end of the routine and restore the 1255 -- SPARK mode. 1256 1257 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is 1258 Items : constant Node_Id := Contract (Task_Id); 1259 1260 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1261 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1262 -- Save the SPARK_Mode-related data to restore on exit 1263 1264 Prag : Node_Id; 1265 1266 begin 1267 -- Do not analyze a contract multiple times 1268 1269 if Present (Items) then 1270 if Analyzed (Items) then 1271 return; 1272 else 1273 Set_Analyzed (Items); 1274 end if; 1275 end if; 1276 1277 -- Due to the timing of contract analysis, delayed pragmas may be 1278 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1279 -- context. To remedy this, restore the original SPARK_Mode of the 1280 -- related task unit. 1281 1282 Set_SPARK_Mode (Task_Id); 1283 1284 -- Analyze Global first, as Depends may mention items classified in the 1285 -- global categorization. 1286 1287 Prag := Get_Pragma (Task_Id, Pragma_Global); 1288 1289 if Present (Prag) then 1290 Analyze_Global_In_Decl_Part (Prag); 1291 end if; 1292 1293 -- Depends must be analyzed after Global in order to see the modes of 1294 -- all global items. 1295 1296 Prag := Get_Pragma (Task_Id, Pragma_Depends); 1297 1298 if Present (Prag) then 1299 Analyze_Depends_In_Decl_Part (Prag); 1300 end if; 1301 1302 -- Restore the SPARK_Mode of the enclosing context after all delayed 1303 -- pragmas have been analyzed. 1304 1305 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1306 end Analyze_Task_Contract; 1307 1308 ----------------------------- 1309 -- Create_Generic_Contract -- 1310 ----------------------------- 1311 1312 procedure Create_Generic_Contract (Unit : Node_Id) is 1313 Templ : constant Node_Id := Original_Node (Unit); 1314 Templ_Id : constant Entity_Id := Defining_Entity (Templ); 1315 1316 procedure Add_Generic_Contract_Pragma (Prag : Node_Id); 1317 -- Add a single contract-related source pragma Prag to the contract of 1318 -- generic template Templ_Id. 1319 1320 --------------------------------- 1321 -- Add_Generic_Contract_Pragma -- 1322 --------------------------------- 1323 1324 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is 1325 Prag_Templ : Node_Id; 1326 1327 begin 1328 -- Mark the pragma to prevent the premature capture of global 1329 -- references when capturing global references of the context 1330 -- (see Save_References_In_Pragma). 1331 1332 Set_Is_Generic_Contract_Pragma (Prag); 1333 1334 -- Pragmas that apply to a generic subprogram declaration are not 1335 -- part of the semantic structure of the generic template: 1336 1337 -- generic 1338 -- procedure Example (Formal : Integer); 1339 -- pragma Precondition (Formal > 0); 1340 1341 -- Create a generic template for such pragmas and link the template 1342 -- of the pragma with the generic template. 1343 1344 if Nkind (Templ) = N_Generic_Subprogram_Declaration then 1345 Rewrite 1346 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); 1347 Prag_Templ := Original_Node (Prag); 1348 1349 Set_Is_Generic_Contract_Pragma (Prag_Templ); 1350 Add_Contract_Item (Prag_Templ, Templ_Id); 1351 1352 -- Otherwise link the pragma with the generic template 1353 1354 else 1355 Add_Contract_Item (Prag, Templ_Id); 1356 end if; 1357 end Add_Generic_Contract_Pragma; 1358 1359 -- Local variables 1360 1361 Context : constant Node_Id := Parent (Unit); 1362 Decl : Node_Id := Empty; 1363 1364 -- Start of processing for Create_Generic_Contract 1365 1366 begin 1367 -- A generic package declaration carries contract-related source pragmas 1368 -- in its visible declarations. 1369 1370 if Nkind (Templ) = N_Generic_Package_Declaration then 1371 Set_Ekind (Templ_Id, E_Generic_Package); 1372 1373 if Present (Visible_Declarations (Specification (Templ))) then 1374 Decl := First (Visible_Declarations (Specification (Templ))); 1375 end if; 1376 1377 -- A generic package body carries contract-related source pragmas in its 1378 -- declarations. 1379 1380 elsif Nkind (Templ) = N_Package_Body then 1381 Set_Ekind (Templ_Id, E_Package_Body); 1382 1383 if Present (Declarations (Templ)) then 1384 Decl := First (Declarations (Templ)); 1385 end if; 1386 1387 -- Generic subprogram declaration 1388 1389 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then 1390 if Nkind (Specification (Templ)) = N_Function_Specification then 1391 Set_Ekind (Templ_Id, E_Generic_Function); 1392 else 1393 Set_Ekind (Templ_Id, E_Generic_Procedure); 1394 end if; 1395 1396 -- When the generic subprogram acts as a compilation unit, inspect 1397 -- the Pragmas_After list for contract-related source pragmas. 1398 1399 if Nkind (Context) = N_Compilation_Unit then 1400 if Present (Aux_Decls_Node (Context)) 1401 and then Present (Pragmas_After (Aux_Decls_Node (Context))) 1402 then 1403 Decl := First (Pragmas_After (Aux_Decls_Node (Context))); 1404 end if; 1405 1406 -- Otherwise inspect the successive declarations for contract-related 1407 -- source pragmas. 1408 1409 else 1410 Decl := Next (Unit); 1411 end if; 1412 1413 -- A generic subprogram body carries contract-related source pragmas in 1414 -- its declarations. 1415 1416 elsif Nkind (Templ) = N_Subprogram_Body then 1417 Set_Ekind (Templ_Id, E_Subprogram_Body); 1418 1419 if Present (Declarations (Templ)) then 1420 Decl := First (Declarations (Templ)); 1421 end if; 1422 end if; 1423 1424 -- Inspect the relevant declarations looking for contract-related source 1425 -- pragmas and add them to the contract of the generic unit. 1426 1427 while Present (Decl) loop 1428 if Comes_From_Source (Decl) then 1429 if Nkind (Decl) = N_Pragma then 1430 1431 -- The source pragma is a contract annotation 1432 1433 if Is_Contract_Annotation (Decl) then 1434 Add_Generic_Contract_Pragma (Decl); 1435 end if; 1436 1437 -- The region where a contract-related source pragma may appear 1438 -- ends with the first source non-pragma declaration or statement. 1439 1440 else 1441 exit; 1442 end if; 1443 end if; 1444 1445 Next (Decl); 1446 end loop; 1447 end Create_Generic_Contract; 1448 1449 -------------------------------- 1450 -- Expand_Subprogram_Contract -- 1451 -------------------------------- 1452 1453 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is 1454 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 1455 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); 1456 1457 procedure Add_Invariant_And_Predicate_Checks 1458 (Subp_Id : Entity_Id; 1459 Stmts : in out List_Id; 1460 Result : out Node_Id); 1461 -- Process the result of function Subp_Id (if applicable) and all its 1462 -- formals. Add invariant and predicate checks where applicable. The 1463 -- routine appends all the checks to list Stmts. If Subp_Id denotes a 1464 -- function, Result contains the entity of parameter _Result, to be 1465 -- used in the creation of procedure _Postconditions. 1466 1467 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); 1468 -- Append a node to a list. If there is no list, create a new one. When 1469 -- the item denotes a pragma, it is added to the list only when it is 1470 -- enabled. 1471 1472 procedure Build_Postconditions_Procedure 1473 (Subp_Id : Entity_Id; 1474 Stmts : List_Id; 1475 Result : Entity_Id); 1476 -- Create the body of procedure _Postconditions which handles various 1477 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list 1478 -- of statements to be checked on exit. Parameter Result is the entity 1479 -- of parameter _Result when Subp_Id denotes a function. 1480 1481 procedure Process_Contract_Cases (Stmts : in out List_Id); 1482 -- Process pragma Contract_Cases. This routine prepends items to the 1483 -- body declarations and appends items to list Stmts. 1484 1485 procedure Process_Postconditions (Stmts : in out List_Id); 1486 -- Collect all [inherited] spec and body postconditions and accumulate 1487 -- their pragma Check equivalents in list Stmts. 1488 1489 procedure Process_Preconditions; 1490 -- Collect all [inherited] spec and body preconditions and prepend their 1491 -- pragma Check equivalents to the declarations of the body. 1492 1493 ---------------------------------------- 1494 -- Add_Invariant_And_Predicate_Checks -- 1495 ---------------------------------------- 1496 1497 procedure Add_Invariant_And_Predicate_Checks 1498 (Subp_Id : Entity_Id; 1499 Stmts : in out List_Id; 1500 Result : out Node_Id) 1501 is 1502 procedure Add_Invariant_Access_Checks (Id : Entity_Id); 1503 -- Id denotes the return value of a function or a formal parameter. 1504 -- Add an invariant check if the type of Id is access to a type with 1505 -- invariants. The routine appends the generated code to Stmts. 1506 1507 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; 1508 -- Determine whether type Typ can benefit from invariant checks. To 1509 -- qualify, the type must have a non-null invariant procedure and 1510 -- subprogram Subp_Id must appear visible from the point of view of 1511 -- the type. 1512 1513 --------------------------------- 1514 -- Add_Invariant_Access_Checks -- 1515 --------------------------------- 1516 1517 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is 1518 Loc : constant Source_Ptr := Sloc (Body_Decl); 1519 Ref : Node_Id; 1520 Typ : Entity_Id; 1521 1522 begin 1523 Typ := Etype (Id); 1524 1525 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then 1526 Typ := Designated_Type (Typ); 1527 1528 if Invariant_Checks_OK (Typ) then 1529 Ref := 1530 Make_Explicit_Dereference (Loc, 1531 Prefix => New_Occurrence_Of (Id, Loc)); 1532 Set_Etype (Ref, Typ); 1533 1534 -- Generate: 1535 -- if <Id> /= null then 1536 -- <invariant_call (<Ref>)> 1537 -- end if; 1538 1539 Append_Enabled_Item 1540 (Item => 1541 Make_If_Statement (Loc, 1542 Condition => 1543 Make_Op_Ne (Loc, 1544 Left_Opnd => New_Occurrence_Of (Id, Loc), 1545 Right_Opnd => Make_Null (Loc)), 1546 Then_Statements => New_List ( 1547 Make_Invariant_Call (Ref))), 1548 List => Stmts); 1549 end if; 1550 end if; 1551 end Add_Invariant_Access_Checks; 1552 1553 ------------------------- 1554 -- Invariant_Checks_OK -- 1555 ------------------------- 1556 1557 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is 1558 function Has_Public_Visibility_Of_Subprogram return Boolean; 1559 -- Determine whether type Typ has public visibility of subprogram 1560 -- Subp_Id. 1561 1562 ----------------------------------------- 1563 -- Has_Public_Visibility_Of_Subprogram -- 1564 ----------------------------------------- 1565 1566 function Has_Public_Visibility_Of_Subprogram return Boolean is 1567 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 1568 1569 begin 1570 -- An Initialization procedure must be considered visible even 1571 -- though it is internally generated. 1572 1573 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then 1574 return True; 1575 1576 elsif Ekind (Scope (Typ)) /= E_Package then 1577 return False; 1578 1579 -- Internally generated code is never publicly visible except 1580 -- for a subprogram that is the implementation of an expression 1581 -- function. In that case the visibility is determined by the 1582 -- last check. 1583 1584 elsif not Comes_From_Source (Subp_Decl) 1585 and then 1586 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function 1587 or else not 1588 Comes_From_Source (Defining_Entity (Subp_Decl))) 1589 then 1590 return False; 1591 1592 -- Determine whether the subprogram is declared in the visible 1593 -- declarations of the package containing the type, or in the 1594 -- visible declaration of a child unit of that package. 1595 1596 else 1597 declare 1598 Decls : constant List_Id := 1599 List_Containing (Subp_Decl); 1600 Subp_Scope : constant Entity_Id := 1601 Scope (Defining_Entity (Subp_Decl)); 1602 Typ_Scope : constant Entity_Id := Scope (Typ); 1603 1604 begin 1605 return 1606 Decls = Visible_Declarations 1607 (Specification (Unit_Declaration_Node (Typ_Scope))) 1608 1609 or else 1610 (Ekind (Subp_Scope) = E_Package 1611 and then Typ_Scope /= Subp_Scope 1612 and then Is_Child_Unit (Subp_Scope) 1613 and then 1614 Is_Ancestor_Package (Typ_Scope, Subp_Scope) 1615 and then 1616 Decls = Visible_Declarations 1617 (Specification 1618 (Unit_Declaration_Node (Subp_Scope)))); 1619 end; 1620 end if; 1621 end Has_Public_Visibility_Of_Subprogram; 1622 1623 -- Start of processing for Invariant_Checks_OK 1624 1625 begin 1626 return 1627 Has_Invariants (Typ) 1628 and then Present (Invariant_Procedure (Typ)) 1629 and then not Has_Null_Body (Invariant_Procedure (Typ)) 1630 and then Has_Public_Visibility_Of_Subprogram; 1631 end Invariant_Checks_OK; 1632 1633 -- Local variables 1634 1635 Loc : constant Source_Ptr := Sloc (Body_Decl); 1636 -- Source location of subprogram body contract 1637 1638 Formal : Entity_Id; 1639 Typ : Entity_Id; 1640 1641 -- Start of processing for Add_Invariant_And_Predicate_Checks 1642 1643 begin 1644 Result := Empty; 1645 1646 -- Process the result of a function 1647 1648 if Ekind (Subp_Id) = E_Function then 1649 Typ := Etype (Subp_Id); 1650 1651 -- Generate _Result which is used in procedure _Postconditions to 1652 -- verify the return value. 1653 1654 Result := Make_Defining_Identifier (Loc, Name_uResult); 1655 Set_Etype (Result, Typ); 1656 1657 -- Add an invariant check when the return type has invariants and 1658 -- the related function is visible to the outside. 1659 1660 if Invariant_Checks_OK (Typ) then 1661 Append_Enabled_Item 1662 (Item => 1663 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), 1664 List => Stmts); 1665 end if; 1666 1667 -- Add an invariant check when the return type is an access to a 1668 -- type with invariants. 1669 1670 Add_Invariant_Access_Checks (Result); 1671 end if; 1672 1673 -- Add invariant and predicates for all formals that qualify 1674 1675 Formal := First_Formal (Subp_Id); 1676 while Present (Formal) loop 1677 Typ := Etype (Formal); 1678 1679 if Ekind (Formal) /= E_In_Parameter 1680 or else Is_Access_Type (Typ) 1681 then 1682 if Invariant_Checks_OK (Typ) then 1683 Append_Enabled_Item 1684 (Item => 1685 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), 1686 List => Stmts); 1687 end if; 1688 1689 Add_Invariant_Access_Checks (Formal); 1690 1691 -- Note: we used to add predicate checks for OUT and IN OUT 1692 -- formals here, but that was misguided, since such checks are 1693 -- performed on the caller side, based on the predicate of the 1694 -- actual, rather than the predicate of the formal. 1695 1696 end if; 1697 1698 Next_Formal (Formal); 1699 end loop; 1700 end Add_Invariant_And_Predicate_Checks; 1701 1702 ------------------------- 1703 -- Append_Enabled_Item -- 1704 ------------------------- 1705 1706 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is 1707 begin 1708 -- Do not chain ignored or disabled pragmas 1709 1710 if Nkind (Item) = N_Pragma 1711 and then (Is_Ignored (Item) or else Is_Disabled (Item)) 1712 then 1713 null; 1714 1715 -- Otherwise, add the item 1716 1717 else 1718 if No (List) then 1719 List := New_List; 1720 end if; 1721 1722 -- If the pragma is a conjunct in a composite postcondition, it 1723 -- has been processed in reverse order. In the postcondition body 1724 -- it must appear before the others. 1725 1726 if Nkind (Item) = N_Pragma 1727 and then From_Aspect_Specification (Item) 1728 and then Split_PPC (Item) 1729 then 1730 Prepend (Item, List); 1731 else 1732 Append (Item, List); 1733 end if; 1734 end if; 1735 end Append_Enabled_Item; 1736 1737 ------------------------------------ 1738 -- Build_Postconditions_Procedure -- 1739 ------------------------------------ 1740 1741 procedure Build_Postconditions_Procedure 1742 (Subp_Id : Entity_Id; 1743 Stmts : List_Id; 1744 Result : Entity_Id) 1745 is 1746 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); 1747 -- Insert node Stmt before the first source declaration of the 1748 -- related subprogram's body. If no such declaration exists, Stmt 1749 -- becomes the last declaration. 1750 1751 -------------------------------------------- 1752 -- Insert_Before_First_Source_Declaration -- 1753 -------------------------------------------- 1754 1755 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is 1756 Decls : constant List_Id := Declarations (Body_Decl); 1757 Decl : Node_Id; 1758 1759 begin 1760 -- Inspect the declarations of the related subprogram body looking 1761 -- for the first source declaration. 1762 1763 if Present (Decls) then 1764 Decl := First (Decls); 1765 while Present (Decl) loop 1766 if Comes_From_Source (Decl) then 1767 Insert_Before (Decl, Stmt); 1768 return; 1769 end if; 1770 1771 Next (Decl); 1772 end loop; 1773 1774 -- If we get there, then the subprogram body lacks any source 1775 -- declarations. The body of _Postconditions now acts as the 1776 -- last declaration. 1777 1778 Append (Stmt, Decls); 1779 1780 -- Ensure that the body has a declaration list 1781 1782 else 1783 Set_Declarations (Body_Decl, New_List (Stmt)); 1784 end if; 1785 end Insert_Before_First_Source_Declaration; 1786 1787 -- Local variables 1788 1789 Loc : constant Source_Ptr := Sloc (Body_Decl); 1790 Params : List_Id := No_List; 1791 Proc_Bod : Node_Id; 1792 Proc_Decl : Node_Id; 1793 Proc_Id : Entity_Id; 1794 Proc_Spec : Node_Id; 1795 1796 -- Start of processing for Build_Postconditions_Procedure 1797 1798 begin 1799 -- Nothing to do if there are no actions to check on exit 1800 1801 if No (Stmts) then 1802 return; 1803 end if; 1804 1805 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); 1806 Set_Debug_Info_Needed (Proc_Id); 1807 Set_Postconditions_Proc (Subp_Id, Proc_Id); 1808 1809 -- Force the front-end inlining of _Postconditions when generating C 1810 -- code, since its body may have references to itypes defined in the 1811 -- enclosing subprogram, which would cause problems for unnesting 1812 -- routines in the absence of inlining. 1813 1814 if Modify_Tree_For_C then 1815 Set_Has_Pragma_Inline (Proc_Id); 1816 Set_Has_Pragma_Inline_Always (Proc_Id); 1817 Set_Is_Inlined (Proc_Id); 1818 end if; 1819 1820 -- The related subprogram is a function: create the specification of 1821 -- parameter _Result. 1822 1823 if Present (Result) then 1824 Params := New_List ( 1825 Make_Parameter_Specification (Loc, 1826 Defining_Identifier => Result, 1827 Parameter_Type => 1828 New_Occurrence_Of (Etype (Result), Loc))); 1829 end if; 1830 1831 Proc_Spec := 1832 Make_Procedure_Specification (Loc, 1833 Defining_Unit_Name => Proc_Id, 1834 Parameter_Specifications => Params); 1835 1836 Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); 1837 1838 -- Insert _Postconditions before the first source declaration of the 1839 -- body. This ensures that the body will not cause any premature 1840 -- freezing, as it may mention types: 1841 1842 -- procedure Proc (Obj : Array_Typ) is 1843 -- procedure _postconditions is 1844 -- begin 1845 -- ... Obj ... 1846 -- end _postconditions; 1847 1848 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); 1849 -- begin 1850 1851 -- In the example above, Obj is of type T but the incorrect placement 1852 -- of _Postconditions will cause a crash in gigi due to an out-of- 1853 -- order reference. The body of _Postconditions must be placed after 1854 -- the declaration of Temp to preserve correct visibility. 1855 1856 Insert_Before_First_Source_Declaration (Proc_Decl); 1857 Analyze (Proc_Decl); 1858 1859 -- Set an explicit End_Label to override the sloc of the implicit 1860 -- RETURN statement, and prevent it from inheriting the sloc of one 1861 -- the postconditions: this would cause confusing debug info to be 1862 -- produced, interfering with coverage-analysis tools. 1863 1864 Proc_Bod := 1865 Make_Subprogram_Body (Loc, 1866 Specification => 1867 Copy_Subprogram_Spec (Proc_Spec), 1868 Declarations => Empty_List, 1869 Handled_Statement_Sequence => 1870 Make_Handled_Sequence_Of_Statements (Loc, 1871 Statements => Stmts, 1872 End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); 1873 1874 Insert_After_And_Analyze (Proc_Decl, Proc_Bod); 1875 end Build_Postconditions_Procedure; 1876 1877 ---------------------------- 1878 -- Process_Contract_Cases -- 1879 ---------------------------- 1880 1881 procedure Process_Contract_Cases (Stmts : in out List_Id) is 1882 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); 1883 -- Process pragma Contract_Cases for subprogram Subp_Id 1884 1885 -------------------------------- 1886 -- Process_Contract_Cases_For -- 1887 -------------------------------- 1888 1889 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is 1890 Items : constant Node_Id := Contract (Subp_Id); 1891 Prag : Node_Id; 1892 1893 begin 1894 if Present (Items) then 1895 Prag := Contract_Test_Cases (Items); 1896 while Present (Prag) loop 1897 if Pragma_Name (Prag) = Name_Contract_Cases 1898 and then Is_Checked (Prag) 1899 then 1900 Expand_Pragma_Contract_Cases 1901 (CCs => Prag, 1902 Subp_Id => Subp_Id, 1903 Decls => Declarations (Body_Decl), 1904 Stmts => Stmts); 1905 end if; 1906 1907 Prag := Next_Pragma (Prag); 1908 end loop; 1909 end if; 1910 end Process_Contract_Cases_For; 1911 1912 pragma Unmodified (Stmts); 1913 -- Stmts is passed as IN OUT to signal that the list can be updated, 1914 -- even if the corresponding integer value representing the list does 1915 -- not change. 1916 1917 -- Start of processing for Process_Contract_Cases 1918 1919 begin 1920 Process_Contract_Cases_For (Body_Id); 1921 1922 if Present (Spec_Id) then 1923 Process_Contract_Cases_For (Spec_Id); 1924 end if; 1925 end Process_Contract_Cases; 1926 1927 ---------------------------- 1928 -- Process_Postconditions -- 1929 ---------------------------- 1930 1931 procedure Process_Postconditions (Stmts : in out List_Id) is 1932 procedure Process_Body_Postconditions (Post_Nam : Name_Id); 1933 -- Collect all [refined] postconditions of a specific kind denoted 1934 -- by Post_Nam that belong to the body, and generate pragma Check 1935 -- equivalents in list Stmts. 1936 1937 procedure Process_Spec_Postconditions; 1938 -- Collect all [inherited] postconditions of the spec, and generate 1939 -- pragma Check equivalents in list Stmts. 1940 1941 --------------------------------- 1942 -- Process_Body_Postconditions -- 1943 --------------------------------- 1944 1945 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is 1946 Items : constant Node_Id := Contract (Body_Id); 1947 Unit_Decl : constant Node_Id := Parent (Body_Decl); 1948 Decl : Node_Id; 1949 Prag : Node_Id; 1950 1951 begin 1952 -- Process the contract 1953 1954 if Present (Items) then 1955 Prag := Pre_Post_Conditions (Items); 1956 while Present (Prag) loop 1957 if Pragma_Name (Prag) = Post_Nam 1958 and then Is_Checked (Prag) 1959 then 1960 Append_Enabled_Item 1961 (Item => Build_Pragma_Check_Equivalent (Prag), 1962 List => Stmts); 1963 end if; 1964 1965 Prag := Next_Pragma (Prag); 1966 end loop; 1967 end if; 1968 1969 -- The subprogram body being processed is actually the proper body 1970 -- of a stub with a corresponding spec. The subprogram stub may 1971 -- carry a postcondition pragma, in which case it must be taken 1972 -- into account. The pragma appears after the stub. 1973 1974 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then 1975 Decl := Next (Corresponding_Stub (Unit_Decl)); 1976 while Present (Decl) loop 1977 1978 -- Note that non-matching pragmas are skipped 1979 1980 if Nkind (Decl) = N_Pragma then 1981 if Pragma_Name (Decl) = Post_Nam 1982 and then Is_Checked (Decl) 1983 then 1984 Append_Enabled_Item 1985 (Item => Build_Pragma_Check_Equivalent (Decl), 1986 List => Stmts); 1987 end if; 1988 1989 -- Skip internally generated code 1990 1991 elsif not Comes_From_Source (Decl) then 1992 null; 1993 1994 -- Postcondition pragmas are usually grouped together. There 1995 -- is no need to inspect the whole declarative list. 1996 1997 else 1998 exit; 1999 end if; 2000 2001 Next (Decl); 2002 end loop; 2003 end if; 2004 end Process_Body_Postconditions; 2005 2006 --------------------------------- 2007 -- Process_Spec_Postconditions -- 2008 --------------------------------- 2009 2010 procedure Process_Spec_Postconditions is 2011 Subps : constant Subprogram_List := 2012 Inherited_Subprograms (Spec_Id); 2013 Item : Node_Id; 2014 Items : Node_Id; 2015 Prag : Node_Id; 2016 Subp_Id : Entity_Id; 2017 2018 begin 2019 -- Process the contract 2020 2021 Items := Contract (Spec_Id); 2022 2023 if Present (Items) then 2024 Prag := Pre_Post_Conditions (Items); 2025 while Present (Prag) loop 2026 if Pragma_Name (Prag) = Name_Postcondition 2027 and then Is_Checked (Prag) 2028 then 2029 Append_Enabled_Item 2030 (Item => Build_Pragma_Check_Equivalent (Prag), 2031 List => Stmts); 2032 end if; 2033 2034 Prag := Next_Pragma (Prag); 2035 end loop; 2036 end if; 2037 2038 -- Process the contracts of all inherited subprograms, looking for 2039 -- class-wide postconditions. 2040 2041 for Index in Subps'Range loop 2042 Subp_Id := Subps (Index); 2043 Items := Contract (Subp_Id); 2044 2045 if Present (Items) then 2046 Prag := Pre_Post_Conditions (Items); 2047 while Present (Prag) loop 2048 if Pragma_Name (Prag) = Name_Postcondition 2049 and then Class_Present (Prag) 2050 then 2051 Item := 2052 Build_Pragma_Check_Equivalent 2053 (Prag => Prag, 2054 Subp_Id => Spec_Id, 2055 Inher_Id => Subp_Id); 2056 2057 -- The pragma Check equivalent of the class-wide 2058 -- postcondition is still created even though the 2059 -- pragma may be ignored because the equivalent 2060 -- performs semantic checks. 2061 2062 if Is_Checked (Prag) then 2063 Append_Enabled_Item (Item, Stmts); 2064 end if; 2065 end if; 2066 2067 Prag := Next_Pragma (Prag); 2068 end loop; 2069 end if; 2070 end loop; 2071 end Process_Spec_Postconditions; 2072 2073 pragma Unmodified (Stmts); 2074 -- Stmts is passed as IN OUT to signal that the list can be updated, 2075 -- even if the corresponding integer value representing the list does 2076 -- not change. 2077 2078 -- Start of processing for Process_Postconditions 2079 2080 begin 2081 -- The processing of postconditions is done in reverse order (body 2082 -- first) to ensure the following arrangement: 2083 2084 -- <refined postconditions from body> 2085 -- <postconditions from body> 2086 -- <postconditions from spec> 2087 -- <inherited postconditions> 2088 2089 Process_Body_Postconditions (Name_Refined_Post); 2090 Process_Body_Postconditions (Name_Postcondition); 2091 2092 if Present (Spec_Id) then 2093 Process_Spec_Postconditions; 2094 end if; 2095 end Process_Postconditions; 2096 2097 --------------------------- 2098 -- Process_Preconditions -- 2099 --------------------------- 2100 2101 procedure Process_Preconditions is 2102 Class_Pre : Node_Id := Empty; 2103 -- The sole [inherited] class-wide precondition pragma that applies 2104 -- to the subprogram. 2105 2106 Insert_Node : Node_Id := Empty; 2107 -- The insertion node after which all pragma Check equivalents are 2108 -- inserted. 2109 2110 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; 2111 -- Determine whether arbitrary declaration Decl denotes a renaming of 2112 -- a discriminant or protection field _object. 2113 2114 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); 2115 -- Merge two class-wide preconditions by "or else"-ing them. The 2116 -- changes are accumulated in parameter Into. Update the error 2117 -- message of Into. 2118 2119 procedure Prepend_To_Decls (Item : Node_Id); 2120 -- Prepend a single item to the declarations of the subprogram body 2121 2122 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); 2123 -- Save a class-wide precondition into Class_Pre, or prepend a normal 2124 -- precondition to the declarations of the body and analyze it. 2125 2126 procedure Process_Inherited_Preconditions; 2127 -- Collect all inherited class-wide preconditions and merge them into 2128 -- one big precondition to be evaluated as pragma Check. 2129 2130 procedure Process_Preconditions_For (Subp_Id : Entity_Id); 2131 -- Collect all preconditions of subprogram Subp_Id and prepend their 2132 -- pragma Check equivalents to the declarations of the body. 2133 2134 -------------------------- 2135 -- Is_Prologue_Renaming -- 2136 -------------------------- 2137 2138 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is 2139 Nam : Node_Id; 2140 Obj : Entity_Id; 2141 Pref : Node_Id; 2142 Sel : Node_Id; 2143 2144 begin 2145 if Nkind (Decl) = N_Object_Renaming_Declaration then 2146 Obj := Defining_Entity (Decl); 2147 Nam := Name (Decl); 2148 2149 if Nkind (Nam) = N_Selected_Component then 2150 Pref := Prefix (Nam); 2151 Sel := Selector_Name (Nam); 2152 2153 -- A discriminant renaming appears as 2154 -- Discr : constant ... := Prefix.Discr; 2155 2156 if Ekind (Obj) = E_Constant 2157 and then Is_Entity_Name (Sel) 2158 and then Present (Entity (Sel)) 2159 and then Ekind (Entity (Sel)) = E_Discriminant 2160 then 2161 return True; 2162 2163 -- A protection field renaming appears as 2164 -- Prot : ... := _object._object; 2165 2166 -- A renamed private component is just a component of 2167 -- _object, with an arbitrary name. 2168 2169 elsif Ekind (Obj) = E_Variable 2170 and then Nkind (Pref) = N_Identifier 2171 and then Chars (Pref) = Name_uObject 2172 and then Nkind (Sel) = N_Identifier 2173 then 2174 return True; 2175 end if; 2176 end if; 2177 end if; 2178 2179 return False; 2180 end Is_Prologue_Renaming; 2181 2182 ------------------------- 2183 -- Merge_Preconditions -- 2184 ------------------------- 2185 2186 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is 2187 function Expression_Arg (Prag : Node_Id) return Node_Id; 2188 -- Return the boolean expression argument of a precondition while 2189 -- updating its parentheses count for the subsequent merge. 2190 2191 function Message_Arg (Prag : Node_Id) return Node_Id; 2192 -- Return the message argument of a precondition 2193 2194 -------------------- 2195 -- Expression_Arg -- 2196 -------------------- 2197 2198 function Expression_Arg (Prag : Node_Id) return Node_Id is 2199 Args : constant List_Id := Pragma_Argument_Associations (Prag); 2200 Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); 2201 2202 begin 2203 if Paren_Count (Arg) = 0 then 2204 Set_Paren_Count (Arg, 1); 2205 end if; 2206 2207 return Arg; 2208 end Expression_Arg; 2209 2210 ----------------- 2211 -- Message_Arg -- 2212 ----------------- 2213 2214 function Message_Arg (Prag : Node_Id) return Node_Id is 2215 Args : constant List_Id := Pragma_Argument_Associations (Prag); 2216 begin 2217 return Get_Pragma_Arg (Last (Args)); 2218 end Message_Arg; 2219 2220 -- Local variables 2221 2222 From_Expr : constant Node_Id := Expression_Arg (From); 2223 From_Msg : constant Node_Id := Message_Arg (From); 2224 Into_Expr : constant Node_Id := Expression_Arg (Into); 2225 Into_Msg : constant Node_Id := Message_Arg (Into); 2226 Loc : constant Source_Ptr := Sloc (Into); 2227 2228 -- Start of processing for Merge_Preconditions 2229 2230 begin 2231 -- Merge the two preconditions by "or else"-ing them 2232 2233 Rewrite (Into_Expr, 2234 Make_Or_Else (Loc, 2235 Right_Opnd => Relocate_Node (Into_Expr), 2236 Left_Opnd => From_Expr)); 2237 2238 -- Merge the two error messages to produce a single message of the 2239 -- form: 2240 2241 -- failed precondition from ... 2242 -- also failed inherited precondition from ... 2243 2244 if not Exception_Locations_Suppressed then 2245 Start_String (Strval (Into_Msg)); 2246 Store_String_Char (ASCII.LF); 2247 Store_String_Chars (" also "); 2248 Store_String_Chars (Strval (From_Msg)); 2249 2250 Set_Strval (Into_Msg, End_String); 2251 end if; 2252 end Merge_Preconditions; 2253 2254 ---------------------- 2255 -- Prepend_To_Decls -- 2256 ---------------------- 2257 2258 procedure Prepend_To_Decls (Item : Node_Id) is 2259 Decls : List_Id; 2260 2261 begin 2262 Decls := Declarations (Body_Decl); 2263 2264 -- Ensure that the body has a declarative list 2265 2266 if No (Decls) then 2267 Decls := New_List; 2268 Set_Declarations (Body_Decl, Decls); 2269 end if; 2270 2271 Prepend_To (Decls, Item); 2272 end Prepend_To_Decls; 2273 2274 ------------------------------ 2275 -- Prepend_To_Decls_Or_Save -- 2276 ------------------------------ 2277 2278 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is 2279 Check_Prag : Node_Id; 2280 2281 begin 2282 Check_Prag := Build_Pragma_Check_Equivalent (Prag); 2283 2284 -- Save the sole class-wide precondition (if any) for the next 2285 -- step, where it will be merged with inherited preconditions. 2286 2287 if Class_Present (Prag) then 2288 pragma Assert (No (Class_Pre)); 2289 Class_Pre := Check_Prag; 2290 2291 -- Accumulate the corresponding Check pragmas at the top of the 2292 -- declarations. Prepending the items ensures that they will be 2293 -- evaluated in their original order. 2294 2295 else 2296 if Present (Insert_Node) then 2297 Insert_After (Insert_Node, Check_Prag); 2298 else 2299 Prepend_To_Decls (Check_Prag); 2300 end if; 2301 2302 Analyze (Check_Prag); 2303 end if; 2304 end Prepend_To_Decls_Or_Save; 2305 2306 ------------------------------------- 2307 -- Process_Inherited_Preconditions -- 2308 ------------------------------------- 2309 2310 procedure Process_Inherited_Preconditions is 2311 Subps : constant Subprogram_List := 2312 Inherited_Subprograms (Spec_Id); 2313 2314 Item : Node_Id; 2315 Items : Node_Id; 2316 Prag : Node_Id; 2317 Subp_Id : Entity_Id; 2318 2319 begin 2320 -- Process the contracts of all inherited subprograms, looking for 2321 -- class-wide preconditions. 2322 2323 for Index in Subps'Range loop 2324 Subp_Id := Subps (Index); 2325 Items := Contract (Subp_Id); 2326 2327 if Present (Items) then 2328 Prag := Pre_Post_Conditions (Items); 2329 while Present (Prag) loop 2330 if Pragma_Name (Prag) = Name_Precondition 2331 and then Class_Present (Prag) 2332 then 2333 Item := 2334 Build_Pragma_Check_Equivalent 2335 (Prag => Prag, 2336 Subp_Id => Spec_Id, 2337 Inher_Id => Subp_Id); 2338 2339 -- The pragma Check equivalent of the class-wide 2340 -- precondition is still created even though the 2341 -- pragma may be ignored because the equivalent 2342 -- performs semantic checks. 2343 2344 if Is_Checked (Prag) then 2345 2346 -- The spec of an inherited subprogram already 2347 -- yielded a class-wide precondition. Merge the 2348 -- existing precondition with the current one 2349 -- using "or else". 2350 2351 if Present (Class_Pre) then 2352 Merge_Preconditions (Item, Class_Pre); 2353 else 2354 Class_Pre := Item; 2355 end if; 2356 end if; 2357 end if; 2358 2359 Prag := Next_Pragma (Prag); 2360 end loop; 2361 end if; 2362 end loop; 2363 2364 -- Add the merged class-wide preconditions 2365 2366 if Present (Class_Pre) then 2367 Prepend_To_Decls (Class_Pre); 2368 Analyze (Class_Pre); 2369 end if; 2370 end Process_Inherited_Preconditions; 2371 2372 ------------------------------- 2373 -- Process_Preconditions_For -- 2374 ------------------------------- 2375 2376 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is 2377 Items : constant Node_Id := Contract (Subp_Id); 2378 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 2379 Decl : Node_Id; 2380 Freeze_T : Boolean; 2381 Prag : Node_Id; 2382 2383 begin 2384 -- Process the contract. If the body is an expression function 2385 -- that is a completion, freeze types within, because this may 2386 -- not have been done yet, when the subprogram declaration and 2387 -- its completion by an expression function appear in distinct 2388 -- declarative lists of the same unit (visible and private). 2389 2390 Freeze_T := 2391 Was_Expression_Function (Body_Decl) 2392 and then Sloc (Body_Id) /= Sloc (Subp_Id) 2393 and then In_Same_Source_Unit (Body_Id, Subp_Id) 2394 and then List_Containing (Body_Decl) /= 2395 List_Containing (Subp_Decl) 2396 and then not In_Instance; 2397 2398 if Present (Items) then 2399 Prag := Pre_Post_Conditions (Items); 2400 while Present (Prag) loop 2401 if Pragma_Name (Prag) = Name_Precondition 2402 and then Is_Checked (Prag) 2403 then 2404 if Freeze_T 2405 and then Present (Corresponding_Aspect (Prag)) 2406 then 2407 Freeze_Expr_Types 2408 (Def_Id => Subp_Id, 2409 Typ => Standard_Boolean, 2410 Expr => Expression (Corresponding_Aspect (Prag)), 2411 N => Body_Decl); 2412 end if; 2413 2414 Prepend_To_Decls_Or_Save (Prag); 2415 end if; 2416 2417 Prag := Next_Pragma (Prag); 2418 end loop; 2419 end if; 2420 2421 -- The subprogram declaration being processed is actually a body 2422 -- stub. The stub may carry a precondition pragma, in which case 2423 -- it must be taken into account. The pragma appears after the 2424 -- stub. 2425 2426 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then 2427 2428 -- Inspect the declarations following the body stub 2429 2430 Decl := Next (Subp_Decl); 2431 while Present (Decl) loop 2432 2433 -- Note that non-matching pragmas are skipped 2434 2435 if Nkind (Decl) = N_Pragma then 2436 if Pragma_Name (Decl) = Name_Precondition 2437 and then Is_Checked (Decl) 2438 then 2439 Prepend_To_Decls_Or_Save (Decl); 2440 end if; 2441 2442 -- Skip internally generated code 2443 2444 elsif not Comes_From_Source (Decl) then 2445 null; 2446 2447 -- Preconditions are usually grouped together. There is no 2448 -- need to inspect the whole declarative list. 2449 2450 else 2451 exit; 2452 end if; 2453 2454 Next (Decl); 2455 end loop; 2456 end if; 2457 end Process_Preconditions_For; 2458 2459 -- Local variables 2460 2461 Decls : constant List_Id := Declarations (Body_Decl); 2462 Decl : Node_Id; 2463 2464 -- Start of processing for Process_Preconditions 2465 2466 begin 2467 -- Find the proper insertion point for all pragma Check equivalents 2468 2469 if Present (Decls) then 2470 Decl := First (Decls); 2471 while Present (Decl) loop 2472 2473 -- First source declaration terminates the search, because all 2474 -- preconditions must be evaluated prior to it, by definition. 2475 2476 if Comes_From_Source (Decl) then 2477 exit; 2478 2479 -- Certain internally generated object renamings such as those 2480 -- for discriminants and protection fields must be elaborated 2481 -- before the preconditions are evaluated, as their expressions 2482 -- may mention the discriminants. The renamings include those 2483 -- for private components so we need to find the last such. 2484 2485 elsif Is_Prologue_Renaming (Decl) then 2486 while Present (Next (Decl)) 2487 and then Is_Prologue_Renaming (Next (Decl)) 2488 loop 2489 Next (Decl); 2490 end loop; 2491 2492 Insert_Node := Decl; 2493 2494 -- Otherwise the declaration does not come from source. This 2495 -- also terminates the search, because internal code may raise 2496 -- exceptions which should not preempt the preconditions. 2497 2498 else 2499 exit; 2500 end if; 2501 2502 Next (Decl); 2503 end loop; 2504 end if; 2505 2506 -- The processing of preconditions is done in reverse order (body 2507 -- first), because each pragma Check equivalent is inserted at the 2508 -- top of the declarations. This ensures that the final order is 2509 -- consistent with following diagram: 2510 2511 -- <inherited preconditions> 2512 -- <preconditions from spec> 2513 -- <preconditions from body> 2514 2515 Process_Preconditions_For (Body_Id); 2516 2517 if Present (Spec_Id) then 2518 Process_Preconditions_For (Spec_Id); 2519 Process_Inherited_Preconditions; 2520 end if; 2521 end Process_Preconditions; 2522 2523 -- Local variables 2524 2525 Restore_Scope : Boolean := False; 2526 Result : Entity_Id; 2527 Stmts : List_Id := No_List; 2528 Subp_Id : Entity_Id; 2529 2530 -- Start of processing for Expand_Subprogram_Contract 2531 2532 begin 2533 -- Obtain the entity of the initial declaration 2534 2535 if Present (Spec_Id) then 2536 Subp_Id := Spec_Id; 2537 else 2538 Subp_Id := Body_Id; 2539 end if; 2540 2541 -- Do not perform expansion activity when it is not needed 2542 2543 if not Expander_Active then 2544 return; 2545 2546 -- ASIS requires an unaltered tree 2547 2548 elsif ASIS_Mode then 2549 return; 2550 2551 -- GNATprove does not need the executable semantics of a contract 2552 2553 elsif GNATprove_Mode then 2554 return; 2555 2556 -- The contract of a generic subprogram or one declared in a generic 2557 -- context is not expanded, as the corresponding instance will provide 2558 -- the executable semantics of the contract. 2559 2560 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then 2561 return; 2562 2563 -- All subprograms carry a contract, but for some it is not significant 2564 -- and should not be processed. This is a small optimization. 2565 2566 elsif not Has_Significant_Contract (Subp_Id) then 2567 return; 2568 2569 -- The contract of an ignored Ghost subprogram does not need expansion, 2570 -- because the subprogram and all calls to it will be removed. 2571 2572 elsif Is_Ignored_Ghost_Entity (Subp_Id) then 2573 return; 2574 2575 -- Do not re-expand the same contract. This scenario occurs when a 2576 -- construct is rewritten into something else during its analysis 2577 -- (expression functions for instance). 2578 2579 elsif Has_Expanded_Contract (Subp_Id) then 2580 return; 2581 end if; 2582 2583 -- Prevent multiple expansion attempts of the same contract 2584 2585 Set_Has_Expanded_Contract (Subp_Id); 2586 2587 -- Ensure that the formal parameters are visible when expanding all 2588 -- contract items. 2589 2590 if not In_Open_Scopes (Subp_Id) then 2591 Restore_Scope := True; 2592 Push_Scope (Subp_Id); 2593 2594 if Is_Generic_Subprogram (Subp_Id) then 2595 Install_Generic_Formals (Subp_Id); 2596 else 2597 Install_Formals (Subp_Id); 2598 end if; 2599 end if; 2600 2601 -- The expansion of a subprogram contract involves the creation of Check 2602 -- pragmas to verify the contract assertions of the spec and body in a 2603 -- particular order. The order is as follows: 2604 2605 -- function Example (...) return ... is 2606 -- procedure _Postconditions (...) is 2607 -- begin 2608 -- <refined postconditions from body> 2609 -- <postconditions from body> 2610 -- <postconditions from spec> 2611 -- <inherited postconditions> 2612 -- <contract case consequences> 2613 -- <invariant check of function result> 2614 -- <invariant and predicate checks of parameters> 2615 -- end _Postconditions; 2616 2617 -- <inherited preconditions> 2618 -- <preconditions from spec> 2619 -- <preconditions from body> 2620 -- <contract case conditions> 2621 2622 -- <source declarations> 2623 -- begin 2624 -- <source statements> 2625 2626 -- _Preconditions (Result); 2627 -- return Result; 2628 -- end Example; 2629 2630 -- Routine _Postconditions holds all contract assertions that must be 2631 -- verified on exit from the related subprogram. 2632 2633 -- Step 1: Handle all preconditions. This action must come before the 2634 -- processing of pragma Contract_Cases because the pragma prepends items 2635 -- to the body declarations. 2636 2637 Process_Preconditions; 2638 2639 -- Step 2: Handle all postconditions. This action must come before the 2640 -- processing of pragma Contract_Cases because the pragma appends items 2641 -- to list Stmts. 2642 2643 Process_Postconditions (Stmts); 2644 2645 -- Step 3: Handle pragma Contract_Cases. This action must come before 2646 -- the processing of invariants and predicates because those append 2647 -- items to list Stmts. 2648 2649 Process_Contract_Cases (Stmts); 2650 2651 -- Step 4: Apply invariant and predicate checks on a function result and 2652 -- all formals. The resulting checks are accumulated in list Stmts. 2653 2654 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); 2655 2656 -- Step 5: Construct procedure _Postconditions 2657 2658 Build_Postconditions_Procedure (Subp_Id, Stmts, Result); 2659 2660 if Restore_Scope then 2661 End_Scope; 2662 end if; 2663 end Expand_Subprogram_Contract; 2664 2665 ------------------------------- 2666 -- Freeze_Previous_Contracts -- 2667 ------------------------------- 2668 2669 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is 2670 function Causes_Contract_Freezing (N : Node_Id) return Boolean; 2671 pragma Inline (Causes_Contract_Freezing); 2672 -- Determine whether arbitrary node N causes contract freezing 2673 2674 procedure Freeze_Contracts; 2675 pragma Inline (Freeze_Contracts); 2676 -- Freeze the contracts of all eligible constructs which precede body 2677 -- Body_Decl. 2678 2679 procedure Freeze_Enclosing_Package_Body; 2680 pragma Inline (Freeze_Enclosing_Package_Body); 2681 -- Freeze the contract of the nearest package body (if any) which 2682 -- encloses body Body_Decl. 2683 2684 ------------------------------ 2685 -- Causes_Contract_Freezing -- 2686 ------------------------------ 2687 2688 function Causes_Contract_Freezing (N : Node_Id) return Boolean is 2689 begin 2690 return Nkind_In (N, N_Entry_Body, 2691 N_Package_Body, 2692 N_Protected_Body, 2693 N_Subprogram_Body, 2694 N_Subprogram_Body_Stub, 2695 N_Task_Body); 2696 end Causes_Contract_Freezing; 2697 2698 ---------------------- 2699 -- Freeze_Contracts -- 2700 ---------------------- 2701 2702 procedure Freeze_Contracts is 2703 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); 2704 Decl : Node_Id; 2705 2706 begin 2707 -- Nothing to do when the body which causes freezing does not appear 2708 -- in a declarative list because there cannot possibly be constructs 2709 -- with contracts. 2710 2711 if not Is_List_Member (Body_Decl) then 2712 return; 2713 end if; 2714 2715 -- Inspect the declarations preceding the body, and freeze individual 2716 -- contracts of eligible constructs. 2717 2718 Decl := Prev (Body_Decl); 2719 while Present (Decl) loop 2720 2721 -- Stop the traversal when a preceding construct that causes 2722 -- freezing is encountered as there is no point in refreezing 2723 -- the already frozen constructs. 2724 2725 if Causes_Contract_Freezing (Decl) then 2726 exit; 2727 2728 -- Entry or subprogram declarations 2729 2730 elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, 2731 N_Entry_Declaration, 2732 N_Generic_Subprogram_Declaration, 2733 N_Subprogram_Declaration) 2734 then 2735 Analyze_Entry_Or_Subprogram_Contract 2736 (Subp_Id => Defining_Entity (Decl), 2737 Freeze_Id => Body_Id); 2738 2739 -- Objects 2740 2741 elsif Nkind (Decl) = N_Object_Declaration then 2742 Analyze_Object_Contract 2743 (Obj_Id => Defining_Entity (Decl), 2744 Freeze_Id => Body_Id); 2745 2746 -- Protected units 2747 2748 elsif Nkind_In (Decl, N_Protected_Type_Declaration, 2749 N_Single_Protected_Declaration) 2750 then 2751 Analyze_Protected_Contract (Defining_Entity (Decl)); 2752 2753 -- Subprogram body stubs 2754 2755 elsif Nkind (Decl) = N_Subprogram_Body_Stub then 2756 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); 2757 2758 -- Task units 2759 2760 elsif Nkind_In (Decl, N_Single_Task_Declaration, 2761 N_Task_Type_Declaration) 2762 then 2763 Analyze_Task_Contract (Defining_Entity (Decl)); 2764 end if; 2765 2766 Prev (Decl); 2767 end loop; 2768 end Freeze_Contracts; 2769 2770 ----------------------------------- 2771 -- Freeze_Enclosing_Package_Body -- 2772 ----------------------------------- 2773 2774 procedure Freeze_Enclosing_Package_Body is 2775 Orig_Decl : constant Node_Id := Original_Node (Body_Decl); 2776 Par : Node_Id; 2777 2778 begin 2779 -- Climb the parent chain looking for an enclosing package body. Do 2780 -- not use the scope stack, because a body utilizes the entity of its 2781 -- corresponding spec. 2782 2783 Par := Parent (Body_Decl); 2784 while Present (Par) loop 2785 if Nkind (Par) = N_Package_Body then 2786 Analyze_Package_Body_Contract 2787 (Body_Id => Defining_Entity (Par), 2788 Freeze_Id => Defining_Entity (Body_Decl)); 2789 2790 exit; 2791 2792 -- Do not look for an enclosing package body when the construct 2793 -- which causes freezing is a body generated for an expression 2794 -- function and it appears within a package spec. This ensures 2795 -- that the traversal will not reach too far up the parent chain 2796 -- and attempt to freeze a package body which must not be frozen. 2797 2798 -- package body Enclosing_Body 2799 -- with Refined_State => (State => Var) 2800 -- is 2801 -- package Nested is 2802 -- type Some_Type is ...; 2803 -- function Cause_Freezing return ...; 2804 -- private 2805 -- function Cause_Freezing is (...); 2806 -- end Nested; 2807 -- 2808 -- Var : Nested.Some_Type; 2809 2810 elsif Nkind (Par) = N_Package_Declaration 2811 and then Nkind (Orig_Decl) = N_Expression_Function 2812 then 2813 exit; 2814 2815 -- Prevent the search from going too far 2816 2817 elsif Is_Body_Or_Package_Declaration (Par) then 2818 exit; 2819 end if; 2820 2821 Par := Parent (Par); 2822 end loop; 2823 end Freeze_Enclosing_Package_Body; 2824 2825 -- Local variables 2826 2827 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); 2828 2829 -- Start of processing for Freeze_Previous_Contracts 2830 2831 begin 2832 pragma Assert (Causes_Contract_Freezing (Body_Decl)); 2833 2834 -- A body that is in the process of being inlined appears from source, 2835 -- but carries name _parent. Such a body does not cause freezing of 2836 -- contracts. 2837 2838 if Chars (Body_Id) = Name_uParent then 2839 return; 2840 end if; 2841 2842 Freeze_Enclosing_Package_Body; 2843 Freeze_Contracts; 2844 end Freeze_Previous_Contracts; 2845 2846 --------------------------------- 2847 -- Inherit_Subprogram_Contract -- 2848 --------------------------------- 2849 2850 procedure Inherit_Subprogram_Contract 2851 (Subp : Entity_Id; 2852 From_Subp : Entity_Id) 2853 is 2854 procedure Inherit_Pragma (Prag_Id : Pragma_Id); 2855 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to 2856 -- Subp's contract. 2857 2858 -------------------- 2859 -- Inherit_Pragma -- 2860 -------------------- 2861 2862 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is 2863 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); 2864 New_Prag : Node_Id; 2865 2866 begin 2867 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma 2868 -- chains, therefore the node must be replicated. The new pragma is 2869 -- flagged as inherited for distinction purposes. 2870 2871 if Present (Prag) then 2872 New_Prag := New_Copy_Tree (Prag); 2873 Set_Is_Inherited_Pragma (New_Prag); 2874 2875 Add_Contract_Item (New_Prag, Subp); 2876 end if; 2877 end Inherit_Pragma; 2878 2879 -- Start of processing for Inherit_Subprogram_Contract 2880 2881 begin 2882 -- Inheritance is carried out only when both entities are subprograms 2883 -- with contracts. 2884 2885 if Is_Subprogram_Or_Generic_Subprogram (Subp) 2886 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) 2887 and then Present (Contract (From_Subp)) 2888 then 2889 Inherit_Pragma (Pragma_Extensions_Visible); 2890 end if; 2891 end Inherit_Subprogram_Contract; 2892 2893 ------------------------------------- 2894 -- Instantiate_Subprogram_Contract -- 2895 ------------------------------------- 2896 2897 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is 2898 procedure Instantiate_Pragmas (First_Prag : Node_Id); 2899 -- Instantiate all contract-related source pragmas found in the list, 2900 -- starting with pragma First_Prag. Each instantiated pragma is added 2901 -- to list L. 2902 2903 ------------------------- 2904 -- Instantiate_Pragmas -- 2905 ------------------------- 2906 2907 procedure Instantiate_Pragmas (First_Prag : Node_Id) is 2908 Inst_Prag : Node_Id; 2909 Prag : Node_Id; 2910 2911 begin 2912 Prag := First_Prag; 2913 while Present (Prag) loop 2914 if Is_Generic_Contract_Pragma (Prag) then 2915 Inst_Prag := 2916 Copy_Generic_Node (Prag, Empty, Instantiating => True); 2917 2918 Set_Analyzed (Inst_Prag, False); 2919 Append_To (L, Inst_Prag); 2920 end if; 2921 2922 Prag := Next_Pragma (Prag); 2923 end loop; 2924 end Instantiate_Pragmas; 2925 2926 -- Local variables 2927 2928 Items : constant Node_Id := Contract (Defining_Entity (Templ)); 2929 2930 -- Start of processing for Instantiate_Subprogram_Contract 2931 2932 begin 2933 if Present (Items) then 2934 Instantiate_Pragmas (Pre_Post_Conditions (Items)); 2935 Instantiate_Pragmas (Contract_Test_Cases (Items)); 2936 Instantiate_Pragmas (Classifications (Items)); 2937 end if; 2938 end Instantiate_Subprogram_Contract; 2939 2940 ---------------------------------------- 2941 -- Save_Global_References_In_Contract -- 2942 ---------------------------------------- 2943 2944 procedure Save_Global_References_In_Contract 2945 (Templ : Node_Id; 2946 Gen_Id : Entity_Id) 2947 is 2948 procedure Save_Global_References_In_List (First_Prag : Node_Id); 2949 -- Save all global references in contract-related source pragmas found 2950 -- in the list, starting with pragma First_Prag. 2951 2952 ------------------------------------ 2953 -- Save_Global_References_In_List -- 2954 ------------------------------------ 2955 2956 procedure Save_Global_References_In_List (First_Prag : Node_Id) is 2957 Prag : Node_Id; 2958 2959 begin 2960 Prag := First_Prag; 2961 while Present (Prag) loop 2962 if Is_Generic_Contract_Pragma (Prag) then 2963 Save_Global_References (Prag); 2964 end if; 2965 2966 Prag := Next_Pragma (Prag); 2967 end loop; 2968 end Save_Global_References_In_List; 2969 2970 -- Local variables 2971 2972 Items : constant Node_Id := Contract (Defining_Entity (Templ)); 2973 2974 -- Start of processing for Save_Global_References_In_Contract 2975 2976 begin 2977 -- The entity of the analyzed generic copy must be on the scope stack 2978 -- to ensure proper detection of global references. 2979 2980 Push_Scope (Gen_Id); 2981 2982 if Permits_Aspect_Specifications (Templ) 2983 and then Has_Aspects (Templ) 2984 then 2985 Save_Global_References_In_Aspects (Templ); 2986 end if; 2987 2988 if Present (Items) then 2989 Save_Global_References_In_List (Pre_Post_Conditions (Items)); 2990 Save_Global_References_In_List (Contract_Test_Cases (Items)); 2991 Save_Global_References_In_List (Classifications (Items)); 2992 end if; 2993 2994 Pop_Scope; 2995 end Save_Global_References_In_Contract; 2996 2997end Contracts; 2998