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