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          Add_SPARK_File
 893            (Ubody => Sdep_Table (D1),
 894             Uspec => Sdep_Table (D2),
 895             Dspec => D2);
 896          D1 := D2 + 1;
 897       end loop;
 898
 899       --  Fill in the spec information when relevant
 900
 901       declare
 902          package Entity_Hash_Table is new
 903            GNAT.HTable.Simple_HTable
 904              (Header_Num => Entity_Hashed_Range,
 905               Element    => Scope_Index,
 906               No_Element => 0,
 907               Key        => Entity_Id,
 908               Hash       => Entity_Hash,
 909               Equal      => "=");
 910
 911       begin
 912          --  Fill in the hash-table
 913
 914          for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
 915             declare
 916                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
 917             begin
 918                Entity_Hash_Table.Set (Srec.Scope_Entity, S);
 919             end;
 920          end loop;
 921
 922          --  Use the hash-table to locate spec entities
 923
 924          for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
 925             declare
 926                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
 927
 928                Spec_Entity : constant Entity_Id :=
 929                                Unique_Entity (Srec.Scope_Entity);
 930                Spec_Scope  : constant Scope_Index :=
 931                                Entity_Hash_Table.Get (Spec_Entity);
 932
 933             begin
 934                --  Generic spec may be missing in which case Spec_Scope is zero
 935
 936                if Spec_Entity /= Srec.Scope_Entity
 937                  and then Spec_Scope /= 0
 938                then
 939                   Srec.Spec_File_Num :=
 940                     SPARK_Scope_Table.Table (Spec_Scope).File_Num;
 941                   Srec.Spec_Scope_Num :=
 942                     SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
 943                end if;
 944             end;
 945          end loop;
 946       end;
 947
 948       --  Generate SPARK cross-reference information
 949
 950       Add_SPARK_Xrefs;
 951    end Collect_SPARK_Xrefs;
 952
 953    --------------------------------
 954    -- Detect_And_Add_SPARK_Scope --
 955    --------------------------------
 956
 957    procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
 958    begin
 959       if Nkind_In (N, N_Subprogram_Declaration,
 960                       N_Subprogram_Body,
 961                       N_Subprogram_Body_Stub,
 962                       N_Package_Declaration,
 963                       N_Package_Body)
 964       then
 965          Add_SPARK_Scope (N);
 966       end if;
 967    end Detect_And_Add_SPARK_Scope;
 968
 969    -------------------------------------
 970    -- Enclosing_Subprogram_Or_Package --
 971    -------------------------------------
 972
 973    function Enclosing_Subprogram_Or_Library_Package
 974      (N : Node_Id) return Entity_Id
 975    is
 976       Result : Entity_Id;
 977
 978    begin
 979       --  If N is the defining identifier for a subprogram, then return the
 980       --  enclosing subprogram or package, not this subprogram.
 981
 982       if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
 983         and then Nkind (Parent (N)) in N_Subprogram_Specification
 984       then
 985          Result := Parent (Parent (Parent (N)));
 986       else
 987          Result := N;
 988       end if;
 989
 990       while Present (Result) loop
 991          case Nkind (Result) is
 992             when N_Package_Specification =>
 993
 994                --  Only return a library-level package
 995
 996                if Is_Library_Level_Entity (Defining_Entity (Result)) then
 997                   Result := Defining_Entity (Result);
 998                   exit;
 999                else
