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