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-2021, 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 Einfo.Entities; use Einfo.Entities; 30with Einfo.Utils; use Einfo.Utils; 31with Elists; use Elists; 32with Errout; use Errout; 33with Exp_Prag; use Exp_Prag; 34with Exp_Tss; use Exp_Tss; 35with Exp_Util; use Exp_Util; 36with Freeze; use Freeze; 37with Lib; use Lib; 38with Namet; use Namet; 39with Nlists; use Nlists; 40with Nmake; use Nmake; 41with Opt; use Opt; 42with Sem; use Sem; 43with Sem_Aux; use Sem_Aux; 44with Sem_Ch6; use Sem_Ch6; 45with Sem_Ch8; use Sem_Ch8; 46with Sem_Ch12; use Sem_Ch12; 47with Sem_Ch13; use Sem_Ch13; 48with Sem_Disp; use Sem_Disp; 49with Sem_Prag; use Sem_Prag; 50with Sem_Res; use Sem_Res; 51with Sem_Type; use Sem_Type; 52with Sem_Util; use Sem_Util; 53with Sinfo; use Sinfo; 54with Sinfo.Nodes; use Sinfo.Nodes; 55with Sinfo.Utils; use Sinfo.Utils; 56with Sinput; use Sinput; 57with Snames; use Snames; 58with Stand; use Stand; 59with Stringt; use Stringt; 60with Tbuild; use Tbuild; 61 62package body Contracts is 63 64 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id); 65 -- Analyze all delayed pragmas chained on the contract of package 66 -- instantiation Inst_Id as if they appear at the end of a declarative 67 -- region. The pragmas in question are: 68 -- 69 -- Part_Of 70 71 procedure Check_Class_Condition 72 (Cond : Node_Id; 73 Subp : Entity_Id; 74 Par_Subp : Entity_Id; 75 Is_Precondition : Boolean); 76 -- Perform checking of class-wide pre/postcondition Cond inherited by Subp 77 -- from Par_Subp. Is_Precondition enables check specific for preconditions. 78 -- In SPARK_Mode, an inherited operation that is not overridden but has 79 -- inherited modified conditions pre/postconditions is illegal. 80 81 procedure Check_Type_Or_Object_External_Properties 82 (Type_Or_Obj_Id : Entity_Id); 83 -- Perform checking of external properties pragmas that is common to both 84 -- type declarations and object declarations. 85 86 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); 87 -- Expand the contracts of a subprogram body and its correspoding spec (if 88 -- any). This routine processes all [refined] pre- and postconditions as 89 -- well as Contract_Cases, Subprogram_Variant, invariants and predicates. 90 -- Body_Id denotes the entity of the subprogram body. 91 92 procedure Set_Class_Condition 93 (Kind : Condition_Kind; 94 Subp : Entity_Id; 95 Cond : Node_Id); 96 -- Set the class-wide Kind condition of Subp 97 98 ----------------------- 99 -- Add_Contract_Item -- 100 ----------------------- 101 102 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is 103 Items : Node_Id := Contract (Id); 104 105 procedure Add_Classification; 106 -- Prepend Prag to the list of classifications 107 108 procedure Add_Contract_Test_Case; 109 -- Prepend Prag to the list of contract and test cases 110 111 procedure Add_Pre_Post_Condition; 112 -- Prepend Prag to the list of pre- and postconditions 113 114 ------------------------ 115 -- Add_Classification -- 116 ------------------------ 117 118 procedure Add_Classification is 119 begin 120 Set_Next_Pragma (Prag, Classifications (Items)); 121 Set_Classifications (Items, Prag); 122 end Add_Classification; 123 124 ---------------------------- 125 -- Add_Contract_Test_Case -- 126 ---------------------------- 127 128 procedure Add_Contract_Test_Case is 129 begin 130 Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); 131 Set_Contract_Test_Cases (Items, Prag); 132 end Add_Contract_Test_Case; 133 134 ---------------------------- 135 -- Add_Pre_Post_Condition -- 136 ---------------------------- 137 138 procedure Add_Pre_Post_Condition is 139 begin 140 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); 141 Set_Pre_Post_Conditions (Items, Prag); 142 end Add_Pre_Post_Condition; 143 144 -- Local variables 145 146 -- A contract must contain only pragmas 147 148 pragma Assert (Nkind (Prag) = N_Pragma); 149 Prag_Nam : constant Name_Id := Pragma_Name (Prag); 150 151 -- Start of processing for Add_Contract_Item 152 153 begin 154 -- Create a new contract when adding the first item 155 156 if No (Items) then 157 Items := Make_Contract (Sloc (Id)); 158 Set_Contract (Id, Items); 159 end if; 160 161 -- Constants, the applicable pragmas are: 162 -- Part_Of 163 164 if Ekind (Id) = E_Constant then 165 if Prag_Nam in Name_Async_Readers 166 | Name_Async_Writers 167 | Name_Effective_Reads 168 | Name_Effective_Writes 169 | Name_No_Caching 170 | Name_Part_Of 171 then 172 Add_Classification; 173 174 -- The pragma is not a proper contract item 175 176 else 177 raise Program_Error; 178 end if; 179 180 -- Entry bodies, the applicable pragmas are: 181 -- Refined_Depends 182 -- Refined_Global 183 -- Refined_Post 184 185 elsif Is_Entry_Body (Id) then 186 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then 187 Add_Classification; 188 189 elsif Prag_Nam = Name_Refined_Post then 190 Add_Pre_Post_Condition; 191 192 -- The pragma is not a proper contract item 193 194 else 195 raise Program_Error; 196 end if; 197 198 -- Entry or subprogram declarations, the applicable pragmas are: 199 -- Attach_Handler 200 -- Contract_Cases 201 -- Depends 202 -- Extensions_Visible 203 -- Global 204 -- Interrupt_Handler 205 -- Postcondition 206 -- Precondition 207 -- Test_Case 208 -- Volatile_Function 209 210 elsif Is_Entry_Declaration (Id) 211 or else Ekind (Id) in E_Function 212 | E_Generic_Function 213 | E_Generic_Procedure 214 | E_Procedure 215 then 216 if Prag_Nam in Name_Attach_Handler | Name_Interrupt_Handler 217 and then Ekind (Id) in E_Generic_Procedure | E_Procedure 218 then 219 Add_Classification; 220 221 elsif Prag_Nam in Name_Depends 222 | Name_Extensions_Visible 223 | Name_Global 224 then 225 Add_Classification; 226 227 elsif Prag_Nam = Name_Volatile_Function 228 and then Ekind (Id) in E_Function | E_Generic_Function 229 then 230 Add_Classification; 231 232 elsif Prag_Nam in Name_Contract_Cases 233 | Name_Subprogram_Variant 234 | Name_Test_Case 235 then 236 Add_Contract_Test_Case; 237 238 elsif Prag_Nam in Name_Postcondition | Name_Precondition then 239 Add_Pre_Post_Condition; 240 241 -- The pragma is not a proper contract item 242 243 else 244 raise Program_Error; 245 end if; 246 247 -- Packages or instantiations, the applicable pragmas are: 248 -- Abstract_States 249 -- Initial_Condition 250 -- Initializes 251 -- Part_Of (instantiation only) 252 253 elsif Is_Package_Or_Generic_Package (Id) then 254 if Prag_Nam in Name_Abstract_State 255 | Name_Initial_Condition 256 | Name_Initializes 257 then 258 Add_Classification; 259 260 -- Indicator Part_Of must be associated with a package instantiation 261 262 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then 263 Add_Classification; 264 265 -- The pragma is not a proper contract item 266 267 else 268 raise Program_Error; 269 end if; 270 271 -- Package bodies, the applicable pragmas are: 272 -- Refined_States 273 274 elsif Ekind (Id) = E_Package_Body then 275 if Prag_Nam = Name_Refined_State then 276 Add_Classification; 277 278 -- The pragma is not a proper contract item 279 280 else 281 raise Program_Error; 282 end if; 283 284 -- The four volatility refinement pragmas are ok for all types. 285 -- Part_Of is ok for task types and protected types. 286 -- Depends and Global are ok for task types. 287 288 elsif Is_Type (Id) then 289 declare 290 Is_OK : constant Boolean := 291 Prag_Nam in Name_Async_Readers 292 | Name_Async_Writers 293 | Name_Effective_Reads 294 | Name_Effective_Writes 295 or else (Ekind (Id) = E_Task_Type 296 and Prag_Nam in Name_Part_Of 297 | Name_Depends 298 | Name_Global) 299 or else (Ekind (Id) = E_Protected_Type 300 and Prag_Nam = Name_Part_Of); 301 begin 302 if Is_OK then 303 Add_Classification; 304 else 305 306 -- The pragma is not a proper contract item 307 308 raise Program_Error; 309 end if; 310 end; 311 312 -- Subprogram bodies, the applicable pragmas are: 313 -- Postcondition 314 -- Precondition 315 -- Refined_Depends 316 -- Refined_Global 317 -- Refined_Post 318 319 elsif Ekind (Id) = E_Subprogram_Body then 320 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then 321 Add_Classification; 322 323 elsif Prag_Nam in Name_Postcondition 324 | Name_Precondition 325 | Name_Refined_Post 326 then 327 Add_Pre_Post_Condition; 328 329 -- The pragma is not a proper contract item 330 331 else 332 raise Program_Error; 333 end if; 334 335 -- Task bodies, the applicable pragmas are: 336 -- Refined_Depends 337 -- Refined_Global 338 339 elsif Ekind (Id) = E_Task_Body then 340 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then 341 Add_Classification; 342 343 -- The pragma is not a proper contract item 344 345 else 346 raise Program_Error; 347 end if; 348 349 -- Task units, the applicable pragmas are: 350 -- Depends 351 -- Global 352 -- Part_Of 353 354 -- Variables, the applicable pragmas are: 355 -- Async_Readers 356 -- Async_Writers 357 -- Constant_After_Elaboration 358 -- Depends 359 -- Effective_Reads 360 -- Effective_Writes 361 -- Global 362 -- No_Caching 363 -- Part_Of 364 365 elsif Ekind (Id) = E_Variable then 366 if Prag_Nam in Name_Async_Readers 367 | Name_Async_Writers 368 | Name_Constant_After_Elaboration 369 | Name_Depends 370 | Name_Effective_Reads 371 | Name_Effective_Writes 372 | Name_Global 373 | Name_No_Caching 374 | Name_Part_Of 375 then 376 Add_Classification; 377 378 -- The pragma is not a proper contract item 379 380 else 381 raise Program_Error; 382 end if; 383 384 else 385 raise Program_Error; 386 end if; 387 end Add_Contract_Item; 388 389 ----------------------- 390 -- Analyze_Contracts -- 391 ----------------------- 392 393 procedure Analyze_Contracts (L : List_Id) is 394 Decl : Node_Id; 395 396 begin 397 Decl := First (L); 398 while Present (Decl) loop 399 400 -- Entry or subprogram declarations 401 402 if Nkind (Decl) in N_Abstract_Subprogram_Declaration 403 | N_Entry_Declaration 404 | N_Generic_Subprogram_Declaration 405 | N_Subprogram_Declaration 406 then 407 Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl)); 408 409 -- Entry or subprogram bodies 410 411 elsif Nkind (Decl) in N_Entry_Body | N_Subprogram_Body then 412 Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl)); 413 414 -- Objects 415 416 elsif Nkind (Decl) = N_Object_Declaration then 417 Analyze_Object_Contract (Defining_Entity (Decl)); 418 419 -- Package instantiation 420 421 elsif Nkind (Decl) = N_Package_Instantiation then 422 Analyze_Package_Instantiation_Contract (Defining_Entity (Decl)); 423 424 -- Protected units 425 426 elsif Nkind (Decl) in N_Protected_Type_Declaration 427 | N_Single_Protected_Declaration 428 then 429 Analyze_Protected_Contract (Defining_Entity (Decl)); 430 431 -- Subprogram body stubs 432 433 elsif Nkind (Decl) = N_Subprogram_Body_Stub then 434 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); 435 436 -- Task units 437 438 elsif Nkind (Decl) in N_Single_Task_Declaration 439 | N_Task_Type_Declaration 440 then 441 Analyze_Task_Contract (Defining_Entity (Decl)); 442 443 -- For type declarations, we need to do the preanalysis of Iterable 444 -- and the 3 Xxx_Literal aspect specifications. 445 446 -- Other type aspects need to be resolved here??? 447 448 elsif Nkind (Decl) = N_Private_Type_Declaration 449 and then Present (Aspect_Specifications (Decl)) 450 then 451 declare 452 E : constant Entity_Id := Defining_Identifier (Decl); 453 It : constant Node_Id := Find_Aspect (E, Aspect_Iterable); 454 I_Lit : constant Node_Id := 455 Find_Aspect (E, Aspect_Integer_Literal); 456 R_Lit : constant Node_Id := 457 Find_Aspect (E, Aspect_Real_Literal); 458 S_Lit : constant Node_Id := 459 Find_Aspect (E, Aspect_String_Literal); 460 461 begin 462 if Present (It) then 463 Validate_Iterable_Aspect (E, It); 464 end if; 465 466 if Present (I_Lit) then 467 Validate_Literal_Aspect (E, I_Lit); 468 end if; 469 if Present (R_Lit) then 470 Validate_Literal_Aspect (E, R_Lit); 471 end if; 472 if Present (S_Lit) then 473 Validate_Literal_Aspect (E, S_Lit); 474 end if; 475 end; 476 end if; 477 478 if Nkind (Decl) in N_Full_Type_Declaration 479 | N_Private_Type_Declaration 480 | N_Task_Type_Declaration 481 | N_Protected_Type_Declaration 482 | N_Formal_Type_Declaration 483 then 484 Analyze_Type_Contract (Defining_Identifier (Decl)); 485 end if; 486 487 Next (Decl); 488 end loop; 489 end Analyze_Contracts; 490 491 ----------------------------------------------- 492 -- Analyze_Entry_Or_Subprogram_Body_Contract -- 493 ----------------------------------------------- 494 495 -- WARNING: This routine manages SPARK regions. Return statements must be 496 -- replaced by gotos which jump to the end of the routine and restore the 497 -- SPARK mode. 498 499 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is 500 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 501 Items : constant Node_Id := Contract (Body_Id); 502 Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); 503 504 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 505 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 506 -- Save the SPARK_Mode-related data to restore on exit 507 508 begin 509 -- When a subprogram body declaration is illegal, its defining entity is 510 -- left unanalyzed. There is nothing left to do in this case because the 511 -- body lacks a contract, or even a proper Ekind. 512 513 if Ekind (Body_Id) = E_Void then 514 return; 515 516 -- Do not analyze a contract multiple times 517 518 elsif Present (Items) then 519 if Analyzed (Items) then 520 return; 521 else 522 Set_Analyzed (Items); 523 end if; 524 end if; 525 526 -- Due to the timing of contract analysis, delayed pragmas may be 527 -- subject to the wrong SPARK_Mode, usually that of the enclosing 528 -- context. To remedy this, restore the original SPARK_Mode of the 529 -- related subprogram body. 530 531 Set_SPARK_Mode (Body_Id); 532 533 -- Ensure that the contract cases or postconditions mention 'Result or 534 -- define a post-state. 535 536 Check_Result_And_Post_State (Body_Id); 537 538 -- A stand-alone nonvolatile function body cannot have an effectively 539 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This 540 -- check is relevant only when SPARK_Mode is on, as it is not a standard 541 -- legality rule. The check is performed here because Volatile_Function 542 -- is processed after the analysis of the related subprogram body. The 543 -- check only applies to source subprograms and not to generated TSS 544 -- subprograms. 545 546 if SPARK_Mode = On 547 and then Ekind (Body_Id) in E_Function | E_Generic_Function 548 and then Comes_From_Source (Spec_Id) 549 and then not Is_Volatile_Function (Body_Id) 550 then 551 Check_Nonvolatile_Function_Profile (Body_Id); 552 end if; 553 554 -- Restore the SPARK_Mode of the enclosing context after all delayed 555 -- pragmas have been analyzed. 556 557 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 558 559 -- Capture all global references in a generic subprogram body now that 560 -- the contract has been analyzed. 561 562 if Is_Generic_Declaration_Or_Body (Body_Decl) then 563 Save_Global_References_In_Contract 564 (Templ => Original_Node (Body_Decl), 565 Gen_Id => Spec_Id); 566 end if; 567 568 -- Deal with preconditions, [refined] postconditions, Contract_Cases, 569 -- Subprogram_Variant, invariants and predicates associated with body 570 -- and its spec. Do not expand the contract of subprogram body stubs. 571 572 if Nkind (Body_Decl) = N_Subprogram_Body then 573 Expand_Subprogram_Contract (Body_Id); 574 end if; 575 end Analyze_Entry_Or_Subprogram_Body_Contract; 576 577 ------------------------------------------ 578 -- Analyze_Entry_Or_Subprogram_Contract -- 579 ------------------------------------------ 580 581 -- WARNING: This routine manages SPARK regions. Return statements must be 582 -- replaced by gotos which jump to the end of the routine and restore the 583 -- SPARK mode. 584 585 procedure Analyze_Entry_Or_Subprogram_Contract 586 (Subp_Id : Entity_Id; 587 Freeze_Id : Entity_Id := Empty) 588 is 589 Items : constant Node_Id := Contract (Subp_Id); 590 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 591 592 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 593 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 594 -- Save the SPARK_Mode-related data to restore on exit 595 596 Skip_Assert_Exprs : constant Boolean := 597 Is_Entry (Subp_Id) and then not GNATprove_Mode; 598 599 Depends : Node_Id := Empty; 600 Global : Node_Id := Empty; 601 Prag : Node_Id; 602 Prag_Nam : Name_Id; 603 604 begin 605 -- Do not analyze a contract multiple times 606 607 if Present (Items) then 608 if Analyzed (Items) then 609 return; 610 else 611 Set_Analyzed (Items); 612 end if; 613 end if; 614 615 -- Due to the timing of contract analysis, delayed pragmas may be 616 -- subject to the wrong SPARK_Mode, usually that of the enclosing 617 -- context. To remedy this, restore the original SPARK_Mode of the 618 -- related subprogram body. 619 620 Set_SPARK_Mode (Subp_Id); 621 622 -- All subprograms carry a contract, but for some it is not significant 623 -- and should not be processed. 624 625 if not Has_Significant_Contract (Subp_Id) then 626 null; 627 628 elsif Present (Items) then 629 630 -- Do not analyze the pre/postconditions of an entry declaration 631 -- unless annotating the original tree for GNATprove. The 632 -- real analysis occurs when the pre/postconditons are relocated to 633 -- the contract wrapper procedure (see Build_Contract_Wrapper). 634 635 if Skip_Assert_Exprs then 636 null; 637 638 -- Otherwise analyze the pre/postconditions. 639 -- If these come from an aspect specification, their expressions 640 -- might include references to types that are not frozen yet, in the 641 -- case where the body is a rewritten expression function that is a 642 -- completion, so freeze all types within before constructing the 643 -- contract code. 644 645 else 646 declare 647 Bod : Node_Id; 648 Freeze_Types : Boolean := False; 649 650 begin 651 if Present (Freeze_Id) then 652 Bod := Unit_Declaration_Node (Freeze_Id); 653 654 if Nkind (Bod) = N_Subprogram_Body 655 and then Was_Expression_Function (Bod) 656 and then Ekind (Subp_Id) = E_Function 657 and then Chars (Subp_Id) = Chars (Freeze_Id) 658 and then Subp_Id /= Freeze_Id 659 then 660 Freeze_Types := True; 661 end if; 662 end if; 663 664 Prag := Pre_Post_Conditions (Items); 665 while Present (Prag) loop 666 if Freeze_Types 667 and then Present (Corresponding_Aspect (Prag)) 668 then 669 Freeze_Expr_Types 670 (Def_Id => Subp_Id, 671 Typ => Standard_Boolean, 672 Expr => 673 Expression 674 (First (Pragma_Argument_Associations (Prag))), 675 N => Bod); 676 end if; 677 678 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id); 679 Prag := Next_Pragma (Prag); 680 end loop; 681 end; 682 end if; 683 684 -- Analyze contract-cases, subprogram-variant and test-cases 685 686 Prag := Contract_Test_Cases (Items); 687 while Present (Prag) loop 688 Prag_Nam := Pragma_Name (Prag); 689 690 if Prag_Nam = Name_Contract_Cases then 691 692 -- Do not analyze the contract cases of an entry declaration 693 -- unless annotating the original tree for GNATprove. 694 -- The real analysis occurs when the contract cases are moved 695 -- to the contract wrapper procedure (Build_Contract_Wrapper). 696 697 if Skip_Assert_Exprs then 698 null; 699 700 -- Otherwise analyze the contract cases 701 702 else 703 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id); 704 end if; 705 706 elsif Prag_Nam = Name_Subprogram_Variant then 707 Analyze_Subprogram_Variant_In_Decl_Part (Prag); 708 709 else 710 pragma Assert (Prag_Nam = Name_Test_Case); 711 Analyze_Test_Case_In_Decl_Part (Prag); 712 end if; 713 714 Prag := Next_Pragma (Prag); 715 end loop; 716 717 -- Analyze classification pragmas 718 719 Prag := Classifications (Items); 720 while Present (Prag) loop 721 Prag_Nam := Pragma_Name (Prag); 722 723 if Prag_Nam = Name_Depends then 724 Depends := Prag; 725 726 elsif Prag_Nam = Name_Global then 727 Global := Prag; 728 end if; 729 730 Prag := Next_Pragma (Prag); 731 end loop; 732 733 -- Analyze Global first, as Depends may mention items classified in 734 -- the global categorization. 735 736 if Present (Global) then 737 Analyze_Global_In_Decl_Part (Global); 738 end if; 739 740 -- Depends must be analyzed after Global in order to see the modes of 741 -- all global items. 742 743 if Present (Depends) then 744 Analyze_Depends_In_Decl_Part (Depends); 745 end if; 746 747 -- Ensure that the contract cases or postconditions mention 'Result 748 -- or define a post-state. 749 750 Check_Result_And_Post_State (Subp_Id); 751 end if; 752 753 -- A nonvolatile function cannot have an effectively volatile formal 754 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant 755 -- only when SPARK_Mode is on, as it is not a standard legality rule. 756 -- The check is performed here because pragma Volatile_Function is 757 -- processed after the analysis of the related subprogram declaration. 758 759 if SPARK_Mode = On 760 and then Ekind (Subp_Id) in E_Function | E_Generic_Function 761 and then Comes_From_Source (Subp_Id) 762 and then not Is_Volatile_Function (Subp_Id) 763 then 764 Check_Nonvolatile_Function_Profile (Subp_Id); 765 end if; 766 767 -- Restore the SPARK_Mode of the enclosing context after all delayed 768 -- pragmas have been analyzed. 769 770 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 771 772 -- Capture all global references in a generic subprogram now that the 773 -- contract has been analyzed. 774 775 if Is_Generic_Declaration_Or_Body (Subp_Decl) then 776 Save_Global_References_In_Contract 777 (Templ => Original_Node (Subp_Decl), 778 Gen_Id => Subp_Id); 779 end if; 780 end Analyze_Entry_Or_Subprogram_Contract; 781 782 ---------------------------------------------- 783 -- Check_Type_Or_Object_External_Properties -- 784 ---------------------------------------------- 785 786 procedure Check_Type_Or_Object_External_Properties 787 (Type_Or_Obj_Id : Entity_Id) 788 is 789 Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id); 790 Decl_Kind : constant String := 791 (if Is_Type_Id then "type" else "object"); 792 793 -- Local variables 794 795 AR_Val : Boolean := False; 796 AW_Val : Boolean := False; 797 ER_Val : Boolean := False; 798 EW_Val : Boolean := False; 799 Seen : Boolean := False; 800 Prag : Node_Id; 801 Obj_Typ : Entity_Id; 802 803 -- Start of processing for Check_Type_Or_Object_External_Properties 804 805 begin 806 -- Analyze all external properties 807 808 if Is_Type_Id then 809 Obj_Typ := Type_Or_Obj_Id; 810 811 -- If the parent type of a derived type is volatile 812 -- then the derived type inherits volatility-related flags. 813 814 if Is_Derived_Type (Type_Or_Obj_Id) then 815 declare 816 Parent_Type : constant Entity_Id := 817 Etype (Base_Type (Type_Or_Obj_Id)); 818 begin 819 if Is_Effectively_Volatile (Parent_Type) then 820 AR_Val := Async_Readers_Enabled (Parent_Type); 821 AW_Val := Async_Writers_Enabled (Parent_Type); 822 ER_Val := Effective_Reads_Enabled (Parent_Type); 823 EW_Val := Effective_Writes_Enabled (Parent_Type); 824 end if; 825 end; 826 end if; 827 else 828 Obj_Typ := Etype (Type_Or_Obj_Id); 829 end if; 830 831 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers); 832 833 if Present (Prag) then 834 declare 835 Saved_AR_Val : constant Boolean := AR_Val; 836 begin 837 Analyze_External_Property_In_Decl_Part (Prag, AR_Val); 838 Seen := True; 839 if Saved_AR_Val and not AR_Val then 840 Error_Msg_N 841 ("illegal non-confirming Async_Readers specification", 842 Prag); 843 end if; 844 end; 845 end if; 846 847 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers); 848 849 if Present (Prag) then 850 declare 851 Saved_AW_Val : constant Boolean := AW_Val; 852 begin 853 Analyze_External_Property_In_Decl_Part (Prag, AW_Val); 854 Seen := True; 855 if Saved_AW_Val and not AW_Val then 856 Error_Msg_N 857 ("illegal non-confirming Async_Writers specification", 858 Prag); 859 end if; 860 end; 861 end if; 862 863 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads); 864 865 if Present (Prag) then 866 declare 867 Saved_ER_Val : constant Boolean := ER_Val; 868 begin 869 Analyze_External_Property_In_Decl_Part (Prag, ER_Val); 870 Seen := True; 871 if Saved_ER_Val and not ER_Val then 872 Error_Msg_N 873 ("illegal non-confirming Effective_Reads specification", 874 Prag); 875 end if; 876 end; 877 end if; 878 879 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes); 880 881 if Present (Prag) then 882 declare 883 Saved_EW_Val : constant Boolean := EW_Val; 884 begin 885 Analyze_External_Property_In_Decl_Part (Prag, EW_Val); 886 Seen := True; 887 if Saved_EW_Val and not EW_Val then 888 Error_Msg_N 889 ("illegal non-confirming Effective_Writes specification", 890 Prag); 891 end if; 892 end; 893 end if; 894 895 -- Verify the mutual interaction of the various external properties 896 897 if Seen then 898 Check_External_Properties 899 (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); 900 end if; 901 902 -- The following checks are relevant only when SPARK_Mode is on, as 903 -- they are not standard Ada legality rules. Internally generated 904 -- temporaries are ignored, as well as return objects. 905 906 if SPARK_Mode = On 907 and then Comes_From_Source (Type_Or_Obj_Id) 908 and then not Is_Return_Object (Type_Or_Obj_Id) 909 then 910 if Is_Effectively_Volatile (Type_Or_Obj_Id) then 911 912 -- The declaration of an effectively volatile object or type must 913 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). 914 915 if not Is_Library_Level_Entity (Type_Or_Obj_Id) then 916 Error_Msg_N 917 ("effectively volatile " 918 & Decl_Kind 919 & " & must be declared at library level " 920 & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id); 921 922 -- An object of a discriminated type cannot be effectively 923 -- volatile except for protected objects (SPARK RM 7.1.3(5)). 924 925 elsif Has_Discriminants (Obj_Typ) 926 and then not Is_Protected_Type (Obj_Typ) 927 then 928 Error_Msg_N 929 ("discriminated " & Decl_Kind & " & cannot be volatile", 930 Type_Or_Obj_Id); 931 end if; 932 933 -- An object decl shall be compatible with respect to volatility 934 -- with its type (SPARK RM 7.1.3(2)). 935 936 if not Is_Type_Id then 937 if Is_Effectively_Volatile (Obj_Typ) then 938 Check_Volatility_Compatibility 939 (Type_Or_Obj_Id, Obj_Typ, 940 "volatile object", "its type", 941 Srcpos_Bearer => Type_Or_Obj_Id); 942 end if; 943 944 -- A component of a composite type (in this case, the composite 945 -- type is an array type) shall be compatible with respect to 946 -- volatility with the composite type (SPARK RM 7.1.3(6)). 947 948 elsif Is_Array_Type (Obj_Typ) then 949 Check_Volatility_Compatibility 950 (Component_Type (Obj_Typ), Obj_Typ, 951 "component type", "its enclosing array type", 952 Srcpos_Bearer => Obj_Typ); 953 954 -- A component of a composite type (in this case, the composite 955 -- type is a record type) shall be compatible with respect to 956 -- volatility with the composite type (SPARK RM 7.1.3(6)). 957 958 elsif Is_Record_Type (Obj_Typ) then 959 declare 960 Comp : Entity_Id := First_Component (Obj_Typ); 961 begin 962 while Present (Comp) loop 963 Check_Volatility_Compatibility 964 (Etype (Comp), Obj_Typ, 965 "record component " & Get_Name_String (Chars (Comp)), 966 "its enclosing record type", 967 Srcpos_Bearer => Comp); 968 Next_Component (Comp); 969 end loop; 970 end; 971 end if; 972 973 -- The type or object is not effectively volatile 974 975 else 976 -- A non-effectively volatile type cannot have effectively 977 -- volatile components (SPARK RM 7.1.3(6)). 978 979 if Is_Type_Id 980 and then not Is_Effectively_Volatile (Type_Or_Obj_Id) 981 and then Has_Volatile_Component (Type_Or_Obj_Id) 982 then 983 Error_Msg_N 984 ("non-volatile type & cannot have volatile" 985 & " components", 986 Type_Or_Obj_Id); 987 end if; 988 end if; 989 end if; 990 end Check_Type_Or_Object_External_Properties; 991 992 ----------------------------- 993 -- Analyze_Object_Contract -- 994 ----------------------------- 995 996 -- WARNING: This routine manages SPARK regions. Return statements must be 997 -- replaced by gotos which jump to the end of the routine and restore the 998 -- SPARK mode. 999 1000 procedure Analyze_Object_Contract 1001 (Obj_Id : Entity_Id; 1002 Freeze_Id : Entity_Id := Empty) 1003 is 1004 Obj_Typ : constant Entity_Id := Etype (Obj_Id); 1005 1006 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1007 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1008 -- Save the SPARK_Mode-related data to restore on exit 1009 1010 NC_Val : Boolean; 1011 Items : Node_Id; 1012 Prag : Node_Id; 1013 Ref_Elmt : Elmt_Id; 1014 1015 begin 1016 -- The loop parameter in an element iterator over a formal container 1017 -- is declared with an object declaration, but no contracts apply. 1018 1019 if Ekind (Obj_Id) = E_Loop_Parameter then 1020 return; 1021 end if; 1022 1023 -- Do not analyze a contract multiple times 1024 1025 Items := Contract (Obj_Id); 1026 1027 if Present (Items) then 1028 if Analyzed (Items) then 1029 return; 1030 else 1031 Set_Analyzed (Items); 1032 end if; 1033 end if; 1034 1035 -- The anonymous object created for a single concurrent type inherits 1036 -- the SPARK_Mode from the type. Due to the timing of contract analysis, 1037 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that 1038 -- of the enclosing context. To remedy this, restore the original mode 1039 -- of the related anonymous object. 1040 1041 if Is_Single_Concurrent_Object (Obj_Id) 1042 and then Present (SPARK_Pragma (Obj_Id)) 1043 then 1044 Set_SPARK_Mode (Obj_Id); 1045 end if; 1046 1047 -- Checks related to external properties, same for constants and 1048 -- variables. 1049 1050 Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id); 1051 1052 -- Analyze the non-external volatility property No_Caching 1053 1054 Prag := Get_Pragma (Obj_Id, Pragma_No_Caching); 1055 1056 if Present (Prag) then 1057 Analyze_External_Property_In_Decl_Part (Prag, NC_Val); 1058 end if; 1059 1060 -- Constant-related checks 1061 1062 if Ekind (Obj_Id) = E_Constant then 1063 1064 -- Analyze indicator Part_Of 1065 1066 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); 1067 1068 -- Check whether the lack of indicator Part_Of agrees with the 1069 -- placement of the constant with respect to the state space. 1070 1071 if No (Prag) then 1072 Check_Missing_Part_Of (Obj_Id); 1073 end if; 1074 1075 -- Variable-related checks 1076 1077 else pragma Assert (Ekind (Obj_Id) = E_Variable); 1078 1079 -- The anonymous object created for a single task type carries 1080 -- pragmas Depends and Global of the type. 1081 1082 if Is_Single_Task_Object (Obj_Id) then 1083 1084 -- Analyze Global first, as Depends may mention items classified 1085 -- in the global categorization. 1086 1087 Prag := Get_Pragma (Obj_Id, Pragma_Global); 1088 1089 if Present (Prag) then 1090 Analyze_Global_In_Decl_Part (Prag); 1091 end if; 1092 1093 -- Depends must be analyzed after Global in order to see the modes 1094 -- of all global items. 1095 1096 Prag := Get_Pragma (Obj_Id, Pragma_Depends); 1097 1098 if Present (Prag) then 1099 Analyze_Depends_In_Decl_Part (Prag); 1100 end if; 1101 end if; 1102 1103 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); 1104 1105 -- Analyze indicator Part_Of 1106 1107 if Present (Prag) then 1108 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id); 1109 1110 -- The variable is a constituent of a single protected/task type 1111 -- and behaves as a component of the type. Verify that references 1112 -- to the variable occur within the definition or body of the type 1113 -- (SPARK RM 9.3). 1114 1115 if Present (Encapsulating_State (Obj_Id)) 1116 and then Is_Single_Concurrent_Object 1117 (Encapsulating_State (Obj_Id)) 1118 and then Present (Part_Of_References (Obj_Id)) 1119 then 1120 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id)); 1121 while Present (Ref_Elmt) loop 1122 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt)); 1123 Next_Elmt (Ref_Elmt); 1124 end loop; 1125 end if; 1126 1127 -- Otherwise check whether the lack of indicator Part_Of agrees with 1128 -- the placement of the variable with respect to the state space. 1129 1130 else 1131 Check_Missing_Part_Of (Obj_Id); 1132 end if; 1133 end if; 1134 1135 -- Common checks 1136 1137 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then 1138 1139 -- A Ghost object cannot be of a type that yields a synchronized 1140 -- object (SPARK RM 6.9(19)). 1141 1142 if Yields_Synchronized_Object (Obj_Typ) then 1143 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); 1144 1145 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and 1146 -- SPARK RM 6.9(19)). 1147 1148 elsif Is_Effectively_Volatile (Obj_Id) then 1149 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); 1150 1151 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). 1152 -- One exception to this is the object that represents the dispatch 1153 -- table of a Ghost tagged type, as the symbol needs to be exported. 1154 1155 elsif Is_Exported (Obj_Id) then 1156 Error_Msg_N ("ghost object & cannot be exported", Obj_Id); 1157 1158 elsif Is_Imported (Obj_Id) then 1159 Error_Msg_N ("ghost object & cannot be imported", Obj_Id); 1160 end if; 1161 end if; 1162 1163 -- Restore the SPARK_Mode of the enclosing context after all delayed 1164 -- pragmas have been analyzed. 1165 1166 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1167 end Analyze_Object_Contract; 1168 1169 ----------------------------------- 1170 -- Analyze_Package_Body_Contract -- 1171 ----------------------------------- 1172 1173 -- WARNING: This routine manages SPARK regions. Return statements must be 1174 -- replaced by gotos which jump to the end of the routine and restore the 1175 -- SPARK mode. 1176 1177 procedure Analyze_Package_Body_Contract 1178 (Body_Id : Entity_Id; 1179 Freeze_Id : Entity_Id := Empty) 1180 is 1181 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 1182 Items : constant Node_Id := Contract (Body_Id); 1183 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); 1184 1185 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1186 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1187 -- Save the SPARK_Mode-related data to restore on exit 1188 1189 Ref_State : Node_Id; 1190 1191 begin 1192 -- Do not analyze a contract multiple times 1193 1194 if Present (Items) then 1195 if Analyzed (Items) then 1196 return; 1197 else 1198 Set_Analyzed (Items); 1199 end if; 1200 end if; 1201 1202 -- Due to the timing of contract analysis, delayed pragmas may be 1203 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1204 -- context. To remedy this, restore the original SPARK_Mode of the 1205 -- related package body. 1206 1207 Set_SPARK_Mode (Body_Id); 1208 1209 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); 1210 1211 -- The analysis of pragma Refined_State detects whether the spec has 1212 -- abstract states available for refinement. 1213 1214 if Present (Ref_State) then 1215 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); 1216 end if; 1217 1218 -- Restore the SPARK_Mode of the enclosing context after all delayed 1219 -- pragmas have been analyzed. 1220 1221 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1222 1223 -- Capture all global references in a generic package body now that the 1224 -- contract has been analyzed. 1225 1226 if Is_Generic_Declaration_Or_Body (Body_Decl) then 1227 Save_Global_References_In_Contract 1228 (Templ => Original_Node (Body_Decl), 1229 Gen_Id => Spec_Id); 1230 end if; 1231 end Analyze_Package_Body_Contract; 1232 1233 ------------------------------ 1234 -- Analyze_Package_Contract -- 1235 ------------------------------ 1236 1237 -- WARNING: This routine manages SPARK regions. Return statements must be 1238 -- replaced by gotos which jump to the end of the routine and restore the 1239 -- SPARK mode. 1240 1241 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is 1242 Items : constant Node_Id := Contract (Pack_Id); 1243 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); 1244 1245 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1246 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1247 -- Save the SPARK_Mode-related data to restore on exit 1248 1249 Init : Node_Id := Empty; 1250 Init_Cond : Node_Id := Empty; 1251 Prag : Node_Id; 1252 Prag_Nam : Name_Id; 1253 1254 begin 1255 -- Do not analyze a contract multiple times 1256 1257 if Present (Items) then 1258 if Analyzed (Items) then 1259 return; 1260 else 1261 Set_Analyzed (Items); 1262 end if; 1263 end if; 1264 1265 -- Due to the timing of contract analysis, delayed pragmas may be 1266 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1267 -- context. To remedy this, restore the original SPARK_Mode of the 1268 -- related package. 1269 1270 Set_SPARK_Mode (Pack_Id); 1271 1272 if Present (Items) then 1273 1274 -- Locate and store pragmas Initial_Condition and Initializes, since 1275 -- their order of analysis matters. 1276 1277 Prag := Classifications (Items); 1278 while Present (Prag) loop 1279 Prag_Nam := Pragma_Name (Prag); 1280 1281 if Prag_Nam = Name_Initial_Condition then 1282 Init_Cond := Prag; 1283 1284 elsif Prag_Nam = Name_Initializes then 1285 Init := Prag; 1286 end if; 1287 1288 Prag := Next_Pragma (Prag); 1289 end loop; 1290 1291 -- Analyze the initialization-related pragmas. Initializes must come 1292 -- before Initial_Condition due to item dependencies. 1293 1294 if Present (Init) then 1295 Analyze_Initializes_In_Decl_Part (Init); 1296 end if; 1297 1298 if Present (Init_Cond) then 1299 Analyze_Initial_Condition_In_Decl_Part (Init_Cond); 1300 end if; 1301 end if; 1302 1303 -- Restore the SPARK_Mode of the enclosing context after all delayed 1304 -- pragmas have been analyzed. 1305 1306 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1307 1308 -- Capture all global references in a generic package now that the 1309 -- contract has been analyzed. 1310 1311 if Is_Generic_Declaration_Or_Body (Pack_Decl) then 1312 Save_Global_References_In_Contract 1313 (Templ => Original_Node (Pack_Decl), 1314 Gen_Id => Pack_Id); 1315 end if; 1316 end Analyze_Package_Contract; 1317 1318 -------------------------------------------- 1319 -- Analyze_Package_Instantiation_Contract -- 1320 -------------------------------------------- 1321 1322 -- WARNING: This routine manages SPARK regions. Return statements must be 1323 -- replaced by gotos which jump to the end of the routine and restore the 1324 -- SPARK mode. 1325 1326 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is 1327 Inst_Spec : constant Node_Id := 1328 Instance_Spec (Unit_Declaration_Node (Inst_Id)); 1329 1330 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1331 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1332 -- Save the SPARK_Mode-related data to restore on exit 1333 1334 Pack_Id : Entity_Id; 1335 Prag : Node_Id; 1336 1337 begin 1338 -- Nothing to do when the package instantiation is erroneous or left 1339 -- partially decorated. 1340 1341 if No (Inst_Spec) then 1342 return; 1343 end if; 1344 1345 Pack_Id := Defining_Entity (Inst_Spec); 1346 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); 1347 1348 -- Due to the timing of contract analysis, delayed pragmas may be 1349 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1350 -- context. To remedy this, restore the original SPARK_Mode of the 1351 -- related package. 1352 1353 Set_SPARK_Mode (Pack_Id); 1354 1355 -- Check whether the lack of indicator Part_Of agrees with the placement 1356 -- of the package instantiation with respect to the state space. Nested 1357 -- package instantiations do not need to be checked because they inherit 1358 -- Part_Of indicator of the outermost package instantiation (see routine 1359 -- Propagate_Part_Of in Sem_Prag). 1360 1361 if In_Instance then 1362 null; 1363 1364 elsif No (Prag) then 1365 Check_Missing_Part_Of (Pack_Id); 1366 end if; 1367 1368 -- Restore the SPARK_Mode of the enclosing context after all delayed 1369 -- pragmas have been analyzed. 1370 1371 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1372 end Analyze_Package_Instantiation_Contract; 1373 1374 -------------------------------- 1375 -- Analyze_Protected_Contract -- 1376 -------------------------------- 1377 1378 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is 1379 Items : constant Node_Id := Contract (Prot_Id); 1380 1381 begin 1382 -- Do not analyze a contract multiple times 1383 1384 if Present (Items) then 1385 if Analyzed (Items) then 1386 return; 1387 else 1388 Set_Analyzed (Items); 1389 end if; 1390 end if; 1391 end Analyze_Protected_Contract; 1392 1393 ------------------------------------------- 1394 -- Analyze_Subprogram_Body_Stub_Contract -- 1395 ------------------------------------------- 1396 1397 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is 1398 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); 1399 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); 1400 1401 begin 1402 -- A subprogram body stub may act as its own spec or as the completion 1403 -- of a previous declaration. Depending on the context, the contract of 1404 -- the stub may contain two sets of pragmas. 1405 1406 -- The stub is a completion, the applicable pragmas are: 1407 -- Refined_Depends 1408 -- Refined_Global 1409 1410 if Present (Spec_Id) then 1411 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); 1412 1413 -- The stub acts as its own spec, the applicable pragmas are: 1414 -- Contract_Cases 1415 -- Depends 1416 -- Global 1417 -- Postcondition 1418 -- Precondition 1419 -- Subprogram_Variant 1420 -- Test_Case 1421 1422 else 1423 Analyze_Entry_Or_Subprogram_Contract (Stub_Id); 1424 end if; 1425 end Analyze_Subprogram_Body_Stub_Contract; 1426 1427 --------------------------- 1428 -- Analyze_Task_Contract -- 1429 --------------------------- 1430 1431 -- WARNING: This routine manages SPARK regions. Return statements must be 1432 -- replaced by gotos which jump to the end of the routine and restore the 1433 -- SPARK mode. 1434 1435 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is 1436 Items : constant Node_Id := Contract (Task_Id); 1437 1438 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; 1439 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; 1440 -- Save the SPARK_Mode-related data to restore on exit 1441 1442 Prag : Node_Id; 1443 1444 begin 1445 -- Do not analyze a contract multiple times 1446 1447 if Present (Items) then 1448 if Analyzed (Items) then 1449 return; 1450 else 1451 Set_Analyzed (Items); 1452 end if; 1453 end if; 1454 1455 -- Due to the timing of contract analysis, delayed pragmas may be 1456 -- subject to the wrong SPARK_Mode, usually that of the enclosing 1457 -- context. To remedy this, restore the original SPARK_Mode of the 1458 -- related task unit. 1459 1460 Set_SPARK_Mode (Task_Id); 1461 1462 -- Analyze Global first, as Depends may mention items classified in the 1463 -- global categorization. 1464 1465 Prag := Get_Pragma (Task_Id, Pragma_Global); 1466 1467 if Present (Prag) then 1468 Analyze_Global_In_Decl_Part (Prag); 1469 end if; 1470 1471 -- Depends must be analyzed after Global in order to see the modes of 1472 -- all global items. 1473 1474 Prag := Get_Pragma (Task_Id, Pragma_Depends); 1475 1476 if Present (Prag) then 1477 Analyze_Depends_In_Decl_Part (Prag); 1478 end if; 1479 1480 -- Restore the SPARK_Mode of the enclosing context after all delayed 1481 -- pragmas have been analyzed. 1482 1483 Restore_SPARK_Mode (Saved_SM, Saved_SMP); 1484 end Analyze_Task_Contract; 1485 1486 --------------------------- 1487 -- Analyze_Type_Contract -- 1488 --------------------------- 1489 1490 procedure Analyze_Type_Contract (Type_Id : Entity_Id) is 1491 begin 1492 Check_Type_Or_Object_External_Properties 1493 (Type_Or_Obj_Id => Type_Id); 1494 end Analyze_Type_Contract; 1495 1496 --------------------------- 1497 -- Check_Class_Condition -- 1498 --------------------------- 1499 1500 procedure Check_Class_Condition 1501 (Cond : Node_Id; 1502 Subp : Entity_Id; 1503 Par_Subp : Entity_Id; 1504 Is_Precondition : Boolean) 1505 is 1506 function Check_Entity (N : Node_Id) return Traverse_Result; 1507 -- Check reference to formal of inherited operation or to primitive 1508 -- operation of root type. 1509 1510 ------------------ 1511 -- Check_Entity -- 1512 ------------------ 1513 1514 function Check_Entity (N : Node_Id) return Traverse_Result is 1515 New_E : Entity_Id; 1516 Orig_E : Entity_Id; 1517 1518 begin 1519 if Nkind (N) = N_Identifier 1520 and then Present (Entity (N)) 1521 and then 1522 (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) 1523 and then 1524 (Nkind (Parent (N)) /= N_Attribute_Reference 1525 or else Attribute_Name (Parent (N)) /= Name_Class) 1526 then 1527 -- These checks do not apply to dispatching calls within the 1528 -- condition, but only to calls whose static tag is that of 1529 -- the parent type. 1530 1531 if Is_Subprogram (Entity (N)) 1532 and then Nkind (Parent (N)) = N_Function_Call 1533 and then Present (Controlling_Argument (Parent (N))) 1534 then 1535 return OK; 1536 end if; 1537 1538 -- Determine whether entity has a renaming 1539 1540 Orig_E := Entity (N); 1541 New_E := Get_Mapped_Entity (Orig_E); 1542 1543 if Present (New_E) then 1544 1545 -- AI12-0166: A precondition for a protected operation 1546 -- cannot include an internal call to a protected function 1547 -- of the type. In the case of an inherited condition for an 1548 -- overriding operation, both the operation and the function 1549 -- are given by primitive wrappers. 1550 1551 if Is_Precondition 1552 and then Ekind (New_E) = E_Function 1553 and then Is_Primitive_Wrapper (New_E) 1554 and then Is_Primitive_Wrapper (Subp) 1555 and then Scope (Subp) = Scope (New_E) 1556 then 1557 Error_Msg_Node_2 := Wrapped_Entity (Subp); 1558 Error_Msg_NE 1559 ("internal call to& cannot appear in inherited " 1560 & "precondition of protected operation&", 1561 Subp, Wrapped_Entity (New_E)); 1562 end if; 1563 end if; 1564 1565 -- Check that there are no calls left to abstract operations if 1566 -- the current subprogram is not abstract. 1567 1568 if Present (New_E) 1569 and then Nkind (Parent (N)) = N_Function_Call 1570 and then N = Name (Parent (N)) 1571 then 1572 if not Is_Abstract_Subprogram (Subp) 1573 and then Is_Abstract_Subprogram (New_E) 1574 then 1575 Error_Msg_Sloc := Sloc (Current_Scope); 1576 Error_Msg_Node_2 := Subp; 1577 1578 if Comes_From_Source (Subp) then 1579 Error_Msg_NE 1580 ("cannot call abstract subprogram & in inherited " 1581 & "condition for&#", Subp, New_E); 1582 else 1583 Error_Msg_NE 1584 ("cannot call abstract subprogram & in inherited " 1585 & "condition for inherited&#", Subp, New_E); 1586 end if; 1587 1588 -- In SPARK mode, report error on inherited condition for an 1589 -- inherited operation if it contains a call to an overriding 1590 -- operation, because this implies that the pre/postconditions 1591 -- of the inherited operation have changed silently. 1592 1593 elsif SPARK_Mode = On 1594 and then Warn_On_Suspicious_Contract 1595 and then Present (Alias (Subp)) 1596 and then Present (New_E) 1597 and then Comes_From_Source (New_E) 1598 then 1599 Error_Msg_N 1600 ("cannot modify inherited condition (SPARK RM 6.1.1(1))", 1601 Parent (Subp)); 1602 Error_Msg_Sloc := Sloc (New_E); 1603 Error_Msg_Node_2 := Subp; 1604 Error_Msg_NE 1605 ("\overriding of&# forces overriding of&", 1606 Parent (Subp), New_E); 1607 end if; 1608 end if; 1609 end if; 1610 1611 return OK; 1612 end Check_Entity; 1613 1614 procedure Check_Condition_Entities is 1615 new Traverse_Proc (Check_Entity); 1616 1617 -- Start of processing for Check_Class_Condition 1618 1619 begin 1620 -- No check required if the subprograms match 1621 1622 if Par_Subp = Subp then 1623 return; 1624 end if; 1625 1626 Update_Primitives_Mapping (Par_Subp, Subp); 1627 Map_Formals (Par_Subp, Subp); 1628 Check_Condition_Entities (Cond); 1629 end Check_Class_Condition; 1630 1631 ----------------------------- 1632 -- Create_Generic_Contract -- 1633 ----------------------------- 1634 1635 procedure Create_Generic_Contract (Unit : Node_Id) is 1636 Templ : constant Node_Id := Original_Node (Unit); 1637 Templ_Id : constant Entity_Id := Defining_Entity (Templ); 1638 1639 procedure Add_Generic_Contract_Pragma (Prag : Node_Id); 1640 -- Add a single contract-related source pragma Prag to the contract of 1641 -- generic template Templ_Id. 1642 1643 --------------------------------- 1644 -- Add_Generic_Contract_Pragma -- 1645 --------------------------------- 1646 1647 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is 1648 Prag_Templ : Node_Id; 1649 1650 begin 1651 -- Mark the pragma to prevent the premature capture of global 1652 -- references when capturing global references of the context 1653 -- (see Save_References_In_Pragma). 1654 1655 Set_Is_Generic_Contract_Pragma (Prag); 1656 1657 -- Pragmas that apply to a generic subprogram declaration are not 1658 -- part of the semantic structure of the generic template: 1659 1660 -- generic 1661 -- procedure Example (Formal : Integer); 1662 -- pragma Precondition (Formal > 0); 1663 1664 -- Create a generic template for such pragmas and link the template 1665 -- of the pragma with the generic template. 1666 1667 if Nkind (Templ) = N_Generic_Subprogram_Declaration then 1668 Rewrite 1669 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); 1670 Prag_Templ := Original_Node (Prag); 1671 1672 Set_Is_Generic_Contract_Pragma (Prag_Templ); 1673 Add_Contract_Item (Prag_Templ, Templ_Id); 1674 1675 -- Otherwise link the pragma with the generic template 1676 1677 else 1678 Add_Contract_Item (Prag, Templ_Id); 1679 end if; 1680 end Add_Generic_Contract_Pragma; 1681 1682 -- Local variables 1683 1684 Context : constant Node_Id := Parent (Unit); 1685 Decl : Node_Id := Empty; 1686 1687 -- Start of processing for Create_Generic_Contract 1688 1689 begin 1690 -- A generic package declaration carries contract-related source pragmas 1691 -- in its visible declarations. 1692 1693 if Nkind (Templ) = N_Generic_Package_Declaration then 1694 Mutate_Ekind (Templ_Id, E_Generic_Package); 1695 1696 if Present (Visible_Declarations (Specification (Templ))) then 1697 Decl := First (Visible_Declarations (Specification (Templ))); 1698 end if; 1699 1700 -- A generic package body carries contract-related source pragmas in its 1701 -- declarations. 1702 1703 elsif Nkind (Templ) = N_Package_Body then 1704 Mutate_Ekind (Templ_Id, E_Package_Body); 1705 1706 if Present (Declarations (Templ)) then 1707 Decl := First (Declarations (Templ)); 1708 end if; 1709 1710 -- Generic subprogram declaration 1711 1712 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then 1713 if Nkind (Specification (Templ)) = N_Function_Specification then 1714 Mutate_Ekind (Templ_Id, E_Generic_Function); 1715 else 1716 Mutate_Ekind (Templ_Id, E_Generic_Procedure); 1717 end if; 1718 1719 -- When the generic subprogram acts as a compilation unit, inspect 1720 -- the Pragmas_After list for contract-related source pragmas. 1721 1722 if Nkind (Context) = N_Compilation_Unit then 1723 if Present (Aux_Decls_Node (Context)) 1724 and then Present (Pragmas_After (Aux_Decls_Node (Context))) 1725 then 1726 Decl := First (Pragmas_After (Aux_Decls_Node (Context))); 1727 end if; 1728 1729 -- Otherwise inspect the successive declarations for contract-related 1730 -- source pragmas. 1731 1732 else 1733 Decl := Next (Unit); 1734 end if; 1735 1736 -- A generic subprogram body carries contract-related source pragmas in 1737 -- its declarations. 1738 1739 elsif Nkind (Templ) = N_Subprogram_Body then 1740 Mutate_Ekind (Templ_Id, E_Subprogram_Body); 1741 1742 if Present (Declarations (Templ)) then 1743 Decl := First (Declarations (Templ)); 1744 end if; 1745 end if; 1746 1747 -- Inspect the relevant declarations looking for contract-related source 1748 -- pragmas and add them to the contract of the generic unit. 1749 1750 while Present (Decl) loop 1751 if Comes_From_Source (Decl) then 1752 if Nkind (Decl) = N_Pragma then 1753 1754 -- The source pragma is a contract annotation 1755 1756 if Is_Contract_Annotation (Decl) then 1757 Add_Generic_Contract_Pragma (Decl); 1758 end if; 1759 1760 -- The region where a contract-related source pragma may appear 1761 -- ends with the first source non-pragma declaration or statement. 1762 1763 else 1764 exit; 1765 end if; 1766 end if; 1767 1768 Next (Decl); 1769 end loop; 1770 end Create_Generic_Contract; 1771 1772 -------------------------------- 1773 -- Expand_Subprogram_Contract -- 1774 -------------------------------- 1775 1776 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is 1777 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); 1778 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); 1779 1780 procedure Add_Invariant_And_Predicate_Checks 1781 (Subp_Id : Entity_Id; 1782 Stmts : in out List_Id; 1783 Result : out Node_Id); 1784 -- Process the result of function Subp_Id (if applicable) and all its 1785 -- formals. Add invariant and predicate checks where applicable. The 1786 -- routine appends all the checks to list Stmts. If Subp_Id denotes a 1787 -- function, Result contains the entity of parameter _Result, to be 1788 -- used in the creation of procedure _Postconditions. 1789 1790 procedure Add_Stable_Property_Contracts 1791 (Subp_Id : Entity_Id; Class_Present : Boolean); 1792 -- Augment postcondition contracts to reflect Stable_Property aspect 1793 -- (if Class_Present = False) or Stable_Property'Class aspect (if 1794 -- Class_Present = True). 1795 1796 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); 1797 -- Append a node to a list. If there is no list, create a new one. When 1798 -- the item denotes a pragma, it is added to the list only when it is 1799 -- enabled. 1800 1801 procedure Build_Postconditions_Procedure 1802 (Subp_Id : Entity_Id; 1803 Stmts : List_Id; 1804 Result : Entity_Id); 1805 -- Create the body of procedure _Postconditions which handles various 1806 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list 1807 -- of statements to be checked on exit. Parameter Result is the entity 1808 -- of parameter _Result when Subp_Id denotes a function. 1809 1810 procedure Process_Contract_Cases (Stmts : in out List_Id); 1811 -- Process pragma Contract_Cases. This routine prepends items to the 1812 -- body declarations and appends items to list Stmts. 1813 1814 procedure Process_Postconditions (Stmts : in out List_Id); 1815 -- Collect all [inherited] spec and body postconditions and accumulate 1816 -- their pragma Check equivalents in list Stmts. 1817 1818 procedure Process_Preconditions; 1819 -- Collect all [inherited] spec and body preconditions and prepend their 1820 -- pragma Check equivalents to the declarations of the body. 1821 1822 ---------------------------------------- 1823 -- Add_Invariant_And_Predicate_Checks -- 1824 ---------------------------------------- 1825 1826 procedure Add_Invariant_And_Predicate_Checks 1827 (Subp_Id : Entity_Id; 1828 Stmts : in out List_Id; 1829 Result : out Node_Id) 1830 is 1831 procedure Add_Invariant_Access_Checks (Id : Entity_Id); 1832 -- Id denotes the return value of a function or a formal parameter. 1833 -- Add an invariant check if the type of Id is access to a type with 1834 -- invariants. The routine appends the generated code to Stmts. 1835 1836 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; 1837 -- Determine whether type Typ can benefit from invariant checks. To 1838 -- qualify, the type must have a non-null invariant procedure and 1839 -- subprogram Subp_Id must appear visible from the point of view of 1840 -- the type. 1841 1842 --------------------------------- 1843 -- Add_Invariant_Access_Checks -- 1844 --------------------------------- 1845 1846 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is 1847 Loc : constant Source_Ptr := Sloc (Body_Decl); 1848 Ref : Node_Id; 1849 Typ : Entity_Id; 1850 1851 begin 1852 Typ := Etype (Id); 1853 1854 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then 1855 Typ := Designated_Type (Typ); 1856 1857 if Invariant_Checks_OK (Typ) then 1858 Ref := 1859 Make_Explicit_Dereference (Loc, 1860 Prefix => New_Occurrence_Of (Id, Loc)); 1861 Set_Etype (Ref, Typ); 1862 1863 -- Generate: 1864 -- if <Id> /= null then 1865 -- <invariant_call (<Ref>)> 1866 -- end if; 1867 1868 Append_Enabled_Item 1869 (Item => 1870 Make_If_Statement (Loc, 1871 Condition => 1872 Make_Op_Ne (Loc, 1873 Left_Opnd => New_Occurrence_Of (Id, Loc), 1874 Right_Opnd => Make_Null (Loc)), 1875 Then_Statements => New_List ( 1876 Make_Invariant_Call (Ref))), 1877 List => Stmts); 1878 end if; 1879 end if; 1880 end Add_Invariant_Access_Checks; 1881 1882 ------------------------- 1883 -- Invariant_Checks_OK -- 1884 ------------------------- 1885 1886 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is 1887 function Has_Public_Visibility_Of_Subprogram return Boolean; 1888 -- Determine whether type Typ has public visibility of subprogram 1889 -- Subp_Id. 1890 1891 ----------------------------------------- 1892 -- Has_Public_Visibility_Of_Subprogram -- 1893 ----------------------------------------- 1894 1895 function Has_Public_Visibility_Of_Subprogram return Boolean is 1896 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 1897 1898 begin 1899 -- An Initialization procedure must be considered visible even 1900 -- though it is internally generated. 1901 1902 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then 1903 return True; 1904 1905 elsif Ekind (Scope (Typ)) /= E_Package then 1906 return False; 1907 1908 -- Internally generated code is never publicly visible except 1909 -- for a subprogram that is the implementation of an expression 1910 -- function. In that case the visibility is determined by the 1911 -- last check. 1912 1913 elsif not Comes_From_Source (Subp_Decl) 1914 and then 1915 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function 1916 or else not 1917 Comes_From_Source (Defining_Entity (Subp_Decl))) 1918 then 1919 return False; 1920 1921 -- Determine whether the subprogram is declared in the visible 1922 -- declarations of the package containing the type, or in the 1923 -- visible declaration of a child unit of that package. 1924 1925 else 1926 declare 1927 Decls : constant List_Id := 1928 List_Containing (Subp_Decl); 1929 Subp_Scope : constant Entity_Id := 1930 Scope (Defining_Entity (Subp_Decl)); 1931 Typ_Scope : constant Entity_Id := Scope (Typ); 1932 1933 begin 1934 return 1935 Decls = Visible_Declarations 1936 (Specification (Unit_Declaration_Node (Typ_Scope))) 1937 1938 or else 1939 (Ekind (Subp_Scope) = E_Package 1940 and then Typ_Scope /= Subp_Scope 1941 and then Is_Child_Unit (Subp_Scope) 1942 and then 1943 Is_Ancestor_Package (Typ_Scope, Subp_Scope) 1944 and then 1945 Decls = Visible_Declarations 1946 (Specification 1947 (Unit_Declaration_Node (Subp_Scope)))); 1948 end; 1949 end if; 1950 end Has_Public_Visibility_Of_Subprogram; 1951 1952 -- Start of processing for Invariant_Checks_OK 1953 1954 begin 1955 return 1956 Has_Invariants (Typ) 1957 and then Present (Invariant_Procedure (Typ)) 1958 and then not Has_Null_Body (Invariant_Procedure (Typ)) 1959 and then Has_Public_Visibility_Of_Subprogram; 1960 end Invariant_Checks_OK; 1961 1962 -- Local variables 1963 1964 Loc : constant Source_Ptr := Sloc (Body_Decl); 1965 -- Source location of subprogram body contract 1966 1967 Formal : Entity_Id; 1968 Typ : Entity_Id; 1969 1970 -- Start of processing for Add_Invariant_And_Predicate_Checks 1971 1972 begin 1973 Result := Empty; 1974 1975 -- Process the result of a function 1976 1977 if Ekind (Subp_Id) = E_Function then 1978 Typ := Etype (Subp_Id); 1979 1980 -- Generate _Result which is used in procedure _Postconditions to 1981 -- verify the return value. 1982 1983 Result := Make_Defining_Identifier (Loc, Name_uResult); 1984 Set_Etype (Result, Typ); 1985 1986 -- Add an invariant check when the return type has invariants and 1987 -- the related function is visible to the outside. 1988 1989 if Invariant_Checks_OK (Typ) then 1990 Append_Enabled_Item 1991 (Item => 1992 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), 1993 List => Stmts); 1994 end if; 1995 1996 -- Add an invariant check when the return type is an access to a 1997 -- type with invariants. 1998 1999 Add_Invariant_Access_Checks (Result); 2000 end if; 2001 2002 -- Add invariant checks for all formals that qualify (see AI05-0289 2003 -- and AI12-0044). 2004 2005 Formal := First_Formal (Subp_Id); 2006 while Present (Formal) loop 2007 Typ := Etype (Formal); 2008 2009 if Ekind (Formal) /= E_In_Parameter 2010 or else Ekind (Subp_Id) = E_Procedure 2011 or else Is_Access_Type (Typ) 2012 then 2013 if Invariant_Checks_OK (Typ) then 2014 Append_Enabled_Item 2015 (Item => 2016 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), 2017 List => Stmts); 2018 end if; 2019 2020 Add_Invariant_Access_Checks (Formal); 2021 2022 -- Note: we used to add predicate checks for OUT and IN OUT 2023 -- formals here, but that was misguided, since such checks are 2024 -- performed on the caller side, based on the predicate of the 2025 -- actual, rather than the predicate of the formal. 2026 2027 end if; 2028 2029 Next_Formal (Formal); 2030 end loop; 2031 end Add_Invariant_And_Predicate_Checks; 2032 2033 ----------------------------------- 2034 -- Add_Stable_Property_Contracts -- 2035 ----------------------------------- 2036 2037 procedure Add_Stable_Property_Contracts 2038 (Subp_Id : Entity_Id; Class_Present : Boolean) 2039 is 2040 Loc : constant Source_Ptr := Sloc (Subp_Id); 2041 2042 procedure Insert_Stable_Property_Check 2043 (Formal : Entity_Id; Property_Function : Entity_Id); 2044 -- Build the pragma for one check and insert it in the tree. 2045 2046 function Make_Stable_Property_Condition 2047 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id; 2048 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression. 2049 2050 function Stable_Properties 2051 (Aspect_Bearer : Entity_Id; Negated : out Boolean) 2052 return Subprogram_List; 2053 -- If no aspect specified, then returns length-zero result. 2054 -- Negated indicates that reserved word NOT was specified. 2055 2056 ---------------------------------- 2057 -- Insert_Stable_Property_Check -- 2058 ---------------------------------- 2059 2060 procedure Insert_Stable_Property_Check 2061 (Formal : Entity_Id; Property_Function : Entity_Id) is 2062 2063 Args : constant List_Id := 2064 New_List 2065 (Make_Pragma_Argument_Association 2066 (Sloc => Loc, 2067 Expression => 2068 Make_Stable_Property_Condition 2069 (Formal => Formal, 2070 Property_Function => Property_Function)), 2071 Make_Pragma_Argument_Association 2072 (Sloc => Loc, 2073 Expression => 2074 Make_String_Literal 2075 (Sloc => Loc, 2076 Strval => 2077 "failed stable property check at " 2078 & Build_Location_String (Loc) 2079 & " for parameter " 2080 & To_String (Fully_Qualified_Name_String 2081 (Formal, Append_NUL => False)) 2082 & " and property function " 2083 & To_String (Fully_Qualified_Name_String 2084 (Property_Function, Append_NUL => False)) 2085 ))); 2086 2087 Prag : constant Node_Id := 2088 Make_Pragma (Loc, 2089 Pragma_Identifier => 2090 Make_Identifier (Loc, Name_Postcondition), 2091 Pragma_Argument_Associations => Args, 2092 Class_Present => Class_Present); 2093 2094 Subp_Decl : Node_Id := Subp_Id; 2095 begin 2096 -- Enclosing_Declaration may return, for example, 2097 -- a N_Procedure_Specification node. Cope with this. 2098 loop 2099 Subp_Decl := Enclosing_Declaration (Subp_Decl); 2100 exit when Is_Declaration (Subp_Decl); 2101 Subp_Decl := Parent (Subp_Decl); 2102 pragma Assert (Present (Subp_Decl)); 2103 end loop; 2104 2105 Insert_After_And_Analyze (Subp_Decl, Prag); 2106 end Insert_Stable_Property_Check; 2107 2108 ------------------------------------ 2109 -- Make_Stable_Property_Condition -- 2110 ------------------------------------ 2111 2112 function Make_Stable_Property_Condition 2113 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id 2114 is 2115 function Call_Property_Function return Node_Id is 2116 (Make_Function_Call 2117 (Loc, 2118 Name => 2119 New_Occurrence_Of (Property_Function, Loc), 2120 Parameter_Associations => 2121 New_List (New_Occurrence_Of (Formal, Loc)))); 2122 begin 2123 return Make_Op_Eq 2124 (Loc, 2125 Call_Property_Function, 2126 Make_Attribute_Reference 2127 (Loc, 2128 Prefix => Call_Property_Function, 2129 Attribute_Name => Name_Old)); 2130 end Make_Stable_Property_Condition; 2131 2132 ----------------------- 2133 -- Stable_Properties -- 2134 ----------------------- 2135 2136 function Stable_Properties 2137 (Aspect_Bearer : Entity_Id; Negated : out Boolean) 2138 return Subprogram_List 2139 is 2140 Aspect_Spec : Node_Id := 2141 Find_Value_Of_Aspect 2142 (Aspect_Bearer, Aspect_Stable_Properties, 2143 Class_Present => Class_Present); 2144 begin 2145 -- ??? For a derived type, we wish Find_Value_Of_Aspect 2146 -- somehow knew that this aspect is not inherited. 2147 -- But it doesn't, so we cope with that here. 2148 -- 2149 -- There are probably issues here with inheritance from 2150 -- interface types, where just looking for the one parent type 2151 -- isn't enough. But this is far from the only work needed for 2152 -- Stable_Properties'Class for interface types. 2153 2154 if Is_Derived_Type (Aspect_Bearer) then 2155 declare 2156 Parent_Type : constant Entity_Id := 2157 Etype (Base_Type (Aspect_Bearer)); 2158 begin 2159 if Aspect_Spec = 2160 Find_Value_Of_Aspect 2161 (Parent_Type, Aspect_Stable_Properties, 2162 Class_Present => Class_Present) 2163 then 2164 -- prevent inheritance 2165 Aspect_Spec := Empty; 2166 end if; 2167 end; 2168 end if; 2169 2170 if No (Aspect_Spec) then 2171 Negated := Aspect_Bearer = Subp_Id; 2172 -- This is a little bit subtle. 2173 -- We need to assign True in the Subp_Id case in order to 2174 -- distinguish between no aspect spec at all vs. an 2175 -- explicitly specified "with S_P => []" empty list. 2176 -- In both cases Stable_Properties will return a length-0 2177 -- array, but the two cases are not equivalent. 2178 -- Very roughly speaking the lack of an S_P aspect spec for 2179 -- a subprogram would be equivalent to something like 2180 -- "with S_P => [not]", where we apply the "not" modifier to 2181 -- an empty set of subprograms, if such a construct existed. 2182 -- We could just assign True here, but it seems untidy to 2183 -- return True in the case of an aspect spec for a type 2184 -- (since negation is only allowed for subp S_P aspects). 2185 2186 return (1 .. 0 => <>); 2187 else 2188 return Parse_Aspect_Stable_Properties 2189 (Aspect_Spec, Negated => Negated); 2190 end if; 2191 end Stable_Properties; 2192 2193 Formal : Entity_Id := First_Formal (Subp_Id); 2194 Type_Of_Formal : Entity_Id; 2195 2196 Subp_Properties_Negated : Boolean; 2197 Subp_Properties : constant Subprogram_List := 2198 Stable_Properties (Subp_Id, Subp_Properties_Negated); 2199 2200 -- start of processing for Add_Stable_Property_Contracts 2201 2202 begin 2203 if not (Is_Primitive (Subp_Id) and then Comes_From_Source (Subp_Id)) 2204 then 2205 return; 2206 end if; 2207 2208 while Present (Formal) loop 2209 Type_Of_Formal := Base_Type (Etype (Formal)); 2210 2211 if not Subp_Properties_Negated then 2212 2213 for SPF_Id of Subp_Properties loop 2214 if Type_Of_Formal = Base_Type (Etype (First_Formal (SPF_Id))) 2215 and then Scope (Type_Of_Formal) = Scope (Subp_Id) 2216 then 2217 -- ??? Need to filter out checks for SPFs that are 2218 -- mentioned explicitly in the postcondition of 2219 -- Subp_Id. 2220 2221 Insert_Stable_Property_Check 2222 (Formal => Formal, Property_Function => SPF_Id); 2223 end if; 2224 end loop; 2225 2226 elsif Scope (Type_Of_Formal) = Scope (Subp_Id) then 2227 declare 2228 Ignored : Boolean range False .. False; 2229 2230 Typ_Property_Funcs : constant Subprogram_List := 2231 Stable_Properties (Type_Of_Formal, Negated => Ignored); 2232 2233 function Excluded_By_Aspect_Spec_Of_Subp 2234 (SPF_Id : Entity_Id) return Boolean; 2235 -- Examine Subp_Properties to determine whether SPF should 2236 -- be excluded. 2237 2238 ------------------------------------- 2239 -- Excluded_By_Aspect_Spec_Of_Subp -- 2240 ------------------------------------- 2241 2242 function Excluded_By_Aspect_Spec_Of_Subp 2243 (SPF_Id : Entity_Id) return Boolean is 2244 begin 2245 pragma Assert (Subp_Properties_Negated); 2246 -- Look through renames for equality test here ??? 2247 return (for some F of Subp_Properties => F = SPF_Id); 2248 end Excluded_By_Aspect_Spec_Of_Subp; 2249 2250 -- Look through renames for equality test here ??? 2251 Subp_Is_Stable_Property_Function : constant Boolean := 2252 (for some F of Typ_Property_Funcs => F = Subp_Id); 2253 begin 2254 if not Subp_Is_Stable_Property_Function then 2255 for SPF_Id of Typ_Property_Funcs loop 2256 if not Excluded_By_Aspect_Spec_Of_Subp (SPF_Id) then 2257 -- ??? Need to filter out checks for SPFs that are 2258 -- mentioned explicitly in the postcondition of 2259 -- Subp_Id. 2260 Insert_Stable_Property_Check 2261 (Formal => Formal, Property_Function => SPF_Id); 2262 end if; 2263 end loop; 2264 end if; 2265 end; 2266 end if; 2267 Next_Formal (Formal); 2268 end loop; 2269 end Add_Stable_Property_Contracts; 2270 2271 ------------------------- 2272 -- Append_Enabled_Item -- 2273 ------------------------- 2274 2275 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is 2276 begin 2277 -- Do not chain ignored or disabled pragmas 2278 2279 if Nkind (Item) = N_Pragma 2280 and then (Is_Ignored (Item) or else Is_Disabled (Item)) 2281 then 2282 null; 2283 2284 -- Otherwise, add the item 2285 2286 else 2287 if No (List) then 2288 List := New_List; 2289 end if; 2290 2291 -- If the pragma is a conjunct in a composite postcondition, it 2292 -- has been processed in reverse order. In the postcondition body 2293 -- it must appear before the others. 2294 2295 if Nkind (Item) = N_Pragma 2296 and then From_Aspect_Specification (Item) 2297 and then Split_PPC (Item) 2298 then 2299 Prepend (Item, List); 2300 else 2301 Append (Item, List); 2302 end if; 2303 end if; 2304 end Append_Enabled_Item; 2305 2306 ------------------------------------ 2307 -- Build_Postconditions_Procedure -- 2308 ------------------------------------ 2309 2310 procedure Build_Postconditions_Procedure 2311 (Subp_Id : Entity_Id; 2312 Stmts : List_Id; 2313 Result : Entity_Id) 2314 is 2315 Loc : constant Source_Ptr := Sloc (Body_Decl); 2316 Last_Decl : Node_Id; 2317 Params : List_Id := No_List; 2318 Proc_Bod : Node_Id; 2319 Proc_Decl : Node_Id; 2320 Proc_Id : Entity_Id; 2321 Proc_Spec : Node_Id; 2322 2323 -- Extra declarations needed to handle interactions between 2324 -- postconditions and finalization. 2325 2326 Postcond_Enabled_Decl : Node_Id; 2327 Return_Success_Decl : Node_Id; 2328 Result_Obj_Decl : Node_Id; 2329 Result_Obj_Type_Decl : Node_Id; 2330 Result_Obj_Type : Entity_Id; 2331 2332 -- Start of processing for Build_Postconditions_Procedure 2333 2334 begin 2335 -- Nothing to do if there are no actions to check on exit 2336 2337 if No (Stmts) then 2338 return; 2339 end if; 2340 2341 -- Otherwise, we generate the postcondition procedure and add 2342 -- associated objects and conditions used to coordinate postcondition 2343 -- evaluation with finalization. 2344 2345 -- Generate: 2346 -- 2347 -- procedure _postconditions (Return_Exp : Result_Typ); 2348 -- 2349 -- -- Result_Obj_Type created when Result_Type is non-elementary 2350 -- [type Result_Obj_Type is access all Result_Typ;] 2351 -- 2352 -- Result_Obj : Result_Obj_Type; 2353 -- 2354 -- Postcond_Enabled : Boolean := True; 2355 -- Return_Success_For_Postcond : Boolean := False; 2356 -- 2357 -- procedure _postconditions (Return_Exp : Result_Typ) is 2358 -- begin 2359 -- if Postcond_Enabled and then Return_Success_For_Postcond then 2360 -- [stmts]; 2361 -- end if; 2362 -- end; 2363 2364 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); 2365 Set_Debug_Info_Needed (Proc_Id); 2366 Set_Postconditions_Proc (Subp_Id, Proc_Id); 2367 2368 -- Force the front-end inlining of _Postconditions when generating C 2369 -- code, since its body may have references to itypes defined in the 2370 -- enclosing subprogram, which would cause problems for unnesting 2371 -- routines in the absence of inlining. 2372 2373 if Modify_Tree_For_C then 2374 Set_Has_Pragma_Inline (Proc_Id); 2375 Set_Has_Pragma_Inline_Always (Proc_Id); 2376 Set_Is_Inlined (Proc_Id); 2377 end if; 2378 2379 -- The related subprogram is a function: create the specification of 2380 -- parameter _Result. 2381 2382 if Present (Result) then 2383 Params := New_List ( 2384 Make_Parameter_Specification (Loc, 2385 Defining_Identifier => Result, 2386 Parameter_Type => 2387 New_Occurrence_Of (Etype (Result), Loc))); 2388 end if; 2389 2390 Proc_Spec := 2391 Make_Procedure_Specification (Loc, 2392 Defining_Unit_Name => Proc_Id, 2393 Parameter_Specifications => Params); 2394 2395 Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); 2396 2397 -- Insert _Postconditions before the first source declaration of the 2398 -- body. This ensures that the body will not cause any premature 2399 -- freezing, as it may mention types: 2400 2401 -- Generate: 2402 -- 2403 -- procedure Proc (Obj : Array_Typ) is 2404 -- procedure _postconditions is 2405 -- begin 2406 -- ... Obj ... 2407 -- end _postconditions; 2408 -- 2409 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); 2410 -- begin 2411 2412 -- In the example above, Obj is of type T but the incorrect placement 2413 -- of _Postconditions will cause a crash in gigi due to an out-of- 2414 -- order reference. The body of _Postconditions must be placed after 2415 -- the declaration of Temp to preserve correct visibility. 2416 2417 Insert_Before_First_Source_Declaration 2418 (Proc_Decl, Declarations (Body_Decl)); 2419 Analyze (Proc_Decl); 2420 Last_Decl := Proc_Decl; 2421 2422 -- When Result is present (e.g. the postcondition checks apply to a 2423 -- function) we make a local object to capture the result, so, if 2424 -- needed, we can call the generated postconditions procedure during 2425 -- finalization instead of at the point of return. 2426 2427 -- Note: The placement of the following declarations before the 2428 -- declaration of the body of the postconditions, but after the 2429 -- declaration of the postconditions spec is deliberate and required 2430 -- since other code within the expander expects them to be located 2431 -- here. Perhaps when more space is available in the tree this will 2432 -- no longer be necessary ??? 2433 2434 if Present (Result) then 2435 -- Elementary result types mean a copy is cheap and preferred over 2436 -- using pointers. 2437 2438 if Is_Elementary_Type (Etype (Result)) then 2439 Result_Obj_Type := Etype (Result); 2440 2441 -- Otherwise, we create a named access type to capture the result 2442 2443 -- Generate: 2444 -- 2445 -- type Result_Obj_Type is access all [Result_Type]; 2446 2447 else 2448 Result_Obj_Type := Make_Temporary (Loc, 'R'); 2449 2450 Result_Obj_Type_Decl := 2451 Make_Full_Type_Declaration (Loc, 2452 Defining_Identifier => Result_Obj_Type, 2453 Type_Definition => 2454 Make_Access_To_Object_Definition (Loc, 2455 All_Present => True, 2456 Subtype_Indication => New_Occurrence_Of 2457 (Etype (Result), Loc))); 2458 Insert_After_And_Analyze (Proc_Decl, Result_Obj_Type_Decl); 2459 Last_Decl := Result_Obj_Type_Decl; 2460 end if; 2461 2462 -- Create the result obj declaration 2463 2464 -- Generate: 2465 -- 2466 -- Result_Object_For_Postcond : Result_Obj_Type; 2467 2468 Result_Obj_Decl := 2469 Make_Object_Declaration (Loc, 2470 Defining_Identifier => 2471 Make_Defining_Identifier 2472 (Loc, Name_uResult_Object_For_Postcond), 2473 Object_Definition => 2474 New_Occurrence_Of 2475 (Result_Obj_Type, Loc)); 2476 Set_No_Initialization (Result_Obj_Decl); 2477 Insert_After_And_Analyze (Last_Decl, Result_Obj_Decl); 2478 Last_Decl := Result_Obj_Decl; 2479 end if; 2480 2481 -- Build the Postcond_Enabled flag used to delay evaluation of 2482 -- postconditions until finalization has been performed when cleanup 2483 -- actions are present. 2484 2485 -- NOTE: This flag could be made into a predicate since we should be 2486 -- able at compile time to recognize when finalization and cleanup 2487 -- actions occur, but in practice this is not possible ??? 2488 2489 -- Generate: 2490 -- 2491 -- Postcond_Enabled : Boolean := True; 2492 2493 Postcond_Enabled_Decl := 2494 Make_Object_Declaration (Loc, 2495 Defining_Identifier => 2496 Make_Defining_Identifier 2497 (Loc, Name_uPostcond_Enabled), 2498 Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc), 2499 Expression => New_Occurrence_Of (Standard_True, Loc)); 2500 Insert_After_And_Analyze (Last_Decl, Postcond_Enabled_Decl); 2501 Last_Decl := Postcond_Enabled_Decl; 2502 2503 -- Create a flag to indicate that return has been reached 2504 2505 -- This is necessary for deciding whether to execute _postconditions 2506 -- during finalization. 2507 2508 -- Generate: 2509 -- 2510 -- Return_Success_For_Postcond : Boolean := False; 2511 2512 Return_Success_Decl := 2513 Make_Object_Declaration (Loc, 2514 Defining_Identifier => 2515 Make_Defining_Identifier 2516 (Loc, Name_uReturn_Success_For_Postcond), 2517 Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc), 2518 Expression => New_Occurrence_Of (Standard_False, Loc)); 2519 Insert_After_And_Analyze (Last_Decl, Return_Success_Decl); 2520 Last_Decl := Return_Success_Decl; 2521 2522 -- Set an explicit End_Label to override the sloc of the implicit 2523 -- RETURN statement, and prevent it from inheriting the sloc of one 2524 -- the postconditions: this would cause confusing debug info to be 2525 -- produced, interfering with coverage-analysis tools. 2526 2527 -- NOTE: Coverage-analysis and static-analysis tools rely on the 2528 -- postconditions procedure being free of internally generated code 2529 -- since some of these tools, like CodePeer, treat _postconditions 2530 -- as original source. 2531 2532 -- Generate: 2533 -- 2534 -- procedure _postconditions is 2535 -- begin 2536 -- [Stmts]; 2537 -- end; 2538 2539 Proc_Bod := 2540 Make_Subprogram_Body (Loc, 2541 Specification => 2542 Copy_Subprogram_Spec (Proc_Spec), 2543 Declarations => Empty_List, 2544 Handled_Statement_Sequence => 2545 Make_Handled_Sequence_Of_Statements (Loc, 2546 End_Label => Make_Identifier (Loc, Chars (Proc_Id)), 2547 Statements => Stmts)); 2548 Insert_After_And_Analyze (Last_Decl, Proc_Bod); 2549 2550 end Build_Postconditions_Procedure; 2551 2552 ---------------------------- 2553 -- Process_Contract_Cases -- 2554 ---------------------------- 2555 2556 procedure Process_Contract_Cases (Stmts : in out List_Id) is 2557 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); 2558 -- Process pragma Contract_Cases for subprogram Subp_Id 2559 2560 -------------------------------- 2561 -- Process_Contract_Cases_For -- 2562 -------------------------------- 2563 2564 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is 2565 Items : constant Node_Id := Contract (Subp_Id); 2566 Prag : Node_Id; 2567 2568 begin 2569 if Present (Items) then 2570 Prag := Contract_Test_Cases (Items); 2571 while Present (Prag) loop 2572 if Is_Checked (Prag) then 2573 if Pragma_Name (Prag) = Name_Contract_Cases then 2574 Expand_Pragma_Contract_Cases 2575 (CCs => Prag, 2576 Subp_Id => Subp_Id, 2577 Decls => Declarations (Body_Decl), 2578 Stmts => Stmts); 2579 2580 elsif Pragma_Name (Prag) = Name_Subprogram_Variant then 2581 Expand_Pragma_Subprogram_Variant 2582 (Prag => Prag, 2583 Subp_Id => Subp_Id, 2584 Body_Decls => Declarations (Body_Decl)); 2585 end if; 2586 end if; 2587 2588 Prag := Next_Pragma (Prag); 2589 end loop; 2590 end if; 2591 end Process_Contract_Cases_For; 2592 2593 pragma Unmodified (Stmts); 2594 -- Stmts is passed as IN OUT to signal that the list can be updated, 2595 -- even if the corresponding integer value representing the list does 2596 -- not change. 2597 2598 -- Start of processing for Process_Contract_Cases 2599 2600 begin 2601 Process_Contract_Cases_For (Body_Id); 2602 2603 if Present (Spec_Id) then 2604 Process_Contract_Cases_For (Spec_Id); 2605 end if; 2606 end Process_Contract_Cases; 2607 2608 ---------------------------- 2609 -- Process_Postconditions -- 2610 ---------------------------- 2611 2612 procedure Process_Postconditions (Stmts : in out List_Id) is 2613 procedure Process_Body_Postconditions (Post_Nam : Name_Id); 2614 -- Collect all [refined] postconditions of a specific kind denoted 2615 -- by Post_Nam that belong to the body, and generate pragma Check 2616 -- equivalents in list Stmts. 2617 2618 procedure Process_Spec_Postconditions; 2619 -- Collect all [inherited] postconditions of the spec, and generate 2620 -- pragma Check equivalents in list Stmts. 2621 2622 --------------------------------- 2623 -- Process_Body_Postconditions -- 2624 --------------------------------- 2625 2626 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is 2627 Items : constant Node_Id := Contract (Body_Id); 2628 Unit_Decl : constant Node_Id := Parent (Body_Decl); 2629 Decl : Node_Id; 2630 Prag : Node_Id; 2631 2632 begin 2633 -- Process the contract 2634 2635 if Present (Items) then 2636 Prag := Pre_Post_Conditions (Items); 2637 while Present (Prag) loop 2638 if Pragma_Name (Prag) = Post_Nam 2639 and then Is_Checked (Prag) 2640 then 2641 Append_Enabled_Item 2642 (Item => Build_Pragma_Check_Equivalent (Prag), 2643 List => Stmts); 2644 end if; 2645 2646 Prag := Next_Pragma (Prag); 2647 end loop; 2648 end if; 2649 2650 -- The subprogram body being processed is actually the proper body 2651 -- of a stub with a corresponding spec. The subprogram stub may 2652 -- carry a postcondition pragma, in which case it must be taken 2653 -- into account. The pragma appears after the stub. 2654 2655 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then 2656 Decl := Next (Corresponding_Stub (Unit_Decl)); 2657 while Present (Decl) loop 2658 2659 -- Note that non-matching pragmas are skipped 2660 2661 if Nkind (Decl) = N_Pragma then 2662 if Pragma_Name (Decl) = Post_Nam 2663 and then Is_Checked (Decl) 2664 then 2665 Append_Enabled_Item 2666 (Item => Build_Pragma_Check_Equivalent (Decl), 2667 List => Stmts); 2668 end if; 2669 2670 -- Skip internally generated code 2671 2672 elsif not Comes_From_Source (Decl) then 2673 null; 2674 2675 -- Postcondition pragmas are usually grouped together. There 2676 -- is no need to inspect the whole declarative list. 2677 2678 else 2679 exit; 2680 end if; 2681 2682 Next (Decl); 2683 end loop; 2684 end if; 2685 end Process_Body_Postconditions; 2686 2687 --------------------------------- 2688 -- Process_Spec_Postconditions -- 2689 --------------------------------- 2690 2691 procedure Process_Spec_Postconditions is 2692 Subps : constant Subprogram_List := 2693 Inherited_Subprograms (Spec_Id); 2694 Seen : Subprogram_List (Subps'Range) := (others => Empty); 2695 2696 function Seen_Subp (Subp_Id : Entity_Id) return Boolean; 2697 -- Return True if the contract of subprogram Subp_Id has been 2698 -- processed. 2699 2700 --------------- 2701 -- Seen_Subp -- 2702 --------------- 2703 2704 function Seen_Subp (Subp_Id : Entity_Id) return Boolean is 2705 begin 2706 for Index in Seen'Range loop 2707 if Seen (Index) = Subp_Id then 2708 return True; 2709 end if; 2710 end loop; 2711 2712 return False; 2713 end Seen_Subp; 2714 2715 -- Local variables 2716 2717 Item : Node_Id; 2718 Items : Node_Id; 2719 Prag : Node_Id; 2720 Subp_Id : Entity_Id; 2721 2722 -- Start of processing for Process_Spec_Postconditions 2723 2724 begin 2725 -- Process the contract 2726 2727 Items := Contract (Spec_Id); 2728 2729 if Present (Items) then 2730 Prag := Pre_Post_Conditions (Items); 2731 while Present (Prag) loop 2732 if Pragma_Name (Prag) = Name_Postcondition 2733 and then Is_Checked (Prag) 2734 then 2735 Append_Enabled_Item 2736 (Item => Build_Pragma_Check_Equivalent (Prag), 2737 List => Stmts); 2738 end if; 2739 2740 Prag := Next_Pragma (Prag); 2741 end loop; 2742 end if; 2743 2744 -- Process the contracts of all inherited subprograms, looking for 2745 -- class-wide postconditions. 2746 2747 for Index in Subps'Range loop 2748 Subp_Id := Subps (Index); 2749 2750 if Present (Alias (Subp_Id)) then 2751 Subp_Id := Ultimate_Alias (Subp_Id); 2752 end if; 2753 2754 -- Wrappers of class-wide pre/postconditions reference the 2755 -- parent primitive that has the inherited contract. 2756 2757 if Is_Wrapper (Subp_Id) 2758 and then Present (LSP_Subprogram (Subp_Id)) 2759 then 2760 Subp_Id := LSP_Subprogram (Subp_Id); 2761 end if; 2762 2763 Items := Contract (Subp_Id); 2764 2765 if not Seen_Subp (Subp_Id) and then Present (Items) then 2766 Seen (Index) := Subp_Id; 2767 2768 Prag := Pre_Post_Conditions (Items); 2769 while Present (Prag) loop 2770 if Pragma_Name (Prag) = Name_Postcondition 2771 and then Class_Present (Prag) 2772 then 2773 Item := 2774 Build_Pragma_Check_Equivalent 2775 (Prag => Prag, 2776 Subp_Id => Spec_Id, 2777 Inher_Id => Subp_Id); 2778 2779 -- The pragma Check equivalent of the class-wide 2780 -- postcondition is still created even though the 2781 -- pragma may be ignored because the equivalent 2782 -- performs semantic checks. 2783 2784 if Is_Checked (Prag) then 2785 Append_Enabled_Item (Item, Stmts); 2786 end if; 2787 end if; 2788 2789 Prag := Next_Pragma (Prag); 2790 end loop; 2791 end if; 2792 end loop; 2793 end Process_Spec_Postconditions; 2794 2795 pragma Unmodified (Stmts); 2796 -- Stmts is passed as IN OUT to signal that the list can be updated, 2797 -- even if the corresponding integer value representing the list does 2798 -- not change. 2799 2800 -- Start of processing for Process_Postconditions 2801 2802 begin 2803 -- The processing of postconditions is done in reverse order (body 2804 -- first) to ensure the following arrangement: 2805 2806 -- <refined postconditions from body> 2807 -- <postconditions from body> 2808 -- <postconditions from spec> 2809 -- <inherited postconditions> 2810 2811 Process_Body_Postconditions (Name_Refined_Post); 2812 Process_Body_Postconditions (Name_Postcondition); 2813 2814 if Present (Spec_Id) then 2815 Process_Spec_Postconditions; 2816 end if; 2817 end Process_Postconditions; 2818 2819 --------------------------- 2820 -- Process_Preconditions -- 2821 --------------------------- 2822 2823 procedure Process_Preconditions is 2824 Insert_Node : Node_Id := Empty; 2825 -- The insertion node after which all pragma Check equivalents are 2826 -- inserted. 2827 2828 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; 2829 -- Determine whether arbitrary declaration Decl denotes a renaming of 2830 -- a discriminant or protection field _object. 2831 2832 procedure Prepend_To_Decls (Item : Node_Id); 2833 -- Prepend a single item to the declarations of the subprogram body 2834 2835 procedure Prepend_Pragma_To_Decls (Prag : Node_Id); 2836 -- Prepend a normal precondition to the declarations of the body and 2837 -- analyze it. 2838 2839 procedure Process_Preconditions_For (Subp_Id : Entity_Id); 2840 -- Collect all preconditions of subprogram Subp_Id and prepend their 2841 -- pragma Check equivalents to the declarations of the body. 2842 2843 -------------------------- 2844 -- Is_Prologue_Renaming -- 2845 -------------------------- 2846 2847 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is 2848 Nam : Node_Id; 2849 Obj : Entity_Id; 2850 Pref : Node_Id; 2851 Sel : Node_Id; 2852 2853 begin 2854 if Nkind (Decl) = N_Object_Renaming_Declaration then 2855 Obj := Defining_Entity (Decl); 2856 Nam := Name (Decl); 2857 2858 if Nkind (Nam) = N_Selected_Component then 2859 Pref := Prefix (Nam); 2860 Sel := Selector_Name (Nam); 2861 2862 -- A discriminant renaming appears as 2863 -- Discr : constant ... := Prefix.Discr; 2864 2865 if Ekind (Obj) = E_Constant 2866 and then Is_Entity_Name (Sel) 2867 and then Present (Entity (Sel)) 2868 and then Ekind (Entity (Sel)) = E_Discriminant 2869 then 2870 return True; 2871 2872 -- A protection field renaming appears as 2873 -- Prot : ... := _object._object; 2874 2875 -- A renamed private component is just a component of 2876 -- _object, with an arbitrary name. 2877 2878 elsif Ekind (Obj) in E_Variable | E_Constant 2879 and then Nkind (Pref) = N_Identifier 2880 and then Chars (Pref) = Name_uObject 2881 and then Nkind (Sel) = N_Identifier 2882 then 2883 return True; 2884 end if; 2885 end if; 2886 end if; 2887 2888 return False; 2889 end Is_Prologue_Renaming; 2890 2891 ---------------------- 2892 -- Prepend_To_Decls -- 2893 ---------------------- 2894 2895 procedure Prepend_To_Decls (Item : Node_Id) is 2896 Decls : List_Id; 2897 2898 begin 2899 Decls := Declarations (Body_Decl); 2900 2901 -- Ensure that the body has a declarative list 2902 2903 if No (Decls) then 2904 Decls := New_List; 2905 Set_Declarations (Body_Decl, Decls); 2906 end if; 2907 2908 Prepend_To (Decls, Item); 2909 end Prepend_To_Decls; 2910 2911 ----------------------------- 2912 -- Prepend_Pragma_To_Decls -- 2913 ----------------------------- 2914 2915 procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is 2916 Check_Prag : Node_Id; 2917 2918 begin 2919 -- Skip the sole class-wide precondition (if any) since it is 2920 -- processed by Merge_Class_Conditions. 2921 2922 if Class_Present (Prag) then 2923 null; 2924 2925 -- Accumulate the corresponding Check pragmas at the top of the 2926 -- declarations. Prepending the items ensures that they will be 2927 -- evaluated in their original order. 2928 2929 else 2930 Check_Prag := Build_Pragma_Check_Equivalent (Prag); 2931 2932 if Present (Insert_Node) then 2933 Insert_After (Insert_Node, Check_Prag); 2934 else 2935 Prepend_To_Decls (Check_Prag); 2936 end if; 2937 2938 Analyze (Check_Prag); 2939 end if; 2940 end Prepend_Pragma_To_Decls; 2941 2942 ------------------------------- 2943 -- Process_Preconditions_For -- 2944 ------------------------------- 2945 2946 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is 2947 Items : constant Node_Id := Contract (Subp_Id); 2948 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); 2949 Decl : Node_Id; 2950 Freeze_T : Boolean; 2951 Prag : Node_Id; 2952 2953 begin 2954 -- Process the contract. If the body is an expression function 2955 -- that is a completion, freeze types within, because this may 2956 -- not have been done yet, when the subprogram declaration and 2957 -- its completion by an expression function appear in distinct 2958 -- declarative lists of the same unit (visible and private). 2959 2960 Freeze_T := 2961 Was_Expression_Function (Body_Decl) 2962 and then Sloc (Body_Id) /= Sloc (Subp_Id) 2963 and then In_Same_Source_Unit (Body_Id, Subp_Id) 2964 and then not In_Same_List (Body_Decl, Subp_Decl); 2965 2966 if Present (Items) then 2967 Prag := Pre_Post_Conditions (Items); 2968 while Present (Prag) loop 2969 if Pragma_Name (Prag) = Name_Precondition 2970 and then Is_Checked (Prag) 2971 then 2972 if Freeze_T 2973 and then Present (Corresponding_Aspect (Prag)) 2974 then 2975 Freeze_Expr_Types 2976 (Def_Id => Subp_Id, 2977 Typ => Standard_Boolean, 2978 Expr => 2979 Expression 2980 (First (Pragma_Argument_Associations (Prag))), 2981 N => Body_Decl); 2982 end if; 2983 2984 Prepend_Pragma_To_Decls (Prag); 2985 end if; 2986 2987 Prag := Next_Pragma (Prag); 2988 end loop; 2989 end if; 2990 2991 -- The subprogram declaration being processed is actually a body 2992 -- stub. The stub may carry a precondition pragma, in which case 2993 -- it must be taken into account. The pragma appears after the 2994 -- stub. 2995 2996 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then 2997 2998 -- Inspect the declarations following the body stub 2999 3000 Decl := Next (Subp_Decl); 3001 while Present (Decl) loop 3002 3003 -- Note that non-matching pragmas are skipped 3004 3005 if Nkind (Decl) = N_Pragma then 3006 if Pragma_Name (Decl) = Name_Precondition 3007 and then Is_Checked (Decl) 3008 then 3009 Prepend_Pragma_To_Decls (Decl); 3010 end if; 3011 3012 -- Skip internally generated code 3013 3014 elsif not Comes_From_Source (Decl) then 3015 null; 3016 3017 -- Preconditions are usually grouped together. There is no 3018 -- need to inspect the whole declarative list. 3019 3020 else 3021 exit; 3022 end if; 3023 3024 Next (Decl); 3025 end loop; 3026 end if; 3027 end Process_Preconditions_For; 3028 3029 -- Local variables 3030 3031 Decls : constant List_Id := Declarations (Body_Decl); 3032 Decl : Node_Id; 3033 3034 -- Start of processing for Process_Preconditions 3035 3036 begin 3037 -- Find the proper insertion point for all pragma Check equivalents 3038 3039 if Present (Decls) then 3040 Decl := First (Decls); 3041 while Present (Decl) loop 3042 3043 -- First source declaration terminates the search, because all 3044 -- preconditions must be evaluated prior to it, by definition. 3045 3046 if Comes_From_Source (Decl) then 3047 exit; 3048 3049 -- Certain internally generated object renamings such as those 3050 -- for discriminants and protection fields must be elaborated 3051 -- before the preconditions are evaluated, as their expressions 3052 -- may mention the discriminants. The renamings include those 3053 -- for private components so we need to find the last such. 3054 3055 elsif Is_Prologue_Renaming (Decl) then 3056 while Present (Next (Decl)) 3057 and then Is_Prologue_Renaming (Next (Decl)) 3058 loop 3059 Next (Decl); 3060 end loop; 3061 3062 Insert_Node := Decl; 3063 3064 -- Otherwise the declaration does not come from source. This 3065 -- also terminates the search, because internal code may raise 3066 -- exceptions which should not preempt the preconditions. 3067 3068 else 3069 exit; 3070 end if; 3071 3072 Next (Decl); 3073 end loop; 3074 3075 -- The processing of preconditions is done in reverse order (body 3076 -- first), because each pragma Check equivalent is inserted at the 3077 -- top of the declarations. This ensures that the final order is 3078 -- consistent with following diagram: 3079 3080 -- <inherited preconditions> 3081 -- <preconditions from spec> 3082 -- <preconditions from body> 3083 3084 Process_Preconditions_For (Body_Id); 3085 end if; 3086 3087 if Present (Spec_Id) then 3088 Process_Preconditions_For (Spec_Id); 3089 end if; 3090 end Process_Preconditions; 3091 3092 -- Local variables 3093 3094 Restore_Scope : Boolean := False; 3095 Result : Entity_Id; 3096 Stmts : List_Id := No_List; 3097 Subp_Id : Entity_Id; 3098 3099 -- Start of processing for Expand_Subprogram_Contract 3100 3101 begin 3102 -- Obtain the entity of the initial declaration 3103 3104 if Present (Spec_Id) then 3105 Subp_Id := Spec_Id; 3106 else 3107 Subp_Id := Body_Id; 3108 end if; 3109 3110 -- Do not perform expansion activity when it is not needed 3111 3112 if not Expander_Active then 3113 return; 3114 3115 -- GNATprove does not need the executable semantics of a contract 3116 3117 elsif GNATprove_Mode then 3118 return; 3119 3120 -- The contract of a generic subprogram or one declared in a generic 3121 -- context is not expanded, as the corresponding instance will provide 3122 -- the executable semantics of the contract. 3123 3124 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then 3125 return; 3126 3127 -- All subprograms carry a contract, but for some it is not significant 3128 -- and should not be processed. This is a small optimization. 3129 3130 elsif not Has_Significant_Contract (Subp_Id) then 3131 return; 3132 3133 -- The contract of an ignored Ghost subprogram does not need expansion, 3134 -- because the subprogram and all calls to it will be removed. 3135 3136 elsif Is_Ignored_Ghost_Entity (Subp_Id) then 3137 return; 3138 3139 -- No action needed for helpers and indirect-call wrapper built to 3140 -- support class-wide preconditions. 3141 3142 elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then 3143 return; 3144 3145 -- Do not re-expand the same contract. This scenario occurs when a 3146 -- construct is rewritten into something else during its analysis 3147 -- (expression functions for instance). 3148 3149 elsif Has_Expanded_Contract (Subp_Id) then 3150 return; 3151 end if; 3152 3153 -- Prevent multiple expansion attempts of the same contract 3154 3155 Set_Has_Expanded_Contract (Subp_Id); 3156 3157 -- Ensure that the formal parameters are visible when expanding all 3158 -- contract items. 3159 3160 if not In_Open_Scopes (Subp_Id) then 3161 Restore_Scope := True; 3162 Push_Scope (Subp_Id); 3163 3164 if Is_Generic_Subprogram (Subp_Id) then 3165 Install_Generic_Formals (Subp_Id); 3166 else 3167 Install_Formals (Subp_Id); 3168 end if; 3169 end if; 3170 3171 -- The expansion of a subprogram contract involves the creation of Check 3172 -- pragmas to verify the contract assertions of the spec and body in a 3173 -- particular order. The order is as follows: 3174 3175 -- function Example (...) return ... is 3176 -- procedure _Postconditions (...) is 3177 -- begin 3178 -- <refined postconditions from body> 3179 -- <postconditions from body> 3180 -- <postconditions from spec> 3181 -- <inherited postconditions> 3182 -- <contract case consequences> 3183 -- <invariant check of function result> 3184 -- <invariant and predicate checks of parameters> 3185 -- end _Postconditions; 3186 3187 -- <inherited preconditions> 3188 -- <preconditions from spec> 3189 -- <preconditions from body> 3190 -- <contract case conditions> 3191 3192 -- <source declarations> 3193 -- begin 3194 -- <source statements> 3195 3196 -- _Preconditions (Result); 3197 -- return Result; 3198 -- end Example; 3199 3200 -- Routine _Postconditions holds all contract assertions that must be 3201 -- verified on exit from the related subprogram. 3202 3203 -- Step 1: augment contracts list with postconditions associated with 3204 -- Stable_Properties and Stable_Properties'Class aspects. This must 3205 -- precede Process_Postconditions. 3206 3207 for Class_Present in Boolean loop 3208 Add_Stable_Property_Contracts 3209 (Subp_Id, Class_Present => Class_Present); 3210 end loop; 3211 3212 -- Step 2: Handle all preconditions. This action must come before the 3213 -- processing of pragma Contract_Cases because the pragma prepends items 3214 -- to the body declarations. 3215 3216 Process_Preconditions; 3217 3218 -- Step 3: Handle all postconditions. This action must come before the 3219 -- processing of pragma Contract_Cases because the pragma appends items 3220 -- to list Stmts. 3221 3222 Process_Postconditions (Stmts); 3223 3224 -- Step 4: Handle pragma Contract_Cases. This action must come before 3225 -- the processing of invariants and predicates because those append 3226 -- items to list Stmts. 3227 3228 Process_Contract_Cases (Stmts); 3229 3230 -- Step 5: Apply invariant and predicate checks on a function result and 3231 -- all formals. The resulting checks are accumulated in list Stmts. 3232 3233 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); 3234 3235 -- Step 6: Construct procedure _Postconditions 3236 3237 Build_Postconditions_Procedure (Subp_Id, Stmts, Result); 3238 3239 if Restore_Scope then 3240 End_Scope; 3241 end if; 3242 end Expand_Subprogram_Contract; 3243 3244 ------------------------------- 3245 -- Freeze_Previous_Contracts -- 3246 ------------------------------- 3247 3248 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is 3249 function Causes_Contract_Freezing (N : Node_Id) return Boolean; 3250 pragma Inline (Causes_Contract_Freezing); 3251 -- Determine whether arbitrary node N causes contract freezing. This is 3252 -- used as an assertion for the current body declaration that caused 3253 -- contract freezing, and as a condition to detect body declaration that 3254 -- already caused contract freezing before. 3255 3256 procedure Freeze_Contracts; 3257 pragma Inline (Freeze_Contracts); 3258 -- Freeze the contracts of all eligible constructs which precede body 3259 -- Body_Decl. 3260 3261 procedure Freeze_Enclosing_Package_Body; 3262 pragma Inline (Freeze_Enclosing_Package_Body); 3263 -- Freeze the contract of the nearest package body (if any) which 3264 -- encloses body Body_Decl. 3265 3266 ------------------------------ 3267 -- Causes_Contract_Freezing -- 3268 ------------------------------ 3269 3270 function Causes_Contract_Freezing (N : Node_Id) return Boolean is 3271 begin 3272 -- The following condition matches guards for calls to 3273 -- Freeze_Previous_Contracts from routines that analyze various body 3274 -- declarations. In particular, it detects expression functions, as 3275 -- described in the call from Analyze_Subprogram_Body_Helper. 3276 3277 return 3278 Comes_From_Source (Original_Node (N)) 3279 and then 3280 Nkind (N) in 3281 N_Entry_Body | N_Package_Body | N_Protected_Body | 3282 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body; 3283 end Causes_Contract_Freezing; 3284 3285 ---------------------- 3286 -- Freeze_Contracts -- 3287 ---------------------- 3288 3289 procedure Freeze_Contracts is 3290 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); 3291 Decl : Node_Id; 3292 3293 begin 3294 -- Nothing to do when the body which causes freezing does not appear 3295 -- in a declarative list because there cannot possibly be constructs 3296 -- with contracts. 3297 3298 if not Is_List_Member (Body_Decl) then 3299 return; 3300 end if; 3301 3302 -- Inspect the declarations preceding the body, and freeze individual 3303 -- contracts of eligible constructs. 3304 3305 Decl := Prev (Body_Decl); 3306 while Present (Decl) loop 3307 3308 -- Stop the traversal when a preceding construct that causes 3309 -- freezing is encountered as there is no point in refreezing 3310 -- the already frozen constructs. 3311 3312 if Causes_Contract_Freezing (Decl) then 3313 exit; 3314 3315 -- Entry or subprogram declarations 3316 3317 elsif Nkind (Decl) in N_Abstract_Subprogram_Declaration 3318 | N_Entry_Declaration 3319 | N_Generic_Subprogram_Declaration 3320 | N_Subprogram_Declaration 3321 then 3322 Analyze_Entry_Or_Subprogram_Contract 3323 (Subp_Id => Defining_Entity (Decl), 3324 Freeze_Id => Body_Id); 3325 3326 -- Objects 3327 3328 elsif Nkind (Decl) = N_Object_Declaration then 3329 Analyze_Object_Contract 3330 (Obj_Id => Defining_Entity (Decl), 3331 Freeze_Id => Body_Id); 3332 3333 -- Protected units 3334 3335 elsif Nkind (Decl) in N_Protected_Type_Declaration 3336 | N_Single_Protected_Declaration 3337 then 3338 Analyze_Protected_Contract (Defining_Entity (Decl)); 3339 3340 -- Subprogram body stubs 3341 3342 elsif Nkind (Decl) = N_Subprogram_Body_Stub then 3343 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); 3344 3345 -- Task units 3346 3347 elsif Nkind (Decl) in N_Single_Task_Declaration 3348 | N_Task_Type_Declaration 3349 then 3350 Analyze_Task_Contract (Defining_Entity (Decl)); 3351 end if; 3352 3353 if Nkind (Decl) in N_Full_Type_Declaration 3354 | N_Private_Type_Declaration 3355 | N_Task_Type_Declaration 3356 | N_Protected_Type_Declaration 3357 | N_Formal_Type_Declaration 3358 then 3359 Analyze_Type_Contract (Defining_Identifier (Decl)); 3360 end if; 3361 3362 Prev (Decl); 3363 end loop; 3364 end Freeze_Contracts; 3365 3366 ----------------------------------- 3367 -- Freeze_Enclosing_Package_Body -- 3368 ----------------------------------- 3369 3370 procedure Freeze_Enclosing_Package_Body is 3371 Orig_Decl : constant Node_Id := Original_Node (Body_Decl); 3372 Par : Node_Id; 3373 3374 begin 3375 -- Climb the parent chain looking for an enclosing package body. Do 3376 -- not use the scope stack, because a body utilizes the entity of its 3377 -- corresponding spec. 3378 3379 Par := Parent (Body_Decl); 3380 while Present (Par) loop 3381 if Nkind (Par) = N_Package_Body then 3382 Analyze_Package_Body_Contract 3383 (Body_Id => Defining_Entity (Par), 3384 Freeze_Id => Defining_Entity (Body_Decl)); 3385 3386 exit; 3387 3388 -- Do not look for an enclosing package body when the construct 3389 -- which causes freezing is a body generated for an expression 3390 -- function and it appears within a package spec. This ensures 3391 -- that the traversal will not reach too far up the parent chain 3392 -- and attempt to freeze a package body which must not be frozen. 3393 3394 -- package body Enclosing_Body 3395 -- with Refined_State => (State => Var) 3396 -- is 3397 -- package Nested is 3398 -- type Some_Type is ...; 3399 -- function Cause_Freezing return ...; 3400 -- private 3401 -- function Cause_Freezing is (...); 3402 -- end Nested; 3403 -- 3404 -- Var : Nested.Some_Type; 3405 3406 elsif Nkind (Par) = N_Package_Declaration 3407 and then Nkind (Orig_Decl) = N_Expression_Function 3408 then 3409 exit; 3410 3411 -- Prevent the search from going too far 3412 3413 elsif Is_Body_Or_Package_Declaration (Par) then 3414 exit; 3415 end if; 3416 3417 Par := Parent (Par); 3418 end loop; 3419 end Freeze_Enclosing_Package_Body; 3420 3421 -- Local variables 3422 3423 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); 3424 3425 -- Start of processing for Freeze_Previous_Contracts 3426 3427 begin 3428 pragma Assert (Causes_Contract_Freezing (Body_Decl)); 3429 3430 -- A body that is in the process of being inlined appears from source, 3431 -- but carries name _parent. Such a body does not cause freezing of 3432 -- contracts. 3433 3434 if Chars (Body_Id) = Name_uParent then 3435 return; 3436 end if; 3437 3438 Freeze_Enclosing_Package_Body; 3439 Freeze_Contracts; 3440 end Freeze_Previous_Contracts; 3441 3442 -------------------------- 3443 -- Get_Postcond_Enabled -- 3444 -------------------------- 3445 3446 function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id is 3447 Decl : Node_Id; 3448 begin 3449 Decl := 3450 Next (Unit_Declaration_Node (Postconditions_Proc (Subp))); 3451 while Present (Decl) loop 3452 3453 if Nkind (Decl) = N_Object_Declaration 3454 and then Chars (Defining_Identifier (Decl)) 3455 = Name_uPostcond_Enabled 3456 then 3457 return Defining_Identifier (Decl); 3458 end if; 3459 3460 Next (Decl); 3461 end loop; 3462 3463 return Empty; 3464 end Get_Postcond_Enabled; 3465 3466 ------------------------------------ 3467 -- Get_Result_Object_For_Postcond -- 3468 ------------------------------------ 3469 3470 function Get_Result_Object_For_Postcond 3471 (Subp : Entity_Id) return Entity_Id 3472 is 3473 Decl : Node_Id; 3474 begin 3475 Decl := 3476 Next (Unit_Declaration_Node (Postconditions_Proc (Subp))); 3477 while Present (Decl) loop 3478 3479 if Nkind (Decl) = N_Object_Declaration 3480 and then Chars (Defining_Identifier (Decl)) 3481 = Name_uResult_Object_For_Postcond 3482 then 3483 return Defining_Identifier (Decl); 3484 end if; 3485 3486 Next (Decl); 3487 end loop; 3488 3489 return Empty; 3490 end Get_Result_Object_For_Postcond; 3491 3492 ------------------------------------- 3493 -- Get_Return_Success_For_Postcond -- 3494 ------------------------------------- 3495 3496 function Get_Return_Success_For_Postcond (Subp : Entity_Id) return Entity_Id 3497 is 3498 Decl : Node_Id; 3499 begin 3500 Decl := 3501 Next (Unit_Declaration_Node (Postconditions_Proc (Subp))); 3502 while Present (Decl) loop 3503 3504 if Nkind (Decl) = N_Object_Declaration 3505 and then Chars (Defining_Identifier (Decl)) 3506 = Name_uReturn_Success_For_Postcond 3507 then 3508 return Defining_Identifier (Decl); 3509 end if; 3510 3511 Next (Decl); 3512 end loop; 3513 3514 return Empty; 3515 end Get_Return_Success_For_Postcond; 3516 3517 --------------------------------- 3518 -- Inherit_Subprogram_Contract -- 3519 --------------------------------- 3520 3521 procedure Inherit_Subprogram_Contract 3522 (Subp : Entity_Id; 3523 From_Subp : Entity_Id) 3524 is 3525 procedure Inherit_Pragma (Prag_Id : Pragma_Id); 3526 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to 3527 -- Subp's contract. 3528 3529 -------------------- 3530 -- Inherit_Pragma -- 3531 -------------------- 3532 3533 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is 3534 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); 3535 New_Prag : Node_Id; 3536 3537 begin 3538 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma 3539 -- chains, therefore the node must be replicated. The new pragma is 3540 -- flagged as inherited for distinction purposes. 3541 3542 if Present (Prag) then 3543 New_Prag := New_Copy_Tree (Prag); 3544 Set_Is_Inherited_Pragma (New_Prag); 3545 3546 Add_Contract_Item (New_Prag, Subp); 3547 end if; 3548 end Inherit_Pragma; 3549 3550 -- Start of processing for Inherit_Subprogram_Contract 3551 3552 begin 3553 -- Inheritance is carried out only when both entities are subprograms 3554 -- with contracts. 3555 3556 if Is_Subprogram_Or_Generic_Subprogram (Subp) 3557 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) 3558 and then Present (Contract (From_Subp)) 3559 then 3560 Inherit_Pragma (Pragma_Extensions_Visible); 3561 end if; 3562 end Inherit_Subprogram_Contract; 3563 3564 ------------------------------------- 3565 -- Instantiate_Subprogram_Contract -- 3566 ------------------------------------- 3567 3568 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is 3569 procedure Instantiate_Pragmas (First_Prag : Node_Id); 3570 -- Instantiate all contract-related source pragmas found in the list, 3571 -- starting with pragma First_Prag. Each instantiated pragma is added 3572 -- to list L. 3573 3574 ------------------------- 3575 -- Instantiate_Pragmas -- 3576 ------------------------- 3577 3578 procedure Instantiate_Pragmas (First_Prag : Node_Id) is 3579 Inst_Prag : Node_Id; 3580 Prag : Node_Id; 3581 3582 begin 3583 Prag := First_Prag; 3584 while Present (Prag) loop 3585 if Is_Generic_Contract_Pragma (Prag) then 3586 Inst_Prag := 3587 Copy_Generic_Node (Prag, Empty, Instantiating => True); 3588 3589 Set_Analyzed (Inst_Prag, False); 3590 Append_To (L, Inst_Prag); 3591 end if; 3592 3593 Prag := Next_Pragma (Prag); 3594 end loop; 3595 end Instantiate_Pragmas; 3596 3597 -- Local variables 3598 3599 Items : constant Node_Id := Contract (Defining_Entity (Templ)); 3600 3601 -- Start of processing for Instantiate_Subprogram_Contract 3602 3603 begin 3604 if Present (Items) then 3605 Instantiate_Pragmas (Pre_Post_Conditions (Items)); 3606 Instantiate_Pragmas (Contract_Test_Cases (Items)); 3607 Instantiate_Pragmas (Classifications (Items)); 3608 end if; 3609 end Instantiate_Subprogram_Contract; 3610 3611 ----------------------------------- 3612 -- Make_Class_Precondition_Subps -- 3613 ----------------------------------- 3614 3615 procedure Make_Class_Precondition_Subps 3616 (Subp_Id : Entity_Id; 3617 Late_Overriding : Boolean := False) 3618 is 3619 Loc : constant Source_Ptr := Sloc (Subp_Id); 3620 Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id); 3621 3622 procedure Add_Indirect_Call_Wrapper; 3623 -- Build the indirect-call wrapper and append it to the freezing actions 3624 -- of Tagged_Type. 3625 3626 procedure Add_Call_Helper 3627 (Helper_Id : Entity_Id; 3628 Is_Dynamic : Boolean); 3629 -- Factorizes code for building a call helper with the given identifier 3630 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic 3631 -- controls building the static or dynamic version of the helper. 3632 3633 ------------------------------- 3634 -- Add_Indirect_Call_Wrapper -- 3635 ------------------------------- 3636 3637 procedure Add_Indirect_Call_Wrapper is 3638 3639 function Build_ICW_Body return Node_Id; 3640 -- Build the body of the indirect call wrapper 3641 3642 function Build_ICW_Decl return Node_Id; 3643 -- Build the declaration of the indirect call wrapper 3644 3645 -------------------- 3646 -- Build_ICW_Body -- 3647 -------------------- 3648 3649 function Build_ICW_Body return Node_Id is 3650 ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id); 3651 Spec : constant Node_Id := Parent (ICW_Id); 3652 Body_Spec : Node_Id; 3653 Call : Node_Id; 3654 ICW_Body : Node_Id; 3655 3656 begin 3657 Body_Spec := Copy_Subprogram_Spec (Spec); 3658 3659 -- Build call to wrapped subprogram 3660 3661 declare 3662 Actuals : constant List_Id := Empty_List; 3663 Formal_Spec : Entity_Id := 3664 First (Parameter_Specifications (Spec)); 3665 begin 3666 -- Build parameter association & call 3667 3668 while Present (Formal_Spec) loop 3669 Append_To (Actuals, 3670 New_Occurrence_Of 3671 (Defining_Identifier (Formal_Spec), Loc)); 3672 Next (Formal_Spec); 3673 end loop; 3674 3675 if Ekind (ICW_Id) = E_Procedure then 3676 Call := 3677 Make_Procedure_Call_Statement (Loc, 3678 Name => New_Occurrence_Of (Subp_Id, Loc), 3679 Parameter_Associations => Actuals); 3680 else 3681 Call := 3682 Make_Simple_Return_Statement (Loc, 3683 Expression => 3684 Make_Function_Call (Loc, 3685 Name => New_Occurrence_Of (Subp_Id, Loc), 3686 Parameter_Associations => Actuals)); 3687 end if; 3688 end; 3689 3690 ICW_Body := 3691 Make_Subprogram_Body (Loc, 3692 Specification => Body_Spec, 3693 Declarations => New_List, 3694 Handled_Statement_Sequence => 3695 Make_Handled_Sequence_Of_Statements (Loc, 3696 Statements => New_List (Call))); 3697 3698 -- The new operation is internal and overriding indicators do not 3699 -- apply. 3700 3701 Set_Must_Override (Body_Spec, False); 3702 3703 return ICW_Body; 3704 end Build_ICW_Body; 3705 3706 -------------------- 3707 -- Build_ICW_Decl -- 3708 -------------------- 3709 3710 function Build_ICW_Decl return Node_Id is 3711 ICW_Id : constant Entity_Id := 3712 Make_Defining_Identifier (Loc, 3713 New_External_Name (Chars (Subp_Id), 3714 Suffix => "ICW", 3715 Suffix_Index => Source_Offset (Loc))); 3716 Decl : Node_Id; 3717 Spec : Node_Id; 3718 3719 begin 3720 Spec := Copy_Subprogram_Spec (Parent (Subp_Id)); 3721 Set_Must_Override (Spec, False); 3722 Set_Must_Not_Override (Spec, False); 3723 Set_Defining_Unit_Name (Spec, ICW_Id); 3724 Mutate_Ekind (ICW_Id, Ekind (Subp_Id)); 3725 Set_Is_Public (ICW_Id); 3726 3727 -- The indirect call wrapper is commonly used for indirect calls 3728 -- but inlined for direct calls performed from the DTW. 3729 3730 Set_Is_Inlined (ICW_Id); 3731 3732 if Nkind (Spec) = N_Procedure_Specification then 3733 Set_Null_Present (Spec, False); 3734 end if; 3735 3736 Decl := Make_Subprogram_Declaration (Loc, Spec); 3737 3738 -- Link original subprogram to indirect wrapper and vice versa 3739 3740 Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id); 3741 Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id); 3742 3743 -- Inherit debug info flag to allow debugging the wrapper 3744 3745 if Needs_Debug_Info (Subp_Id) then 3746 Set_Debug_Info_Needed (ICW_Id); 3747 end if; 3748 3749 return Decl; 3750 end Build_ICW_Decl; 3751 3752 -- Local Variables 3753 3754 ICW_Body : Node_Id; 3755 ICW_Decl : Node_Id; 3756 3757 -- Start of processing for Add_Indirect_Call_Wrapper 3758 3759 begin 3760 pragma Assert (No (Indirect_Call_Wrapper (Subp_Id))); 3761 3762 ICW_Decl := Build_ICW_Decl; 3763 3764 Append_Freeze_Action (Tagged_Type, ICW_Decl); 3765 Analyze (ICW_Decl); 3766 3767 ICW_Body := Build_ICW_Body; 3768 Append_Freeze_Action (Tagged_Type, ICW_Body); 3769 3770 -- We cannot defer the analysis of this ICW wrapper when it is 3771 -- built as a consequence of building its partner DTW wrapper 3772 -- at the freezing point of the tagged type. 3773 3774 if Is_Dispatch_Table_Wrapper (Subp_Id) then 3775 Analyze (ICW_Body); 3776 end if; 3777 end Add_Indirect_Call_Wrapper; 3778 3779 --------------------- 3780 -- Add_Call_Helper -- 3781 --------------------- 3782 3783 procedure Add_Call_Helper 3784 (Helper_Id : Entity_Id; 3785 Is_Dynamic : Boolean) 3786 is 3787 function Build_Call_Helper_Body return Node_Id; 3788 -- Build the body of a call helper 3789 3790 function Build_Call_Helper_Decl return Node_Id; 3791 -- Build the declaration of a call helper 3792 3793 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id; 3794 -- Build the specification of the helper 3795 3796 ---------------------------- 3797 -- Build_Call_Helper_Body -- 3798 ---------------------------- 3799 3800 function Build_Call_Helper_Body return Node_Id is 3801 3802 function Copy_And_Update_References 3803 (Expr : Node_Id) return Node_Id; 3804 -- Copy Expr updating references to formals of Helper_Id; update 3805 -- also references to loop identifiers of quantified expressions. 3806 3807 -------------------------------- 3808 -- Copy_And_Update_References -- 3809 -------------------------------- 3810 3811 function Copy_And_Update_References 3812 (Expr : Node_Id) return Node_Id 3813 is 3814 Assoc_List : constant Elist_Id := New_Elmt_List; 3815 3816 procedure Map_Quantified_Expression_Loop_Identifiers; 3817 -- Traverse Expr and append to Assoc_List the mapping of loop 3818 -- identifers of quantified expressions with its new copy. 3819 3820 ------------------------------------------------ 3821 -- Map_Quantified_Expression_Loop_Identifiers -- 3822 ------------------------------------------------ 3823 3824 procedure Map_Quantified_Expression_Loop_Identifiers is 3825 function Map_Loop_Param (N : Node_Id) return Traverse_Result; 3826 -- Append to Assoc_List the mapping of loop identifers of 3827 -- quantified expressions with its new copy. 3828 3829 -------------------- 3830 -- Map_Loop_Param -- 3831 -------------------- 3832 3833 function Map_Loop_Param (N : Node_Id) return Traverse_Result 3834 is 3835 begin 3836 if Nkind (N) = N_Loop_Parameter_Specification 3837 and then Nkind (Parent (N)) = N_Quantified_Expression 3838 then 3839 declare 3840 Def_Id : constant Entity_Id := 3841 Defining_Identifier (N); 3842 begin 3843 Append_Elmt (Def_Id, Assoc_List); 3844 Append_Elmt (New_Copy (Def_Id), Assoc_List); 3845 end; 3846 end if; 3847 3848 return OK; 3849 end Map_Loop_Param; 3850 3851 procedure Map_Quantified_Expressions is 3852 new Traverse_Proc (Map_Loop_Param); 3853 3854 begin 3855 Map_Quantified_Expressions (Expr); 3856 end Map_Quantified_Expression_Loop_Identifiers; 3857 3858 -- Local variables 3859 3860 Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id); 3861 Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id); 3862 3863 -- Start of processing for Copy_And_Update_References 3864 3865 begin 3866 while Present (Subp_Formal_Id) loop 3867 Append_Elmt (Subp_Formal_Id, Assoc_List); 3868 Append_Elmt (Helper_Formal_Id, Assoc_List); 3869 3870 Next_Formal (Subp_Formal_Id); 3871 Next_Formal (Helper_Formal_Id); 3872 end loop; 3873 3874 Map_Quantified_Expression_Loop_Identifiers; 3875 3876 return New_Copy_Tree (Expr, Map => Assoc_List); 3877 end Copy_And_Update_References; 3878 3879 -- Local variables 3880 3881 Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id)); 3882 Body_Id : Entity_Id; 3883 Body_Spec : Node_Id; 3884 Body_Stmts : Node_Id; 3885 Helper_Body : Node_Id; 3886 Return_Expr : Node_Id; 3887 3888 -- Start of processing for Build_Call_Helper_Body 3889 3890 begin 3891 pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id))); 3892 pragma Assert (No (Corresponding_Body (Helper_Decl))); 3893 3894 Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id)); 3895 Body_Spec := Build_Call_Helper_Spec (Body_Id); 3896 3897 Set_Corresponding_Body (Helper_Decl, Body_Id); 3898 Set_Must_Override (Body_Spec, False); 3899 3900 if Present (Class_Preconditions (Subp_Id)) then 3901 Return_Expr := 3902 Copy_And_Update_References (Class_Preconditions (Subp_Id)); 3903 3904 -- When the subprogram is compiled with assertions disabled the 3905 -- helper just returns True; done to avoid reporting errors at 3906 -- link time since a unit may be compiled with assertions disabled 3907 -- and another (which depends on it) compiled with assertions 3908 -- enabled. 3909 3910 else 3911 pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id))); 3912 Return_Expr := New_Occurrence_Of (Standard_True, Loc); 3913 end if; 3914 3915 Body_Stmts := 3916 Make_Handled_Sequence_Of_Statements (Loc, 3917 Statements => New_List ( 3918 Make_Simple_Return_Statement (Loc, Return_Expr))); 3919 3920 Helper_Body := 3921 Make_Subprogram_Body (Loc, 3922 Specification => Body_Spec, 3923 Declarations => New_List, 3924 Handled_Statement_Sequence => Body_Stmts); 3925 3926 return Helper_Body; 3927 end Build_Call_Helper_Body; 3928 3929 ---------------------------- 3930 -- Build_Call_Helper_Decl -- 3931 ---------------------------- 3932 3933 function Build_Call_Helper_Decl return Node_Id is 3934 Decl : Node_Id; 3935 Spec : Node_Id; 3936 3937 begin 3938 Spec := Build_Call_Helper_Spec (Helper_Id); 3939 Set_Must_Override (Spec, False); 3940 Set_Must_Not_Override (Spec, False); 3941 Set_Is_Inlined (Helper_Id); 3942 Set_Is_Public (Helper_Id); 3943 3944 Decl := Make_Subprogram_Declaration (Loc, Spec); 3945 3946 -- Inherit debug info flag from Subp_Id to Helper_Id to allow 3947 -- debugging of the helper subprogram. 3948 3949 if Needs_Debug_Info (Subp_Id) then 3950 Set_Debug_Info_Needed (Helper_Id); 3951 end if; 3952 3953 return Decl; 3954 end Build_Call_Helper_Decl; 3955 3956 ---------------------------- 3957 -- Build_Call_Helper_Spec -- 3958 ---------------------------- 3959 3960 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id 3961 is 3962 Spec : constant Node_Id := Parent (Subp_Id); 3963 Def_Id : constant Node_Id := Defining_Unit_Name (Spec); 3964 Formal : Entity_Id; 3965 Func_Formals : constant List_Id := New_List; 3966 P_Spec : constant List_Id := Parameter_Specifications (Spec); 3967 Par_Formal : Node_Id; 3968 Param : Node_Id; 3969 Param_Type : Node_Id; 3970 3971 begin 3972 -- Create a list of formal parameters with the same types as the 3973 -- original subprogram but changing the controlling formal. 3974 3975 Param := First (P_Spec); 3976 Formal := First_Formal (Def_Id); 3977 while Present (Formal) loop 3978 Par_Formal := Parent (Formal); 3979 3980 if Is_Dynamic and then Is_Controlling_Formal (Formal) then 3981 if Nkind (Parameter_Type (Par_Formal)) 3982 = N_Access_Definition 3983 then 3984 Param_Type := 3985 Copy_Separate_Tree (Parameter_Type (Par_Formal)); 3986 Rewrite (Subtype_Mark (Param_Type), 3987 Make_Attribute_Reference (Loc, 3988 Prefix => Relocate_Node (Subtype_Mark (Param_Type)), 3989 Attribute_Name => Name_Class)); 3990 3991 else 3992 Param_Type := 3993 Make_Attribute_Reference (Loc, 3994 Prefix => New_Occurrence_Of (Etype (Formal), Loc), 3995 Attribute_Name => Name_Class); 3996 end if; 3997 else 3998 Param_Type := New_Occurrence_Of (Etype (Formal), Loc); 3999 end if; 4000 4001 Append_To (Func_Formals, 4002 Make_Parameter_Specification (Loc, 4003 Defining_Identifier => 4004 Make_Defining_Identifier (Loc, Chars (Formal)), 4005 In_Present => In_Present (Par_Formal), 4006 Out_Present => Out_Present (Par_Formal), 4007 Null_Exclusion_Present => Null_Exclusion_Present 4008 (Par_Formal), 4009 Parameter_Type => Param_Type)); 4010 4011 Next (Param); 4012 Next_Formal (Formal); 4013 end loop; 4014 4015 return 4016 Make_Function_Specification (Loc, 4017 Defining_Unit_Name => Spec_Id, 4018 Parameter_Specifications => Func_Formals, 4019 Result_Definition => 4020 New_Occurrence_Of (Standard_Boolean, Loc)); 4021 end Build_Call_Helper_Spec; 4022 4023 -- Local variables 4024 4025 Helper_Body : Node_Id; 4026 Helper_Decl : Node_Id; 4027 4028 -- Start of processing for Add_Call_Helper 4029 4030 begin 4031 Helper_Decl := Build_Call_Helper_Decl; 4032 Mutate_Ekind (Helper_Id, Ekind (Subp_Id)); 4033 4034 -- Add the helper to the freezing actions of the tagged type 4035 4036 Append_Freeze_Action (Tagged_Type, Helper_Decl); 4037 Analyze (Helper_Decl); 4038 4039 Helper_Body := Build_Call_Helper_Body; 4040 Append_Freeze_Action (Tagged_Type, Helper_Body); 4041 4042 -- If this helper is built as part of building the DTW at the 4043 -- freezing point of its tagged type then we cannot defer 4044 -- its analysis. 4045 4046 if Late_Overriding then 4047 pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id)); 4048 Analyze (Helper_Body); 4049 end if; 4050 end Add_Call_Helper; 4051 4052 -- Local variables 4053 4054 Helper_Id : Entity_Id; 4055 4056 -- Start of processing for Make_Class_Precondition_Subps 4057 4058 begin 4059 if Present (Class_Preconditions (Subp_Id)) 4060 or Present (Ignored_Class_Preconditions (Subp_Id)) 4061 then 4062 pragma Assert 4063 (Comes_From_Source (Subp_Id) 4064 or else Is_Dispatch_Table_Wrapper (Subp_Id)); 4065 4066 if No (Dynamic_Call_Helper (Subp_Id)) then 4067 4068 -- Build and add to the freezing actions of Tagged_Type its 4069 -- dynamic-call helper. 4070 4071 Helper_Id := 4072 Make_Defining_Identifier (Loc, 4073 New_External_Name (Chars (Subp_Id), 4074 Suffix => "DP", 4075 Suffix_Index => Source_Offset (Loc))); 4076 Add_Call_Helper (Helper_Id, Is_Dynamic => True); 4077 4078 -- Link original subprogram to helper and vice versa 4079 4080 Set_Dynamic_Call_Helper (Subp_Id, Helper_Id); 4081 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); 4082 end if; 4083 4084 if not Is_Abstract_Subprogram (Subp_Id) 4085 and then No (Static_Call_Helper (Subp_Id)) 4086 then 4087 -- Build and add to the freezing actions of Tagged_Type its 4088 -- static-call helper. 4089 4090 Helper_Id := 4091 Make_Defining_Identifier (Loc, 4092 New_External_Name (Chars (Subp_Id), 4093 Suffix => "SP", 4094 Suffix_Index => Source_Offset (Loc))); 4095 4096 Add_Call_Helper (Helper_Id, Is_Dynamic => False); 4097 4098 -- Link original subprogram to helper and vice versa 4099 4100 Set_Static_Call_Helper (Subp_Id, Helper_Id); 4101 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); 4102 4103 -- Build and add to the freezing actions of Tagged_Type the 4104 -- indirect-call wrapper. 4105 4106 Add_Indirect_Call_Wrapper; 4107 end if; 4108 end if; 4109 end Make_Class_Precondition_Subps; 4110 4111 ---------------------------------------------- 4112 -- Process_Class_Conditions_At_Freeze_Point -- 4113 ---------------------------------------------- 4114 4115 procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is 4116 4117 procedure Check_Class_Conditions (Spec_Id : Entity_Id); 4118 -- Check class-wide pre/postconditions of Spec_Id 4119 4120 function Has_Class_Postconditions_Subprogram 4121 (Spec_Id : Entity_Id) return Boolean; 4122 -- Return True if Spec_Id has (or inherits) a postconditions subprogram. 4123 4124 function Has_Class_Preconditions_Subprogram 4125 (Spec_Id : Entity_Id) return Boolean; 4126 -- Return True if Spec_Id has (or inherits) a preconditions subprogram. 4127 4128 ---------------------------- 4129 -- Check_Class_Conditions -- 4130 ---------------------------- 4131 4132 procedure Check_Class_Conditions (Spec_Id : Entity_Id) is 4133 Par_Subp : Entity_Id; 4134 4135 begin 4136 for Kind in Condition_Kind loop 4137 Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id); 4138 4139 if Present (Par_Subp) then 4140 Check_Class_Condition 4141 (Cond => Class_Condition (Kind, Par_Subp), 4142 Subp => Spec_Id, 4143 Par_Subp => Par_Subp, 4144 Is_Precondition => Kind in Ignored_Class_Precondition 4145 | Class_Precondition); 4146 end if; 4147 end loop; 4148 end Check_Class_Conditions; 4149 4150 ----------------------------------------- 4151 -- Has_Class_Postconditions_Subprogram -- 4152 ----------------------------------------- 4153 4154 function Has_Class_Postconditions_Subprogram 4155 (Spec_Id : Entity_Id) return Boolean is 4156 begin 4157 return 4158 Present (Nearest_Class_Condition_Subprogram 4159 (Spec_Id => Spec_Id, 4160 Kind => Class_Postcondition)) 4161 or else 4162 Present (Nearest_Class_Condition_Subprogram 4163 (Spec_Id => Spec_Id, 4164 Kind => Ignored_Class_Postcondition)); 4165 end Has_Class_Postconditions_Subprogram; 4166 4167 ---------------------------------------- 4168 -- Has_Class_Preconditions_Subprogram -- 4169 ---------------------------------------- 4170 4171 function Has_Class_Preconditions_Subprogram 4172 (Spec_Id : Entity_Id) return Boolean is 4173 begin 4174 return 4175 Present (Nearest_Class_Condition_Subprogram 4176 (Spec_Id => Spec_Id, 4177 Kind => Class_Precondition)) 4178 or else 4179 Present (Nearest_Class_Condition_Subprogram 4180 (Spec_Id => Spec_Id, 4181 Kind => Ignored_Class_Precondition)); 4182 end Has_Class_Preconditions_Subprogram; 4183 4184 -- Local variables 4185 4186 Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ)); 4187 Prim : Entity_Id; 4188 4189 -- Start of processing for Process_Class_Conditions_At_Freeze_Point 4190 4191 begin 4192 while Present (Prim_Elmt) loop 4193 Prim := Node (Prim_Elmt); 4194 4195 if Has_Class_Preconditions_Subprogram (Prim) 4196 or else Has_Class_Postconditions_Subprogram (Prim) 4197 then 4198 if Comes_From_Source (Prim) then 4199 if Has_Significant_Contract (Prim) then 4200 Merge_Class_Conditions (Prim); 4201 end if; 4202 4203 -- Handle wrapper of protected operation 4204 4205 elsif Is_Primitive_Wrapper (Prim) then 4206 Merge_Class_Conditions (Prim); 4207 4208 -- Check inherited class-wide conditions, excluding internal 4209 -- entities built for mapping of interface primitives. 4210 4211 elsif Is_Derived_Type (Typ) 4212 and then Present (Alias (Prim)) 4213 and then No (Interface_Alias (Prim)) 4214 then 4215 Check_Class_Conditions (Prim); 4216 end if; 4217 end if; 4218 4219 Next_Elmt (Prim_Elmt); 4220 end loop; 4221 end Process_Class_Conditions_At_Freeze_Point; 4222 4223 ---------------------------- 4224 -- Merge_Class_Conditions -- 4225 ---------------------------- 4226 4227 procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is 4228 4229 procedure Preanalyze_Condition 4230 (Subp : Entity_Id; 4231 Expr : Node_Id); 4232 -- Preanalyze the class-wide condition Expr of Subp 4233 4234 procedure Process_Inherited_Conditions (Kind : Condition_Kind); 4235 -- Collect all inherited class-wide conditions of Spec_Id and merge 4236 -- them into one big condition. 4237 4238 -------------------------- 4239 -- Preanalyze_Condition -- 4240 -------------------------- 4241 4242 procedure Preanalyze_Condition 4243 (Subp : Entity_Id; 4244 Expr : Node_Id) 4245 is 4246 procedure Clear_Unset_References; 4247 -- Clear unset references on formals of Subp since preanalysis 4248 -- occurs in a place unrelated to the actual code. 4249 4250 procedure Remove_Controlling_Arguments; 4251 -- Traverse Expr and clear the Controlling_Argument of calls to 4252 -- nonabstract functions. 4253 4254 procedure Remove_Formals (Id : Entity_Id); 4255 -- Remove formals from homonym chains and make them not visible 4256 4257 ---------------------------- 4258 -- Clear_Unset_References -- 4259 ---------------------------- 4260 4261 procedure Clear_Unset_References is 4262 F : Entity_Id := First_Formal (Subp); 4263 4264 begin 4265 while Present (F) loop 4266 Set_Unset_Reference (F, Empty); 4267 Next_Formal (F); 4268 end loop; 4269 end Clear_Unset_References; 4270 4271 ---------------------------------- 4272 -- Remove_Controlling_Arguments -- 4273 ---------------------------------- 4274 4275 procedure Remove_Controlling_Arguments is 4276 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result; 4277 -- Reset the Controlling_Argument of calls to nonabstract 4278 -- function calls. 4279 4280 --------------------- 4281 -- Remove_Ctrl_Arg -- 4282 --------------------- 4283 4284 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is 4285 begin 4286 if Nkind (N) = N_Function_Call 4287 and then Present (Controlling_Argument (N)) 4288 and then not Is_Abstract_Subprogram (Entity (Name (N))) 4289 then 4290 Set_Controlling_Argument (N, Empty); 4291 end if; 4292 4293 return OK; 4294 end Remove_Ctrl_Arg; 4295 4296 procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg); 4297 begin 4298 Remove_Ctrl_Args (Expr); 4299 end Remove_Controlling_Arguments; 4300 4301 -------------------- 4302 -- Remove_Formals -- 4303 -------------------- 4304 4305 procedure Remove_Formals (Id : Entity_Id) is 4306 F : Entity_Id := First_Formal (Id); 4307 4308 begin 4309 while Present (F) loop 4310 Set_Is_Immediately_Visible (F, False); 4311 Remove_Homonym (F); 4312 Next_Formal (F); 4313 end loop; 4314 end Remove_Formals; 4315 4316 -- Start of processing for Preanalyze_Condition 4317 4318 begin 4319 pragma Assert (Present (Expr)); 4320 pragma Assert (Inside_Class_Condition_Preanalysis = False); 4321 4322 Push_Scope (Subp); 4323 Install_Formals (Subp); 4324 Inside_Class_Condition_Preanalysis := True; 4325 4326 Preanalyze_And_Resolve (Expr, Standard_Boolean); 4327 4328 Inside_Class_Condition_Preanalysis := False; 4329 Remove_Formals (Subp); 4330 Pop_Scope; 4331 4332 -- Traverse Expr and clear the Controlling_Argument of calls to 4333 -- nonabstract functions. Required since the preanalyzed condition 4334 -- is not yet installed on its definite context and will be cloned 4335 -- and extended in derivations with additional conditions. 4336 4337 Remove_Controlling_Arguments; 4338 4339 -- Clear also attribute Unset_Reference; again because preanalysis 4340 -- occurs in a place unrelated to the actual code. 4341 4342 Clear_Unset_References; 4343 end Preanalyze_Condition; 4344 4345 ---------------------------------- 4346 -- Process_Inherited_Conditions -- 4347 ---------------------------------- 4348 4349 procedure Process_Inherited_Conditions (Kind : Condition_Kind) is 4350 Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id); 4351 Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id); 4352 Seen : Subprogram_List (Subps'Range) := (others => Empty); 4353 4354 function Inherit_Condition 4355 (Par_Subp : Entity_Id; 4356 Subp : Entity_Id) return Node_Id; 4357 -- Inherit the class-wide condition from Par_Subp to Subp and adjust 4358 -- all the references to formals in the inherited condition. 4359 4360 procedure Merge_Conditions (From : Node_Id; Into : Node_Id); 4361 -- Merge two class-wide preconditions or postconditions (the former 4362 -- are merged using "or else", and the latter are merged using "and- 4363 -- then"). The changes are accumulated in parameter Into. 4364 4365 function Seen_Subp (Id : Entity_Id) return Boolean; 4366 -- Return True if the contract of subprogram Id has been processed 4367 4368 ----------------------- 4369 -- Inherit_Condition -- 4370 ----------------------- 4371 4372 function Inherit_Condition 4373 (Par_Subp : Entity_Id; 4374 Subp : Entity_Id) return Node_Id 4375 is 4376 Installed_Calls : constant Elist_Id := New_Elmt_List; 4377 4378 procedure Install_Original_Selected_Component (Expr : Node_Id); 4379 -- Traverse the given expression searching for dispatching calls 4380 -- to functions whose original nodes was a selected component, 4381 -- and replacing them temporarily by a copy of their original 4382 -- node. Modified calls are stored in the list Installed_Calls 4383 -- (to undo this work later). 4384 4385 procedure Restore_Dispatching_Calls (Expr : Node_Id); 4386 -- Undo the work done by Install_Original_Selected_Component. 4387 4388 ----------------------------------------- 4389 -- Install_Original_Selected_Component -- 4390 ----------------------------------------- 4391 4392 procedure Install_Original_Selected_Component (Expr : Node_Id) is 4393 function Install_Node (N : Node_Id) return Traverse_Result; 4394 -- Process a single node 4395 4396 ------------------ 4397 -- Install_Node -- 4398 ------------------ 4399 4400 function Install_Node (N : Node_Id) return Traverse_Result is 4401 New_N : Node_Id; 4402 Orig_Nod : Node_Id; 4403 4404 begin 4405 if Nkind (N) = N_Function_Call 4406 and then Nkind (Original_Node (N)) = N_Selected_Component 4407 and then Is_Dispatching_Operation (Entity (Name (N))) 4408 then 4409 Orig_Nod := Original_Node (N); 4410 4411 -- Temporarily use the original node field to keep the 4412 -- reference to this node (to undo this work later!). 4413 4414 New_N := New_Copy (N); 4415 Set_Original_Node (New_N, Orig_Nod); 4416 Append_Elmt (New_N, Installed_Calls); 4417 4418 Rewrite (N, Orig_Nod); 4419 Set_Original_Node (N, New_N); 4420 end if; 4421 4422 return OK; 4423 end Install_Node; 4424 4425 procedure Install_Nodes is new Traverse_Proc (Install_Node); 4426 4427 begin 4428 Install_Nodes (Expr); 4429 end Install_Original_Selected_Component; 4430 4431 ------------------------------- 4432 -- Restore_Dispatching_Calls -- 4433 ------------------------------- 4434 4435 procedure Restore_Dispatching_Calls (Expr : Node_Id) is 4436 function Restore_Node (N : Node_Id) return Traverse_Result; 4437 -- Process a single node 4438 4439 ------------------ 4440 -- Restore_Node -- 4441 ------------------ 4442 4443 function Restore_Node (N : Node_Id) return Traverse_Result is 4444 Orig_Sel_N : Node_Id; 4445 4446 begin 4447 if Nkind (N) = N_Selected_Component 4448 and then Nkind (Original_Node (N)) = N_Function_Call 4449 and then Contains (Installed_Calls, Original_Node (N)) 4450 then 4451 Orig_Sel_N := Original_Node (Original_Node (N)); 4452 pragma Assert (Nkind (Orig_Sel_N) = N_Selected_Component); 4453 Rewrite (N, Original_Node (N)); 4454 Set_Original_Node (N, Orig_Sel_N); 4455 end if; 4456 4457 return OK; 4458 end Restore_Node; 4459 4460 procedure Restore_Nodes is new Traverse_Proc (Restore_Node); 4461 4462 begin 4463 Restore_Nodes (Expr); 4464 end Restore_Dispatching_Calls; 4465 4466 -- Local variables 4467 4468 Assoc_List : constant Elist_Id := New_Elmt_List; 4469 Par_Formal_Id : Entity_Id := First_Formal (Par_Subp); 4470 Subp_Formal_Id : Entity_Id := First_Formal (Subp); 4471 New_Expr : Node_Id; 4472 Class_Cond : Node_Id; 4473 4474 -- Start of processing for Inherit_Condition 4475 4476 begin 4477 while Present (Par_Formal_Id) loop 4478 Append_Elmt (Par_Formal_Id, Assoc_List); 4479 Append_Elmt (Subp_Formal_Id, Assoc_List); 4480 4481 Next_Formal (Par_Formal_Id); 4482 Next_Formal (Subp_Formal_Id); 4483 end loop; 4484 4485 -- In order to properly preanalyze an inherited preanalyzed 4486 -- condition that has occurrences of the Object.Operation 4487 -- notation we must restore the original node; otherwise we 4488 -- would report spurious errors. 4489 4490 Class_Cond := Class_Condition (Kind, Par_Subp); 4491 4492 Install_Original_Selected_Component (Class_Cond); 4493 New_Expr := New_Copy_Tree (Class_Cond); 4494 Restore_Dispatching_Calls (Class_Cond); 4495 4496 return New_Copy_Tree (New_Expr, Map => Assoc_List); 4497 end Inherit_Condition; 4498 4499 ---------------------- 4500 -- Merge_Conditions -- 4501 ---------------------- 4502 4503 procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is 4504 function Expression_Arg (Expr : Node_Id) return Node_Id; 4505 -- Return the boolean expression argument of a condition while 4506 -- updating its parentheses count for the subsequent merge. 4507 4508 -------------------- 4509 -- Expression_Arg -- 4510 -------------------- 4511 4512 function Expression_Arg (Expr : Node_Id) return Node_Id is 4513 begin 4514 if Paren_Count (Expr) = 0 then 4515 Set_Paren_Count (Expr, 1); 4516 end if; 4517 4518 return Expr; 4519 end Expression_Arg; 4520 4521 -- Local variables 4522 4523 From_Expr : constant Node_Id := Expression_Arg (From); 4524 Into_Expr : constant Node_Id := Expression_Arg (Into); 4525 Loc : constant Source_Ptr := Sloc (Into); 4526 4527 -- Start of processing for Merge_Conditions 4528 4529 begin 4530 case Kind is 4531 4532 -- Merge the two preconditions by "or else"-ing them 4533 4534 when Ignored_Class_Precondition 4535 | Class_Precondition 4536 => 4537 Rewrite (Into_Expr, 4538 Make_Or_Else (Loc, 4539 Right_Opnd => Relocate_Node (Into_Expr), 4540 Left_Opnd => From_Expr)); 4541 4542 -- Merge the two postconditions by "and then"-ing them 4543 4544 when Ignored_Class_Postcondition 4545 | Class_Postcondition 4546 => 4547 Rewrite (Into_Expr, 4548 Make_And_Then (Loc, 4549 Right_Opnd => Relocate_Node (Into_Expr), 4550 Left_Opnd => From_Expr)); 4551 end case; 4552 end Merge_Conditions; 4553 4554 --------------- 4555 -- Seen_Subp -- 4556 --------------- 4557 4558 function Seen_Subp (Id : Entity_Id) return Boolean is 4559 begin 4560 for Index in Seen'Range loop 4561 if Seen (Index) = Id then 4562 return True; 4563 end if; 4564 end loop; 4565 4566 return False; 4567 end Seen_Subp; 4568 4569 -- Local variables 4570 4571 Class_Cond : Node_Id; 4572 Cond : Node_Id; 4573 Subp_Id : Entity_Id; 4574 Par_Prim : Entity_Id := Empty; 4575 Par_Iface_Prims : Elist_Id := No_Elist; 4576 4577 -- Start of processing for Process_Inherited_Conditions 4578 4579 begin 4580 Class_Cond := Class_Condition (Kind, Spec_Id); 4581 4582 -- Process parent primitives looking for nearest ancestor with 4583 -- class-wide conditions. 4584 4585 for Index in Subps'Range loop 4586 Subp_Id := Subps (Index); 4587 4588 if No (Par_Prim) 4589 and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ) 4590 then 4591 if Present (Alias (Subp_Id)) then 4592 Subp_Id := Ultimate_Alias (Subp_Id); 4593 end if; 4594 4595 -- Wrappers of class-wide pre/postconditions reference the 4596 -- parent primitive that has the inherited contract and help 4597 -- us to climb fast. 4598 4599 if Is_Wrapper (Subp_Id) 4600 and then Present (LSP_Subprogram (Subp_Id)) 4601 then 4602 Subp_Id := LSP_Subprogram (Subp_Id); 4603 end if; 4604 4605 if not Seen_Subp (Subp_Id) 4606 and then Present (Class_Condition (Kind, Subp_Id)) 4607 then 4608 Seen (Index) := Subp_Id; 4609 Par_Prim := Subp_Id; 4610 Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim); 4611 4612 Cond := Inherit_Condition 4613 (Subp => Spec_Id, 4614 Par_Subp => Subp_Id); 4615 4616 if Present (Class_Cond) then 4617 Merge_Conditions (Cond, Class_Cond); 4618 else 4619 Class_Cond := Cond; 4620 end if; 4621 4622 Check_Class_Condition 4623 (Cond => Class_Cond, 4624 Subp => Spec_Id, 4625 Par_Subp => Subp_Id, 4626 Is_Precondition => Kind in Ignored_Class_Precondition 4627 | Class_Precondition); 4628 Build_Class_Wide_Expression 4629 (Pragma_Or_Expr => Class_Cond, 4630 Subp => Spec_Id, 4631 Par_Subp => Subp_Id, 4632 Adjust_Sloc => False); 4633 4634 -- We are done as soon as we process the nearest ancestor 4635 4636 exit; 4637 end if; 4638 end if; 4639 end loop; 4640 4641 -- Process the contract of interface primitives not covered by 4642 -- the nearest ancestor. 4643 4644 for Index in Subps'Range loop 4645 Subp_Id := Subps (Index); 4646 4647 if Is_Interface (Find_Dispatching_Type (Subp_Id)) then 4648 if Present (Alias (Subp_Id)) then 4649 Subp_Id := Ultimate_Alias (Subp_Id); 4650 end if; 4651 4652 if not Seen_Subp (Subp_Id) 4653 and then Present (Class_Condition (Kind, Subp_Id)) 4654 and then not Contains (Par_Iface_Prims, Subp_Id) 4655 then 4656 Seen (Index) := Subp_Id; 4657 4658 Cond := Inherit_Condition 4659 (Subp => Spec_Id, 4660 Par_Subp => Subp_Id); 4661 4662 Check_Class_Condition 4663 (Cond => Cond, 4664 Subp => Spec_Id, 4665 Par_Subp => Subp_Id, 4666 Is_Precondition => Kind in Ignored_Class_Precondition 4667 | Class_Precondition); 4668 Build_Class_Wide_Expression 4669 (Pragma_Or_Expr => Cond, 4670 Subp => Spec_Id, 4671 Par_Subp => Subp_Id, 4672 Adjust_Sloc => False); 4673 4674 if Present (Class_Cond) then 4675 Merge_Conditions (Cond, Class_Cond); 4676 else 4677 Class_Cond := Cond; 4678 end if; 4679 end if; 4680 end if; 4681 end loop; 4682 4683 Set_Class_Condition (Kind, Spec_Id, Class_Cond); 4684 end Process_Inherited_Conditions; 4685 4686 -- Local variables 4687 4688 Cond : Node_Id; 4689 4690 -- Start of processing for Merge_Class_Conditions 4691 4692 begin 4693 for Kind in Condition_Kind loop 4694 Cond := Class_Condition (Kind, Spec_Id); 4695 4696 -- If this subprogram has class-wide conditions then preanalyze 4697 -- them before processing inherited conditions since conditions 4698 -- are checked and merged from right to left. 4699 4700 if Present (Cond) then 4701 Preanalyze_Condition (Spec_Id, Cond); 4702 end if; 4703 4704 Process_Inherited_Conditions (Kind); 4705 4706 -- Preanalyze merged inherited conditions 4707 4708 if Cond /= Class_Condition (Kind, Spec_Id) then 4709 Preanalyze_Condition (Spec_Id, 4710 Class_Condition (Kind, Spec_Id)); 4711 end if; 4712 end loop; 4713 end Merge_Class_Conditions; 4714 4715 ---------------------------------------- 4716 -- Save_Global_References_In_Contract -- 4717 ---------------------------------------- 4718 4719 procedure Save_Global_References_In_Contract 4720 (Templ : Node_Id; 4721 Gen_Id : Entity_Id) 4722 is 4723 procedure Save_Global_References_In_List (First_Prag : Node_Id); 4724 -- Save all global references in contract-related source pragmas found 4725 -- in the list, starting with pragma First_Prag. 4726 4727 ------------------------------------ 4728 -- Save_Global_References_In_List -- 4729 ------------------------------------ 4730 4731 procedure Save_Global_References_In_List (First_Prag : Node_Id) is 4732 Prag : Node_Id := First_Prag; 4733 4734 begin 4735 while Present (Prag) loop 4736 if Is_Generic_Contract_Pragma (Prag) then 4737 Save_Global_References (Prag); 4738 end if; 4739 4740 Prag := Next_Pragma (Prag); 4741 end loop; 4742 end Save_Global_References_In_List; 4743 4744 -- Local variables 4745 4746 Items : constant Node_Id := Contract (Defining_Entity (Templ)); 4747 4748 -- Start of processing for Save_Global_References_In_Contract 4749 4750 begin 4751 -- The entity of the analyzed generic copy must be on the scope stack 4752 -- to ensure proper detection of global references. 4753 4754 Push_Scope (Gen_Id); 4755 4756 if Permits_Aspect_Specifications (Templ) 4757 and then Has_Aspects (Templ) 4758 then 4759 Save_Global_References_In_Aspects (Templ); 4760 end if; 4761 4762 if Present (Items) then 4763 Save_Global_References_In_List (Pre_Post_Conditions (Items)); 4764 Save_Global_References_In_List (Contract_Test_Cases (Items)); 4765 Save_Global_References_In_List (Classifications (Items)); 4766 end if; 4767 4768 Pop_Scope; 4769 end Save_Global_References_In_Contract; 4770 4771 ------------------------- 4772 -- Set_Class_Condition -- 4773 ------------------------- 4774 4775 procedure Set_Class_Condition 4776 (Kind : Condition_Kind; 4777 Subp : Entity_Id; 4778 Cond : Node_Id) 4779 is 4780 begin 4781 case Kind is 4782 when Class_Postcondition => 4783 Set_Class_Postconditions (Subp, Cond); 4784 4785 when Class_Precondition => 4786 Set_Class_Preconditions (Subp, Cond); 4787 4788 when Ignored_Class_Postcondition => 4789 Set_Ignored_Class_Postconditions (Subp, Cond); 4790 4791 when Ignored_Class_Precondition => 4792 Set_Ignored_Class_Preconditions (Subp, Cond); 4793 end case; 4794 end Set_Class_Condition; 4795 4796end Contracts; 4797