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