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