1000                   Result := Parent (Result);
1001                end if;
1002
1003             when N_Package_Body =>
1004
1005                --  Only return a library-level package
1006
1007                if Is_Library_Level_Entity (Defining_Entity (Result)) then
1008                   Result := Defining_Entity (Result);
1009                   exit;
1010                else
1011                   Result := Parent (Result);
1012                end if;
1013
1014             when N_Subprogram_Specification =>
1015                Result := Defining_Unit_Name (Result);
1016                exit;
1017
1018             when N_Subprogram_Declaration =>
1019                Result := Defining_Unit_Name (Specification (Result));
1020                exit;
1021
1022             when N_Subprogram_Body =>
1023                Result := Defining_Unit_Name (Specification (Result));
1024                exit;
1025
1026             when N_Pragma =>
1027
1028                --  The enclosing subprogram for a precondition, postcondition,
1029                --  or contract case should be the declaration preceding the
1030                --  pragma (skipping any other pragmas between this pragma and
1031                --  this declaration.
1032
1033                while Nkind (Result) = N_Pragma
1034                  and then Is_List_Member (Result)
1035                  and then Present (Prev (Result))
1036                loop
1037                   Result := Prev (Result);
1038                end loop;
1039
1040                if Nkind (Result) = N_Pragma then
1041                   Result := Parent (Result);
1042                end if;
1043
1044             when others =>
1045                Result := Parent (Result);
1046          end case;
1047       end loop;
1048
1049       if Nkind (Result) = N_Defining_Program_Unit_Name then
1050          Result := Defining_Identifier (Result);
1051       end if;
1052
1053       --  Do not return a scope without a proper location
1054
1055       if Present (Result)
1056         and then Sloc (Result) = No_Location
1057       then
1058          return Empty;
1059       end if;
1060
1061       return Result;
1062    end Enclosing_Subprogram_Or_Library_Package;
1063
1064    -----------------
1065    -- Entity_Hash --
1066    -----------------
1067
1068    function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1069    begin
1070       return
1071         Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1072    end Entity_Hash;
1073
1074    --------------------------
1075    -- Generate_Dereference --
1076    --------------------------
1077
1078    procedure Generate_Dereference
1079      (N   : Node_Id;
1080       Typ : Character := 'r')
1081    is
1082       procedure Create_Heap;
1083       --  Create and decorate the special entity which denotes the heap
1084
1085       -----------------
1086       -- Create_Heap --
1087       -----------------
1088
1089       procedure Create_Heap is
1090       begin
1091          Name_Len := Name_Of_Heap_Variable'Length;
1092          Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1093
1094          Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1095
1096          Set_Ekind       (Heap, E_Variable);
1097          Set_Is_Internal (Heap, True);
1098          Set_Has_Fully_Qualified_Name (Heap);
1099       end Create_Heap;
1100
1101       --  Local variables
1102
1103       Loc       : constant Source_Ptr := Sloc (N);
1104       Index     : Nat;
1105       Ref_Scope : Entity_Id;
1106
1107    --  Start of processing for Generate_Dereference
1108
1109    begin
1110
1111       if Loc > No_Location then
1112          Drefs.Increment_Last;
1113          Index := Drefs.Last;
1114
1115          declare
1116             Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1117             Deref       : Xref_Key   renames Deref_Entry.Key;
1118
1119          begin
1120             if No (Heap) then
1121                Create_Heap;
1122             end if;
1123
1124             Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1125
1126             Deref.Ent := Heap;
1127             Deref.Loc := Loc;
1128             Deref.Typ := Typ;
1129
1130             --  It is as if the special "Heap" was defined in every scope where
1131             --  it is referenced.
1132
1133             Deref.Eun := Get_Code_Unit (Loc);
1134             Deref.Lun := Get_Code_Unit (Loc);
1135
1136             Deref.Ref_Scope := Ref_Scope;
1137             Deref.Ent_Scope := Ref_Scope;
1138
1139             Deref_Entry.Def := No_Location;
1140
1141             Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1142          end;
1143       end if;
1144    end Generate_Dereference;
1145
1146    ------------------------------------
1147    -- Traverse_All_Compilation_Units --
1148    ------------------------------------
1149
1150    procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1151    begin
1152       for U in Units.First .. Last_Unit loop
1153          Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1154       end loop;
1155    end Traverse_All_Compilation_Units;
1156
1157    -------------------------------
1158    -- Traverse_Compilation_Unit --
1159    -------------------------------
1160
1161    procedure Traverse_Compilation_Unit
1162      (CU           : Node_Id;
1163       Process      : Node_Processing;
1164       Inside_Stubs : Boolean)
1165    is
1166       Lu : Node_Id;
1167
1168    begin
1169       --  Get Unit (checking case of subunit)
1170
1171       Lu := Unit (CU);
1172
1173       if Nkind (Lu) = N_Subunit then
1174          Lu := Proper_Body (Lu);
1175       end if;
1176
1177       --  Do not add scopes for generic units
1178
1179       if Nkind (Lu) = N_Package_Body
1180         and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1181       then
1182          return;
1183       end if;
1184
1185       --  Call Process on all declarations
1186
1187       if Nkind (Lu) in N_Declaration
1188         or else Nkind (Lu) in N_Later_Decl_Item
1189       then
1190          Process (Lu);
1191       end if;
1192
1193       --  Traverse the unit
1194
1195       if Nkind (Lu) = N_Subprogram_Body then
1196          Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1197
1198       elsif Nkind (Lu) = N_Subprogram_Declaration then
1199          null;
1200
1201       elsif Nkind (Lu) = N_Package_Declaration then
1202          Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1203
1204       elsif Nkind (Lu) = N_Package_Body then
1205          Traverse_Package_Body (Lu, Process, Inside_Stubs);
1206
1207       --  All other cases of compilation units (e.g. renamings), are not
1208       --  declarations, or else generic declarations which are ignored.
1209
1210       else
1211          null;
1212       end if;
1213    end Traverse_Compilation_Unit;
1214
1215    -----------------------------------------
1216    -- Traverse_Declarations_Or_Statements --
1217    -----------------------------------------
1218
1219    procedure Traverse_Declarations_Or_Statements
1220      (L            : List_Id;
1221       Process      : Node_Processing;
1222       Inside_Stubs : Boolean)
1223    is
1224       N : Node_Id;
1225
1226    begin
1227       --  Loop through statements or declarations
1228
1229       N := First (L);
1230       while Present (N) loop
1231          --  Call Process on all declarations
1232
1233          if Nkind (N) in N_Declaration
1234               or else
1235             Nkind (N) in N_Later_Decl_Item
1236          then
1237             Process (N);
1238          end if;
1239
1240          case Nkind (N) is
1241
1242             --  Package declaration
1243
1244             when N_Package_Declaration =>
1245                Traverse_Package_Declaration (N, Process, Inside_Stubs);
1246
1247             --  Package body
1248
1249             when N_Package_Body =>
1250                if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1251                   Traverse_Package_Body (N, Process, Inside_Stubs);
1252                end if;
1253
1254             when N_Package_Body_Stub =>
1255                if Present (Library_Unit (N)) then
1256                   declare
1257                      Body_N : constant Node_Id := Get_Body_From_Stub (N);
1258                   begin
1259                      if Inside_Stubs
1260                        and then
1261                          Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1262                      then
1263                         Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1264                      end if;
1265                   end;
1266                end if;
1267
1268             --  Subprogram declaration
1269
1270             when N_Subprogram_Declaration =>
1271                null;
1272
1273             --  Subprogram body
1274
1275             when N_Subprogram_Body =>
1276                if not Is_Generic_Subprogram (Defining_Entity (N)) then
1277                   Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1278                end if;
1279
1280             when N_Subprogram_Body_Stub =>
1281                if Present (Library_Unit (N)) then
1282                   declare
1283                      Body_N : constant Node_Id := Get_Body_From_Stub (N);
1284                   begin
1285                      if Inside_Stubs
1286                        and then
1287                          not Is_Generic_Subprogram (Defining_Entity (Body_N))
1288                      then
1289                         Traverse_Subprogram_Body
1290                           (Body_N, Process, Inside_Stubs);
1291                      end if;
1292                   end;
1293                end if;
1294
1295             --  Block statement
1296
1297             when N_Block_Statement =>
1298                Traverse_Declarations_Or_Statements
1299                  (Declarations (N), Process, Inside_Stubs);
1300                Traverse_Handled_Statement_Sequence
1301                  (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1302
1303             when N_If_Statement =>
1304
1305                --  Traverse the statements in the THEN part
1306
1307                Traverse_Declarations_Or_Statements
1308                  (Then_Statements (N), Process, Inside_Stubs);
1309
1310                --  Loop through ELSIF parts if present
1311
1312                if Present (Elsif_Parts (N)) then
1313                   declare
1314                      Elif : Node_Id := First (Elsif_Parts (N));
1315
1316                   begin
1317                      while Present (Elif) loop
1318                         Traverse_Declarations_Or_Statements
1319                           (Then_Statements (Elif), Process, Inside_Stubs);
1320                         Next (Elif);
1321                      end loop;
1322                   end;
1323                end if;
1324
1325                --  Finally traverse the ELSE statements if present
1326
1327                Traverse_Declarations_Or_Statements
1328                  (Else_Statements (N), Process, Inside_Stubs);
1329
1330             --  Case statement
1331
1332             when N_Case_Statement =>
1333
1334                --  Process case branches
1335
1336                declare
1337                   Alt : Node_Id;
1338                begin
1339                   Alt := First (Alternatives (N));
1340                   while Present (Alt) loop
1341                      Traverse_Declarations_Or_Statements
1342                        (Statements (Alt), Process, Inside_Stubs);
1343                      Next (Alt);
1344                   end loop;
1345                end;
1346
1347             --  Extended return statement
1348
1349             when N_Extended_Return_Statement =>
1350                Traverse_Handled_Statement_Sequence
1351                  (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1352
1353             --  Loop
1354
1355             when N_Loop_Statement =>
1356                Traverse_Declarations_Or_Statements
1357                  (Statements (N), Process, Inside_Stubs);
1358
1359             --  Generic declarations are ignored
1360
1361             when others =>
1362                null;
1363          end case;
1364
1365          Next (N);
1366       end loop;
1367    end Traverse_Declarations_Or_Statements;
1368
1369    -----------------------------------------
1370    -- Traverse_Handled_Statement_Sequence --
1371    -----------------------------------------
1372
1373    procedure Traverse_Handled_Statement_Sequence
1374      (N            : Node_Id;
1375       Process      : Node_Processing;
1376       Inside_Stubs : Boolean)
1377    is
1378       Handler : Node_Id;
1379
1380    begin
1381       if Present (N) then
1382          Traverse_Declarations_Or_Statements
1383            (Statements (N), Process, Inside_Stubs);
1384
1385          if Present (Exception_Handlers (N)) then
1386             Handler := First (Exception_Handlers (N));
1387             while Present (Handler) loop
1388                Traverse_Declarations_Or_Statements
1389                  (Statements (Handler), Process, Inside_Stubs);
1390                Next (Handler);
1391             end loop;
1392          end if;
1393       end if;
1394    end Traverse_Handled_Statement_Sequence;
1395
1396    ---------------------------
1397    -- Traverse_Package_Body --
1398    ---------------------------
1399
1400    procedure Traverse_Package_Body
1401      (N            : Node_Id;
1402       Process      : Node_Processing;
1403       Inside_Stubs : Boolean) is
1404    begin
1405       Traverse_Declarations_Or_Statements
1406         (Declarations (N), Process, Inside_Stubs);
1407       Traverse_Handled_Statement_Sequence
1408         (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1409    end Traverse_Package_Body;
1410
1411    ----------------------------------
1412    -- Traverse_Package_Declaration --
1413    ----------------------------------
1414
1415    procedure Traverse_Package_Declaration
1416      (N            : Node_Id;
1417       Process      : Node_Processing;
1418       Inside_Stubs : Boolean)
1419    is
1420       Spec : constant Node_Id := Specification (N);
1421    begin
1422       Traverse_Declarations_Or_Statements
1423         (Visible_Declarations (Spec), Process, Inside_Stubs);
1424       Traverse_Declarations_Or_Statements
1425         (Private_Declarations (Spec), Process, Inside_Stubs);
1426    end Traverse_Package_Declaration;
1427
1428    ------------------------------
1429    -- Traverse_Subprogram_Body --
1430    ------------------------------
1431
1432    procedure Traverse_Subprogram_Body
1433      (N            : Node_Id;
1434       Process      : Node_Processing;
1435       Inside_Stubs : Boolean)
1436    is
1437    begin
1438       Traverse_Declarations_Or_Statements
1439         (Declarations (N), Process, Inside_Stubs);
1440       Traverse_Handled_Statement_Sequence
1441         (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1442    end Traverse_Subprogram_Body;
1443
1444 end SPARK_Specific;