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