1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- L I B . X R E F . S P A R K _ S P E C I F I C -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2011-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 Einfo; use Einfo; 27with Nmake; use Nmake; 28with SPARK_Xrefs; use SPARK_Xrefs; 29 30with GNAT.HTable; 31 32separate (Lib.Xref) 33package body SPARK_Specific is 34 35 --------------------- 36 -- Local Constants -- 37 --------------------- 38 39 -- Table of SPARK_Entities, True for each entity kind used in SPARK 40 41 SPARK_Entities : constant array (Entity_Kind) of Boolean := 42 (E_Constant => True, 43 E_Entry => True, 44 E_Function => True, 45 E_In_Out_Parameter => True, 46 E_In_Parameter => True, 47 E_Loop_Parameter => True, 48 E_Operator => True, 49 E_Out_Parameter => True, 50 E_Procedure => True, 51 E_Variable => True, 52 others => False); 53 54 -- True for each reference type used in SPARK 55 56 SPARK_References : constant array (Character) of Boolean := 57 ('m' => True, 58 'r' => True, 59 's' => True, 60 others => False); 61 62 type Entity_Hashed_Range is range 0 .. 255; 63 -- Size of hash table headers 64 65 --------------------- 66 -- Local Variables -- 67 --------------------- 68 69 Heap : Entity_Id := Empty; 70 -- A special entity which denotes the heap object 71 72 package Drefs is new Table.Table ( 73 Table_Component_Type => Xref_Entry, 74 Table_Index_Type => Xref_Entry_Number, 75 Table_Low_Bound => 1, 76 Table_Initial => Alloc.Drefs_Initial, 77 Table_Increment => Alloc.Drefs_Increment, 78 Table_Name => "Drefs"); 79 -- Table of cross-references for reads and writes through explicit 80 -- dereferences, that are output as reads/writes to the special variable 81 -- "Heap". These references are added to the regular references when 82 -- computing SPARK cross-references. 83 84 ----------------------- 85 -- Local Subprograms -- 86 ----------------------- 87 88 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat); 89 -- Add file and corresponding scopes for unit to the tables 90 -- SPARK_File_Table and SPARK_Scope_Table. When two units are present for 91 -- the same compilation unit, as it happens for library-level 92 -- instantiations of generics, then Ubody /= Uspec, and all scopes are 93 -- added to the same SPARK file. Otherwise Ubody = Uspec. 94 95 procedure Add_SPARK_Scope (N : Node_Id); 96 -- Add scope N to the table SPARK_Scope_Table 97 98 procedure Add_SPARK_Xrefs; 99 -- Filter table Xrefs to add all references used in SPARK to the table 100 -- SPARK_Xref_Table. 101 102 procedure Detect_And_Add_SPARK_Scope (N : Node_Id); 103 -- Call Add_SPARK_Scope on scopes 104 105 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; 106 -- Hash function for hash table 107 108 procedure Traverse_Declaration_Or_Statement 109 (N : Node_Id; 110 Process : Node_Processing; 111 Inside_Stubs : Boolean); 112 procedure Traverse_Declarations_Or_Statements 113 (L : List_Id; 114 Process : Node_Processing; 115 Inside_Stubs : Boolean); 116 procedure Traverse_Handled_Statement_Sequence 117 (N : Node_Id; 118 Process : Node_Processing; 119 Inside_Stubs : Boolean); 120 procedure Traverse_Protected_Body 121 (N : Node_Id; 122 Process : Node_Processing; 123 Inside_Stubs : Boolean); 124 procedure Traverse_Package_Body 125 (N : Node_Id; 126 Process : Node_Processing; 127 Inside_Stubs : Boolean); 128 procedure Traverse_Subprogram_Body 129 (N : Node_Id; 130 Process : Node_Processing; 131 Inside_Stubs : Boolean); 132 -- Traverse corresponding construct, calling Process on all declarations 133 134 -------------------- 135 -- Add_SPARK_File -- 136 -------------------- 137 138 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat) is 139 File : constant Source_File_Index := Source_Index (Uspec); 140 From : Scope_Index; 141 142 File_Name : String_Ptr; 143 Unit_File_Name : String_Ptr; 144 145 begin 146 -- Source file could be inexistant as a result of an error, if option 147 -- gnatQ is used. 148 149 if File = No_Source_File then 150 return; 151 end if; 152 153 From := SPARK_Scope_Table.Last + 1; 154 155 -- Unit might not have an associated compilation unit, as seen in code 156 -- filling Sdep_Table in Write_ALI. 157 158 if Present (Cunit (Ubody)) then 159 Traverse_Compilation_Unit 160 (CU => Cunit (Ubody), 161 Process => Detect_And_Add_SPARK_Scope'Access, 162 Inside_Stubs => True); 163 end if; 164 165 -- When two units are present for the same compilation unit, as it 166 -- happens for library-level instantiations of generics, then add all 167 -- scopes to the same SPARK file. 168 169 if Ubody /= Uspec then 170 if Present (Cunit (Uspec)) then 171 Traverse_Compilation_Unit 172 (CU => Cunit (Uspec), 173 Process => Detect_And_Add_SPARK_Scope'Access, 174 Inside_Stubs => True); 175 end if; 176 end if; 177 178 -- Update scope numbers 179 180 declare 181 Scope_Id : Int; 182 begin 183 Scope_Id := 1; 184 for Index in From .. SPARK_Scope_Table.Last loop 185 declare 186 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 187 begin 188 S.Scope_Num := Scope_Id; 189 S.File_Num := Dspec; 190 Scope_Id := Scope_Id + 1; 191 end; 192 end loop; 193 end; 194 195 -- Remove those scopes previously marked for removal 196 197 declare 198 Scope_Id : Scope_Index; 199 200 begin 201 Scope_Id := From; 202 for Index in From .. SPARK_Scope_Table.Last loop 203 declare 204 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 205 begin 206 if S.Scope_Num /= 0 then 207 SPARK_Scope_Table.Table (Scope_Id) := S; 208 Scope_Id := Scope_Id + 1; 209 end if; 210 end; 211 end loop; 212 213 SPARK_Scope_Table.Set_Last (Scope_Id - 1); 214 end; 215 216 -- Make entry for new file in file table 217 218 Get_Name_String (Reference_Name (File)); 219 File_Name := new String'(Name_Buffer (1 .. Name_Len)); 220 221 -- For subunits, also retrieve the file name of the unit. Only do so if 222 -- unit has an associated compilation unit. 223 224 if Present (Cunit (Uspec)) 225 and then Present (Cunit (Unit (File))) 226 and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit 227 then 228 Get_Name_String (Reference_Name (Main_Source_File)); 229 Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len)); 230 end if; 231 232 SPARK_File_Table.Append ( 233 (File_Name => File_Name, 234 Unit_File_Name => Unit_File_Name, 235 File_Num => Dspec, 236 From_Scope => From, 237 To_Scope => SPARK_Scope_Table.Last)); 238 end Add_SPARK_File; 239 240 --------------------- 241 -- Add_SPARK_Scope -- 242 --------------------- 243 244 procedure Add_SPARK_Scope (N : Node_Id) is 245 E : constant Entity_Id := Defining_Entity (N); 246 Loc : constant Source_Ptr := Sloc (E); 247 248 -- The character describing the kind of scope is chosen to be the same 249 -- as the one describing the corresponding entity in cross references, 250 -- see Xref_Entity_Letters in lib-xrefs.ads 251 252 Typ : Character; 253 254 begin 255 -- Ignore scopes without a proper location 256 257 if Sloc (N) = No_Location then 258 return; 259 end if; 260 261 case Ekind (E) is 262 when E_Entry 263 | E_Entry_Family 264 | E_Function 265 | E_Generic_Function 266 | E_Generic_Package 267 | E_Generic_Procedure 268 | E_Package 269 | E_Procedure 270 => 271 Typ := Xref_Entity_Letters (Ekind (E)); 272 273 when E_Package_Body | E_Subprogram_Body | E_Task_Body => 274 Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); 275 276 when E_Void => 277 278 -- Compilation of prj-attr.adb with -gnatn creates a node with 279 -- entity E_Void for the package defined at a-charac.ads16:13. 280 -- ??? TBD 281 282 return; 283 284 when others => 285 raise Program_Error; 286 end case; 287 288 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref are 289 -- filled even later, but are initialized to represent an empty range. 290 291 SPARK_Scope_Table.Append ( 292 (Scope_Name => new String'(Unique_Name (E)), 293 File_Num => 0, 294 Scope_Num => 0, 295 Spec_File_Num => 0, 296 Spec_Scope_Num => 0, 297 Line => Nat (Get_Logical_Line_Number (Loc)), 298 Stype => Typ, 299 Col => Nat (Get_Column_Number (Loc)), 300 From_Xref => 1, 301 To_Xref => 0, 302 Scope_Entity => E)); 303 end Add_SPARK_Scope; 304 305 --------------------- 306 -- Add_SPARK_Xrefs -- 307 --------------------- 308 309 procedure Add_SPARK_Xrefs is 310 function Entity_Of_Scope (S : Scope_Index) return Entity_Id; 311 -- Return the entity which maps to the input scope index 312 313 function Get_Entity_Type (E : Entity_Id) return Character; 314 -- Return a character representing the type of entity 315 316 function Is_Constant_Object_Without_Variable_Input 317 (E : Entity_Id) return Boolean; 318 -- Return True if E is known to have no variable input, as defined in 319 -- SPARK RM. 320 321 function Is_Future_Scope_Entity 322 (E : Entity_Id; 323 S : Scope_Index) return Boolean; 324 -- Check whether entity E is in SPARK_Scope_Table at index S or higher 325 326 function Is_SPARK_Reference 327 (E : Entity_Id; 328 Typ : Character) return Boolean; 329 -- Return whether entity reference E meets SPARK requirements. Typ is 330 -- the reference type. 331 332 function Is_SPARK_Scope (E : Entity_Id) return Boolean; 333 -- Return whether the entity or reference scope meets requirements for 334 -- being a SPARK scope. 335 336 function Lt (Op1 : Natural; Op2 : Natural) return Boolean; 337 -- Comparison function for Sort call 338 339 procedure Move (From : Natural; To : Natural); 340 -- Move procedure for Sort call 341 342 procedure Update_Scope_Range 343 (S : Scope_Index; 344 From : Xref_Index; 345 To : Xref_Index); 346 -- Update the scope which maps to S with the new range From .. To 347 348 package Sorting is new GNAT.Heap_Sort_G (Move, Lt); 349 350 function Get_Scope_Num (N : Entity_Id) return Nat; 351 -- Return the scope number associated to entity N 352 353 procedure Set_Scope_Num (N : Entity_Id; Num : Nat); 354 -- Associate entity N to scope number Num 355 356 No_Scope : constant Nat := 0; 357 -- Initial scope counter 358 359 type Scope_Rec is record 360 Num : Nat; 361 Entity : Entity_Id; 362 end record; 363 -- Type used to relate an entity and a scope number 364 365 package Scopes is new GNAT.HTable.Simple_HTable 366 (Header_Num => Entity_Hashed_Range, 367 Element => Scope_Rec, 368 No_Element => (Num => No_Scope, Entity => Empty), 369 Key => Entity_Id, 370 Hash => Entity_Hash, 371 Equal => "="); 372 -- Package used to build a correspondance between entities and scope 373 -- numbers used in SPARK cross references. 374 375 Nrefs : Nat := Xrefs.Last; 376 -- Number of references in table. This value may get reset (reduced) 377 -- when we eliminate duplicate reference entries as well as references 378 -- not suitable for local cross-references. 379 380 Nrefs_Add : constant Nat := Drefs.Last; 381 -- Number of additional references which correspond to dereferences in 382 -- the source code. 383 384 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat; 385 -- This array contains numbers of references in the Xrefs table. This 386 -- list is sorted in output order. The extra 0'th entry is convenient 387 -- for the call to sort. When we sort the table, we move the entries in 388 -- Rnums around, but we do not move the original table entries. 389 390 --------------------- 391 -- Entity_Of_Scope -- 392 --------------------- 393 394 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is 395 begin 396 return SPARK_Scope_Table.Table (S).Scope_Entity; 397 end Entity_Of_Scope; 398 399 --------------------- 400 -- Get_Entity_Type -- 401 --------------------- 402 403 function Get_Entity_Type (E : Entity_Id) return Character is 404 begin 405 case Ekind (E) is 406 when E_Out_Parameter => return '<'; 407 when E_In_Out_Parameter => return '='; 408 when E_In_Parameter => return '>'; 409 when others => return '*'; 410 end case; 411 end Get_Entity_Type; 412 413 ------------------- 414 -- Get_Scope_Num -- 415 ------------------- 416 417 function Get_Scope_Num (N : Entity_Id) return Nat is 418 begin 419 return Scopes.Get (N).Num; 420 end Get_Scope_Num; 421 422 ----------------------------------------------- 423 -- Is_Constant_Object_Without_Variable_Input -- 424 ----------------------------------------------- 425 426 function Is_Constant_Object_Without_Variable_Input 427 (E : Entity_Id) return Boolean 428 is 429 Result : Boolean; 430 431 begin 432 case Ekind (E) is 433 434 -- A constant is known to have no variable input if its 435 -- initializing expression is static (a value which is 436 -- compile-time-known is not guaranteed to have no variable input 437 -- as defined in the SPARK RM). Otherwise, the constant may or not 438 -- have variable input. 439 440 when E_Constant => 441 declare 442 Decl : Node_Id; 443 begin 444 if Present (Full_View (E)) then 445 Decl := Parent (Full_View (E)); 446 else 447 Decl := Parent (E); 448 end if; 449 450 if Is_Imported (E) then 451 Result := False; 452 else 453 pragma Assert (Present (Expression (Decl))); 454 Result := Is_Static_Expression (Expression (Decl)); 455 end if; 456 end; 457 458 when E_Loop_Parameter | E_In_Parameter => 459 Result := True; 460 461 when others => 462 Result := False; 463 end case; 464 465 return Result; 466 end Is_Constant_Object_Without_Variable_Input; 467 468 ---------------------------- 469 -- Is_Future_Scope_Entity -- 470 ---------------------------- 471 472 function Is_Future_Scope_Entity 473 (E : Entity_Id; 474 S : Scope_Index) return Boolean 475 is 476 function Is_Past_Scope_Entity return Boolean; 477 -- Check whether entity E is in SPARK_Scope_Table at index strictly 478 -- lower than S. 479 480 -------------------------- 481 -- Is_Past_Scope_Entity -- 482 -------------------------- 483 484 function Is_Past_Scope_Entity return Boolean is 485 begin 486 for Index in SPARK_Scope_Table.First .. S - 1 loop 487 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then 488 return True; 489 end if; 490 end loop; 491 492 return False; 493 end Is_Past_Scope_Entity; 494 495 -- Start of processing for Is_Future_Scope_Entity 496 497 begin 498 for Index in S .. SPARK_Scope_Table.Last loop 499 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then 500 return True; 501 end if; 502 end loop; 503 504 -- If this assertion fails, this means that the scope which we are 505 -- looking for has been treated already, which reveals a problem in 506 -- the order of cross-references. 507 508 pragma Assert (not Is_Past_Scope_Entity); 509 510 return False; 511 end Is_Future_Scope_Entity; 512 513 ------------------------ 514 -- Is_SPARK_Reference -- 515 ------------------------ 516 517 function Is_SPARK_Reference 518 (E : Entity_Id; 519 Typ : Character) return Boolean 520 is 521 begin 522 -- The only references of interest on callable entities are calls. On 523 -- uncallable entities, the only references of interest are reads and 524 -- writes. 525 526 if Ekind (E) in Overloadable_Kind then 527 return Typ = 's'; 528 529 -- Objects of task or protected types are not SPARK references 530 531 elsif Present (Etype (E)) 532 and then Ekind (Etype (E)) in Concurrent_Kind 533 then 534 return False; 535 536 -- In all other cases, result is true for reference/modify cases, 537 -- and false for all other cases. 538 539 else 540 return Typ = 'r' or else Typ = 'm'; 541 end if; 542 end Is_SPARK_Reference; 543 544 -------------------- 545 -- Is_SPARK_Scope -- 546 -------------------- 547 548 function Is_SPARK_Scope (E : Entity_Id) return Boolean is 549 begin 550 return Present (E) 551 and then not Is_Generic_Unit (E) 552 and then Renamed_Entity (E) = Empty 553 and then Get_Scope_Num (E) /= No_Scope; 554 end Is_SPARK_Scope; 555 556 -------- 557 -- Lt -- 558 -------- 559 560 function Lt (Op1, Op2 : Natural) return Boolean is 561 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1))); 562 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2))); 563 564 begin 565 -- First test: if entity is in different unit, sort by unit. Note: 566 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to 567 -- the file where the generic scope is defined, which may differ from 568 -- the file where the enclosing scope is defined. It is the latter 569 -- which matters for a correct order here. 570 571 if T1.Ent_Scope_File /= T2.Ent_Scope_File then 572 return Dependency_Num (T1.Ent_Scope_File) < 573 Dependency_Num (T2.Ent_Scope_File); 574 575 -- Second test: within same unit, sort by location of the scope of 576 -- the entity definition. 577 578 elsif Get_Scope_Num (T1.Key.Ent_Scope) /= 579 Get_Scope_Num (T2.Key.Ent_Scope) 580 then 581 return Get_Scope_Num (T1.Key.Ent_Scope) < 582 Get_Scope_Num (T2.Key.Ent_Scope); 583 584 -- Third test: within same unit and scope, sort by location of 585 -- entity definition. 586 587 elsif T1.Def /= T2.Def then 588 return T1.Def < T2.Def; 589 590 else 591 -- Both entities must be equal at this point 592 593 pragma Assert (T1.Key.Ent = T2.Key.Ent); 594 595 -- Fourth test: if reference is in same unit as entity definition, 596 -- sort first. 597 598 if T1.Key.Lun /= T2.Key.Lun 599 and then T1.Ent_Scope_File = T1.Key.Lun 600 then 601 return True; 602 603 elsif T1.Key.Lun /= T2.Key.Lun 604 and then T2.Ent_Scope_File = T2.Key.Lun 605 then 606 return False; 607 608 -- Fifth test: if reference is in same unit and same scope as 609 -- entity definition, sort first. 610 611 elsif T1.Ent_Scope_File = T1.Key.Lun 612 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope 613 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope 614 then 615 return True; 616 617 elsif T2.Ent_Scope_File = T2.Key.Lun 618 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope 619 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope 620 then 621 return False; 622 623 -- Sixth test: for same entity, sort by reference location unit 624 625 elsif T1.Key.Lun /= T2.Key.Lun then 626 return Dependency_Num (T1.Key.Lun) < 627 Dependency_Num (T2.Key.Lun); 628 629 -- Seventh test: for same entity, sort by reference location scope 630 631 elsif Get_Scope_Num (T1.Key.Ref_Scope) /= 632 Get_Scope_Num (T2.Key.Ref_Scope) 633 then 634 return Get_Scope_Num (T1.Key.Ref_Scope) < 635 Get_Scope_Num (T2.Key.Ref_Scope); 636 637 -- Eighth test: order of location within referencing unit 638 639 elsif T1.Key.Loc /= T2.Key.Loc then 640 return T1.Key.Loc < T2.Key.Loc; 641 642 -- Finally, for two locations at the same address prefer the one 643 -- that does NOT have the type 'r', so that a modification or 644 -- extension takes preference, when there are more than one 645 -- reference at the same location. As a result, in the case of 646 -- entities that are in-out actuals, the read reference follows 647 -- the modify reference. 648 649 else 650 return T2.Key.Typ = 'r'; 651 end if; 652 end if; 653 end Lt; 654 655 ---------- 656 -- Move -- 657 ---------- 658 659 procedure Move (From : Natural; To : Natural) is 660 begin 661 Rnums (Nat (To)) := Rnums (Nat (From)); 662 end Move; 663 664 ------------------- 665 -- Set_Scope_Num -- 666 ------------------- 667 668 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is 669 begin 670 Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N)); 671 end Set_Scope_Num; 672 673 ------------------------ 674 -- Update_Scope_Range -- 675 ------------------------ 676 677 procedure Update_Scope_Range 678 (S : Scope_Index; 679 From : Xref_Index; 680 To : Xref_Index) 681 is 682 begin 683 SPARK_Scope_Table.Table (S).From_Xref := From; 684 SPARK_Scope_Table.Table (S).To_Xref := To; 685 end Update_Scope_Range; 686 687 -- Local variables 688 689 Col : Nat; 690 From_Index : Xref_Index; 691 Line : Nat; 692 Loc : Source_Ptr; 693 Prev_Typ : Character; 694 Ref_Count : Nat; 695 Ref_Id : Entity_Id; 696 Ref_Name : String_Ptr; 697 Scope_Id : Scope_Index; 698 699 -- Start of processing for Add_SPARK_Xrefs 700 701 begin 702 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 703 declare 704 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 705 begin 706 Set_Scope_Num (S.Scope_Entity, S.Scope_Num); 707 end; 708 end loop; 709 710 -- Set up the pointer vector for the sort 711 712 for Index in 1 .. Nrefs loop 713 Rnums (Index) := Index; 714 end loop; 715 716 for Index in Drefs.First .. Drefs.Last loop 717 Xrefs.Append (Drefs.Table (Index)); 718 719 Nrefs := Nrefs + 1; 720 Rnums (Nrefs) := Xrefs.Last; 721 end loop; 722 723 -- Capture the definition Sloc values. As in the case of normal cross 724 -- references, we have to wait until now to get the correct value. 725 726 for Index in 1 .. Nrefs loop 727 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent); 728 end loop; 729 730 -- Eliminate entries not appropriate for SPARK. Done prior to sorting 731 -- cross-references, as it discards useless references which do not have 732 -- a proper format for the comparison function (like no location). 733 734 Ref_Count := Nrefs; 735 Nrefs := 0; 736 737 for Index in 1 .. Ref_Count loop 738 declare 739 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; 740 741 begin 742 if SPARK_Entities (Ekind (Ref.Ent)) 743 and then SPARK_References (Ref.Typ) 744 and then Is_SPARK_Scope (Ref.Ent_Scope) 745 and then Is_SPARK_Scope (Ref.Ref_Scope) 746 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) 747 748 -- Discard references from unknown scopes, e.g. generic scopes 749 750 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope 751 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope 752 then 753 Nrefs := Nrefs + 1; 754 Rnums (Nrefs) := Rnums (Index); 755 end if; 756 end; 757 end loop; 758 759 -- Sort the references 760 761 Sorting.Sort (Integer (Nrefs)); 762 763 -- Eliminate duplicate entries 764 765 -- We need this test for Ref_Count because if we force ALI file 766 -- generation in case of errors detected, it may be the case that 767 -- Nrefs is 0, so we should not reset it here. 768 769 if Nrefs >= 2 then 770 Ref_Count := Nrefs; 771 Nrefs := 1; 772 773 for Index in 2 .. Ref_Count loop 774 if Xrefs.Table (Rnums (Index)) /= 775 Xrefs.Table (Rnums (Nrefs)) 776 then 777 Nrefs := Nrefs + 1; 778 Rnums (Nrefs) := Rnums (Index); 779 end if; 780 end loop; 781 end if; 782 783 -- Eliminate the reference if it is at the same location as the previous 784 -- one, unless it is a read-reference indicating that the entity is an 785 -- in-out actual in a call. 786 787 Ref_Count := Nrefs; 788 Nrefs := 0; 789 Loc := No_Location; 790 Prev_Typ := 'm'; 791 792 for Index in 1 .. Ref_Count loop 793 declare 794 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; 795 796 begin 797 if Ref.Loc /= Loc 798 or else (Prev_Typ = 'm' and then Ref.Typ = 'r') 799 then 800 Loc := Ref.Loc; 801 Prev_Typ := Ref.Typ; 802 Nrefs := Nrefs + 1; 803 Rnums (Nrefs) := Rnums (Index); 804 end if; 805 end; 806 end loop; 807 808 -- The two steps have eliminated all references, nothing to do 809 810 if SPARK_Scope_Table.Last = 0 then 811 return; 812 end if; 813 814 Ref_Id := Empty; 815 Scope_Id := 1; 816 From_Index := 1; 817 818 -- Loop to output references 819 820 for Refno in 1 .. Nrefs loop 821 declare 822 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); 823 Ref : Xref_Key renames Ref_Entry.Key; 824 Typ : Character; 825 826 begin 827 -- If this assertion fails, the scope which we are looking for is 828 -- not in SPARK scope table, which reveals either a problem in the 829 -- construction of the scope table, or an erroneous scope for the 830 -- current cross-reference. 831 832 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id)); 833 834 -- Update the range of cross references to which the current scope 835 -- refers to. This may be the empty range only for the first scope 836 -- considered. 837 838 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then 839 Update_Scope_Range 840 (S => Scope_Id, 841 From => From_Index, 842 To => SPARK_Xref_Table.Last); 843 844 From_Index := SPARK_Xref_Table.Last + 1; 845 end if; 846 847 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop 848 Scope_Id := Scope_Id + 1; 849 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); 850 end loop; 851 852 if Ref.Ent /= Ref_Id then 853 Ref_Name := new String'(Unique_Name (Ref.Ent)); 854 end if; 855 856 if Ref.Ent = Heap then 857 Line := 0; 858 Col := 0; 859 else 860 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def)); 861 Col := Int (Get_Column_Number (Ref_Entry.Def)); 862 end if; 863 864 -- References to constant objects without variable inputs (see 865 -- SPARK RM 3.3.1) are considered specially in SPARK section, 866 -- because these will be translated as constants in the 867 -- intermediate language for formal verification, and should 868 -- therefore never appear in frame conditions. Other constants may 869 -- later be treated the same, up to GNATprove to decide based on 870 -- its flow analysis. 871 872 if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then 873 Typ := 'c'; 874 else 875 Typ := Ref.Typ; 876 end if; 877 878 SPARK_Xref_Table.Append ( 879 (Entity_Name => Ref_Name, 880 Entity_Line => Line, 881 Etype => Get_Entity_Type (Ref.Ent), 882 Entity_Col => Col, 883 File_Num => Dependency_Num (Ref.Lun), 884 Scope_Num => Get_Scope_Num (Ref.Ref_Scope), 885 Line => Int (Get_Logical_Line_Number (Ref.Loc)), 886 Rtype => Typ, 887 Col => Int (Get_Column_Number (Ref.Loc)))); 888 end; 889 end loop; 890 891 -- Update the range of cross references to which the scope refers to 892 893 Update_Scope_Range 894 (S => Scope_Id, 895 From => From_Index, 896 To => SPARK_Xref_Table.Last); 897 end Add_SPARK_Xrefs; 898 899 ------------------------- 900 -- Collect_SPARK_Xrefs -- 901 ------------------------- 902 903 procedure Collect_SPARK_Xrefs 904 (Sdep_Table : Unit_Ref_Table; 905 Num_Sdep : Nat) 906 is 907 D1 : Nat; 908 D2 : Nat; 909 910 begin 911 -- Cross-references should have been computed first 912 913 pragma Assert (Xrefs.Last /= 0); 914 915 Initialize_SPARK_Tables; 916 917 -- Generate file and scope SPARK cross-reference information 918 919 D1 := 1; 920 while D1 <= Num_Sdep loop 921 922 -- In rare cases, when treating the library-level instantiation of a 923 -- generic, two consecutive units refer to the same compilation unit 924 -- node and entity. In that case, treat them as a single unit for the 925 -- sake of SPARK cross references by passing to Add_SPARK_File. 926 927 if D1 < Num_Sdep 928 and then Cunit_Entity (Sdep_Table (D1)) = 929 Cunit_Entity (Sdep_Table (D1 + 1)) 930 then 931 D2 := D1 + 1; 932 else 933 D2 := D1; 934 end if; 935 936 -- Some files do not correspond to Ada units, and as such present no 937 -- interest for SPARK cross references. Skip these files, as printing 938 -- their name may require printing the full name with spaces, which 939 -- is not handled in the code doing I/O of SPARK cross references. 940 941 if Present (Cunit_Entity (Sdep_Table (D1))) then 942 Add_SPARK_File 943 (Ubody => Sdep_Table (D1), 944 Uspec => Sdep_Table (D2), 945 Dspec => D2); 946 end if; 947 948 D1 := D2 + 1; 949 end loop; 950 951 -- Fill in the spec information when relevant 952 953 declare 954 package Entity_Hash_Table is new 955 GNAT.HTable.Simple_HTable 956 (Header_Num => Entity_Hashed_Range, 957 Element => Scope_Index, 958 No_Element => 0, 959 Key => Entity_Id, 960 Hash => Entity_Hash, 961 Equal => "="); 962 963 begin 964 -- Fill in the hash-table 965 966 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 967 declare 968 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); 969 begin 970 Entity_Hash_Table.Set (Srec.Scope_Entity, S); 971 end; 972 end loop; 973 974 -- Use the hash-table to locate spec entities 975 976 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 977 declare 978 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); 979 980 Spec_Entity : constant Entity_Id := 981 Unique_Entity (Srec.Scope_Entity); 982 Spec_Scope : constant Scope_Index := 983 Entity_Hash_Table.Get (Spec_Entity); 984 985 begin 986 -- Generic spec may be missing in which case Spec_Scope is zero 987 988 if Spec_Entity /= Srec.Scope_Entity 989 and then Spec_Scope /= 0 990 then 991 Srec.Spec_File_Num := 992 SPARK_Scope_Table.Table (Spec_Scope).File_Num; 993 Srec.Spec_Scope_Num := 994 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num; 995 end if; 996 end; 997 end loop; 998 end; 999 1000 -- Generate SPARK cross-reference information 1001 1002 Add_SPARK_Xrefs; 1003 end Collect_SPARK_Xrefs; 1004 1005 -------------------------------- 1006 -- Detect_And_Add_SPARK_Scope -- 1007 -------------------------------- 1008 1009 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is 1010 begin 1011 if Nkind_In (N, N_Entry_Body, -- entries 1012 N_Entry_Declaration) 1013 or else 1014 Nkind_In (N, N_Package_Body, -- packages 1015 N_Package_Body_Stub, 1016 N_Package_Declaration) 1017 or else 1018 Nkind_In (N, N_Subprogram_Body, -- subprograms 1019 N_Subprogram_Body_Stub, 1020 N_Subprogram_Declaration) 1021 or else 1022 Nkind_In (N, N_Task_Body, -- tasks 1023 N_Task_Body_Stub) 1024 then 1025 Add_SPARK_Scope (N); 1026 end if; 1027 end Detect_And_Add_SPARK_Scope; 1028 1029 ------------------------------------- 1030 -- Enclosing_Subprogram_Or_Package -- 1031 ------------------------------------- 1032 1033 function Enclosing_Subprogram_Or_Library_Package 1034 (N : Node_Id) return Entity_Id 1035 is 1036 Result : Entity_Id; 1037 1038 begin 1039 -- If N is the defining identifier for a subprogram, then return the 1040 -- enclosing subprogram or package, not this subprogram. 1041 1042 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) 1043 and then Nkind (Parent (N)) in N_Subprogram_Specification 1044 then 1045 Result := Parent (Parent (Parent (N))); 1046 1047 -- If this was a library-level subprogram then replace Result with 1048 -- its Unit, which points to N_Subprogram_* node. 1049 1050 if Nkind (Result) = N_Compilation_Unit then 1051 Result := Unit (Result); 1052 end if; 1053 else 1054 Result := N; 1055 end if; 1056 1057 while Present (Result) loop 1058 case Nkind (Result) is 1059 when N_Package_Specification => 1060 1061 -- Only return a library-level package 1062 1063 if Is_Library_Level_Entity (Defining_Entity (Result)) then 1064 Result := Defining_Entity (Result); 1065 exit; 1066 else 1067 Result := Parent (Result); 1068 end if; 1069 1070 when N_Package_Body => 1071 1072 -- Only return a library-level package 1073 1074 if Is_Library_Level_Entity (Defining_Entity (Result)) then 1075 Result := Defining_Entity (Result); 1076 exit; 1077 else 1078 Result := Parent (Result); 1079 end if; 1080 1081 when N_Subprogram_Specification => 1082 Result := Defining_Unit_Name (Result); 1083 exit; 1084 1085 when N_Subprogram_Declaration => 1086 Result := Defining_Unit_Name (Specification (Result)); 1087 exit; 1088 1089 when N_Subprogram_Body => 1090 Result := Defining_Unit_Name (Specification (Result)); 1091 exit; 1092 1093 when N_Pragma => 1094 1095 -- The enclosing subprogram for a precondition, postcondition, 1096 -- or contract case should be the declaration preceding the 1097 -- pragma (skipping any other pragmas between this pragma and 1098 -- this declaration. 1099 1100 while Nkind (Result) = N_Pragma 1101 and then Is_List_Member (Result) 1102 and then Present (Prev (Result)) 1103 loop 1104 Result := Prev (Result); 1105 end loop; 1106 1107 if Nkind (Result) = N_Pragma then 1108 Result := Parent (Result); 1109 end if; 1110 1111 when N_Entry_Body => 1112 Result := Defining_Identifier (Result); 1113 exit; 1114 1115 when N_Task_Body => 1116 Result := Defining_Identifier (Result); 1117 exit; 1118 1119 when others => 1120 Result := Parent (Result); 1121 end case; 1122 end loop; 1123 1124 if Nkind (Result) = N_Defining_Program_Unit_Name then 1125 Result := Defining_Identifier (Result); 1126 end if; 1127 1128 -- Do not return a scope without a proper location 1129 1130 if Present (Result) 1131 and then Sloc (Result) = No_Location 1132 then 1133 return Empty; 1134 end if; 1135 1136 return Result; 1137 end Enclosing_Subprogram_Or_Library_Package; 1138 1139 ----------------- 1140 -- Entity_Hash -- 1141 ----------------- 1142 1143 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is 1144 begin 1145 return 1146 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1)); 1147 end Entity_Hash; 1148 1149 -------------------------- 1150 -- Generate_Dereference -- 1151 -------------------------- 1152 1153 procedure Generate_Dereference 1154 (N : Node_Id; 1155 Typ : Character := 'r') 1156 is 1157 procedure Create_Heap; 1158 -- Create and decorate the special entity which denotes the heap 1159 1160 ----------------- 1161 -- Create_Heap -- 1162 ----------------- 1163 1164 procedure Create_Heap is 1165 begin 1166 Name_Len := Name_Of_Heap_Variable'Length; 1167 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable; 1168 1169 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter); 1170 1171 Set_Ekind (Heap, E_Variable); 1172 Set_Is_Internal (Heap, True); 1173 Set_Has_Fully_Qualified_Name (Heap); 1174 end Create_Heap; 1175 1176 -- Local variables 1177 1178 Loc : constant Source_Ptr := Sloc (N); 1179 Index : Nat; 1180 Ref_Scope : Entity_Id; 1181 1182 -- Start of processing for Generate_Dereference 1183 1184 begin 1185 1186 if Loc > No_Location then 1187 Drefs.Increment_Last; 1188 Index := Drefs.Last; 1189 1190 declare 1191 Deref_Entry : Xref_Entry renames Drefs.Table (Index); 1192 Deref : Xref_Key renames Deref_Entry.Key; 1193 1194 begin 1195 if No (Heap) then 1196 Create_Heap; 1197 end if; 1198 1199 Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N); 1200 1201 Deref.Ent := Heap; 1202 Deref.Loc := Loc; 1203 Deref.Typ := Typ; 1204 1205 -- It is as if the special "Heap" was defined in every scope where 1206 -- it is referenced. 1207 1208 Deref.Eun := Get_Code_Unit (Loc); 1209 Deref.Lun := Get_Code_Unit (Loc); 1210 1211 Deref.Ref_Scope := Ref_Scope; 1212 Deref.Ent_Scope := Ref_Scope; 1213 1214 Deref_Entry.Def := No_Location; 1215 1216 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N); 1217 end; 1218 end if; 1219 end Generate_Dereference; 1220 1221 ------------------------------- 1222 -- Traverse_Compilation_Unit -- 1223 ------------------------------- 1224 1225 procedure Traverse_Compilation_Unit 1226 (CU : Node_Id; 1227 Process : Node_Processing; 1228 Inside_Stubs : Boolean) 1229 is 1230 Lu : Node_Id; 1231 1232 begin 1233 -- Get Unit (checking case of subunit) 1234 1235 Lu := Unit (CU); 1236 1237 if Nkind (Lu) = N_Subunit then 1238 Lu := Proper_Body (Lu); 1239 end if; 1240 1241 -- Do not add scopes for generic units 1242 1243 if Nkind (Lu) = N_Package_Body 1244 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind 1245 then 1246 return; 1247 end if; 1248 1249 -- Call Process on all declarations 1250 1251 if Nkind (Lu) in N_Declaration 1252 or else Nkind (Lu) in N_Later_Decl_Item 1253 then 1254 Process (Lu); 1255 end if; 1256 1257 -- Traverse the unit 1258 1259 Traverse_Declaration_Or_Statement (Lu, Process, Inside_Stubs); 1260 end Traverse_Compilation_Unit; 1261 1262 --------------------------------------- 1263 -- Traverse_Declaration_Or_Statement -- 1264 --------------------------------------- 1265 1266 procedure Traverse_Declaration_Or_Statement 1267 (N : Node_Id; 1268 Process : Node_Processing; 1269 Inside_Stubs : Boolean) 1270 is 1271 begin 1272 case Nkind (N) is 1273 when N_Package_Declaration => 1274 declare 1275 Spec : constant Node_Id := Specification (N); 1276 begin 1277 Traverse_Declarations_Or_Statements 1278 (Visible_Declarations (Spec), Process, Inside_Stubs); 1279 Traverse_Declarations_Or_Statements 1280 (Private_Declarations (Spec), Process, Inside_Stubs); 1281 end; 1282 1283 when N_Package_Body => 1284 if Ekind (Defining_Entity (N)) /= E_Generic_Package then 1285 Traverse_Package_Body (N, Process, Inside_Stubs); 1286 end if; 1287 1288 when N_Package_Body_Stub => 1289 if Present (Library_Unit (N)) then 1290 declare 1291 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1292 begin 1293 if Inside_Stubs 1294 and then 1295 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package 1296 then 1297 Traverse_Package_Body (Body_N, Process, Inside_Stubs); 1298 end if; 1299 end; 1300 end if; 1301 1302 when N_Subprogram_Declaration => 1303 null; 1304 1305 when N_Entry_Body | N_Subprogram_Body => 1306 if not Is_Generic_Subprogram (Defining_Entity (N)) then 1307 Traverse_Subprogram_Body (N, Process, Inside_Stubs); 1308 end if; 1309 1310 when N_Subprogram_Body_Stub => 1311 if Present (Library_Unit (N)) then 1312 declare 1313 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1314 begin 1315 if Inside_Stubs 1316 and then 1317 not Is_Generic_Subprogram (Defining_Entity (Body_N)) 1318 then 1319 Traverse_Subprogram_Body (Body_N, Process, Inside_Stubs); 1320 end if; 1321 end; 1322 end if; 1323 1324 when N_Protected_Body => 1325 Traverse_Protected_Body (N, Process, Inside_Stubs); 1326 1327 when N_Protected_Body_Stub => 1328 if Present (Library_Unit (N)) then 1329 declare 1330 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1331 begin 1332 if Inside_Stubs then 1333 Traverse_Declarations_Or_Statements 1334 (Declarations (Body_N), Process, Inside_Stubs); 1335 end if; 1336 end; 1337 end if; 1338 1339 when N_Protected_Type_Declaration | N_Single_Protected_Declaration => 1340 declare 1341 Def : constant Node_Id := Protected_Definition (N); 1342 begin 1343 Traverse_Declarations_Or_Statements 1344 (Visible_Declarations (Def), Process, Inside_Stubs); 1345 Traverse_Declarations_Or_Statements 1346 (Private_Declarations (Def), Process, Inside_Stubs); 1347 end; 1348 1349 when N_Task_Definition => 1350 Traverse_Declarations_Or_Statements 1351 (Visible_Declarations (N), Process, Inside_Stubs); 1352 Traverse_Declarations_Or_Statements 1353 (Private_Declarations (N), Process, Inside_Stubs); 1354 1355 when N_Task_Body => 1356 Traverse_Declarations_Or_Statements 1357 (Declarations (N), Process, Inside_Stubs); 1358 Traverse_Handled_Statement_Sequence 1359 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1360 1361 when N_Task_Body_Stub => 1362 if Present (Library_Unit (N)) then 1363 declare 1364 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1365 begin 1366 if Inside_Stubs then 1367 Traverse_Declarations_Or_Statements 1368 (Declarations (Body_N), Process, Inside_Stubs); 1369 Traverse_Handled_Statement_Sequence 1370 (Handled_Statement_Sequence (Body_N), Process, 1371 Inside_Stubs); 1372 end if; 1373 end; 1374 end if; 1375 1376 when N_Block_Statement => 1377 Traverse_Declarations_Or_Statements 1378 (Declarations (N), Process, Inside_Stubs); 1379 Traverse_Handled_Statement_Sequence 1380 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1381 1382 when N_If_Statement => 1383 1384 -- Traverse the statements in the THEN part 1385 1386 Traverse_Declarations_Or_Statements 1387 (Then_Statements (N), Process, Inside_Stubs); 1388 1389 -- Loop through ELSIF parts if present 1390 1391 if Present (Elsif_Parts (N)) then 1392 declare 1393 Elif : Node_Id := First (Elsif_Parts (N)); 1394 1395 begin 1396 while Present (Elif) loop 1397 Traverse_Declarations_Or_Statements 1398 (Then_Statements (Elif), Process, Inside_Stubs); 1399 Next (Elif); 1400 end loop; 1401 end; 1402 end if; 1403 1404 -- Finally traverse the ELSE statements if present 1405 1406 Traverse_Declarations_Or_Statements 1407 (Else_Statements (N), Process, Inside_Stubs); 1408 1409 when N_Case_Statement => 1410 1411 -- Process case branches 1412 1413 declare 1414 Alt : Node_Id; 1415 begin 1416 Alt := First (Alternatives (N)); 1417 while Present (Alt) loop 1418 Traverse_Declarations_Or_Statements 1419 (Statements (Alt), Process, Inside_Stubs); 1420 Next (Alt); 1421 end loop; 1422 end; 1423 1424 when N_Extended_Return_Statement => 1425 Traverse_Handled_Statement_Sequence 1426 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1427 1428 when N_Loop_Statement => 1429 Traverse_Declarations_Or_Statements 1430 (Statements (N), Process, Inside_Stubs); 1431 1432 -- Generic declarations are ignored 1433 1434 when others => 1435 null; 1436 end case; 1437 end Traverse_Declaration_Or_Statement; 1438 1439 ----------------------------------------- 1440 -- Traverse_Declarations_Or_Statements -- 1441 ----------------------------------------- 1442 1443 procedure Traverse_Declarations_Or_Statements 1444 (L : List_Id; 1445 Process : Node_Processing; 1446 Inside_Stubs : Boolean) 1447 is 1448 N : Node_Id; 1449 1450 begin 1451 -- Loop through statements or declarations 1452 1453 N := First (L); 1454 while Present (N) loop 1455 -- Call Process on all declarations 1456 1457 if Nkind (N) in N_Declaration 1458 or else 1459 Nkind (N) in N_Later_Decl_Item 1460 or else 1461 Nkind (N) = N_Entry_Body 1462 then 1463 Process (N); 1464 end if; 1465 1466 Traverse_Declaration_Or_Statement (N, Process, Inside_Stubs); 1467 1468 Next (N); 1469 end loop; 1470 end Traverse_Declarations_Or_Statements; 1471 1472 ----------------------------------------- 1473 -- Traverse_Handled_Statement_Sequence -- 1474 ----------------------------------------- 1475 1476 procedure Traverse_Handled_Statement_Sequence 1477 (N : Node_Id; 1478 Process : Node_Processing; 1479 Inside_Stubs : Boolean) 1480 is 1481 Handler : Node_Id; 1482 1483 begin 1484 if Present (N) then 1485 Traverse_Declarations_Or_Statements 1486 (Statements (N), Process, Inside_Stubs); 1487 1488 if Present (Exception_Handlers (N)) then 1489 Handler := First (Exception_Handlers (N)); 1490 while Present (Handler) loop 1491 Traverse_Declarations_Or_Statements 1492 (Statements (Handler), Process, Inside_Stubs); 1493 Next (Handler); 1494 end loop; 1495 end if; 1496 end if; 1497 end Traverse_Handled_Statement_Sequence; 1498 1499 --------------------------- 1500 -- Traverse_Package_Body -- 1501 --------------------------- 1502 1503 procedure Traverse_Package_Body 1504 (N : Node_Id; 1505 Process : Node_Processing; 1506 Inside_Stubs : Boolean) is 1507 begin 1508 Traverse_Declarations_Or_Statements 1509 (Declarations (N), Process, Inside_Stubs); 1510 Traverse_Handled_Statement_Sequence 1511 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1512 end Traverse_Package_Body; 1513 1514 ----------------------------- 1515 -- Traverse_Protected_Body -- 1516 ----------------------------- 1517 1518 procedure Traverse_Protected_Body 1519 (N : Node_Id; 1520 Process : Node_Processing; 1521 Inside_Stubs : Boolean) is 1522 begin 1523 Traverse_Declarations_Or_Statements 1524 (Declarations (N), Process, Inside_Stubs); 1525 end Traverse_Protected_Body; 1526 1527 ------------------------------ 1528 -- Traverse_Subprogram_Body -- 1529 ------------------------------ 1530 1531 procedure Traverse_Subprogram_Body 1532 (N : Node_Id; 1533 Process : Node_Processing; 1534 Inside_Stubs : Boolean) 1535 is 1536 begin 1537 Traverse_Declarations_Or_Statements 1538 (Declarations (N), Process, Inside_Stubs); 1539 Traverse_Handled_Statement_Sequence 1540 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1541 end Traverse_Subprogram_Body; 1542 1543end SPARK_Specific; 1544