gcc/ada/lib-xref-spark_specific.adb

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