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 Is_Global_Constant (E : Entity_Id) return Boolean;
 338       --  Return True if E is a global constant for which we should ignore
 339       --  reads in SPARK.
 340
 341       function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
 342       --  Comparison function for Sort call
 343
 344       procedure Move (From : Natural; To : Natural);
 345       --  Move procedure for Sort call
 346
 347       procedure Update_Scope_Range
 348         (S    : Scope_Index;
 349          From : Xref_Index;
 350          To   : Xref_Index);
 351       --  Update the scope which maps to S with the new range From .. To
 352
 353       package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
 354
 355       function Get_Scope_Num (N : Entity_Id) return Nat;
 356       --  Return the scope number associated to entity N
 357
 358       procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
 359       --  Associate entity N to scope number Num
 360
 361       No_Scope : constant Nat := 0;
 362       --  Initial scope counter
 363
 364       type Scope_Rec is record
 365          Num    : Nat;
 366          Entity : Entity_Id;
 367       end record;
 368       --  Type used to relate an entity and a scope number
 369
 370       package Scopes is new GNAT.HTable.Simple_HTable
 371         (Header_Num => Entity_Hashed_Range,
 372          Element    => Scope_Rec,
 373          No_Element => (Num => No_Scope, Entity => Empty),
 374          Key        => Entity_Id,
 375          Hash       => Entity_Hash,
 376          Equal      => "=");
 377       --  Package used to build a correspondance between entities and scope
 378       --  numbers used in SPARK cross references.
 379
 380       Nrefs : Nat := Xrefs.Last;
 381       --  Number of references in table. This value may get reset (reduced)
 382       --  when we eliminate duplicate reference entries as well as references
 383       --  not suitable for local cross-references.
 384
 385       Nrefs_Add : constant Nat := Drefs.Last;
 386       --  Number of additional references which correspond to dereferences in
 387       --  the source code.
 388
 389       Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
 390       --  This array contains numbers of references in the Xrefs table. This
 391       --  list is sorted in output order. The extra 0'th entry is convenient
 392       --  for the call to sort. When we sort the table, we move the entries in
 393       --  Rnums around, but we do not move the original table entries.
 394
 395       ---------------------
 396       -- Entity_Of_Scope --
 397       ---------------------
 398
 399       function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
 400       begin
 401          return SPARK_Scope_Table.Table (S).Scope_Entity;
 402       end Entity_Of_Scope;
 403
 404       ---------------------
 405       -- Get_Entity_Type --
 406       ---------------------
 407
 408       function Get_Entity_Type (E : Entity_Id) return Character is
 409       begin
 410          case Ekind (E) is
 411             when E_Out_Parameter    => return '<';
 412             when E_In_Out_Parameter => return '=';
 413             when E_In_Parameter     => return '>';
 414             when others             => return '*';
 415          end case;
 416       end Get_Entity_Type;
 417
 418       -------------------
 419       -- Get_Scope_Num --
 420       -------------------
 421
 422       function Get_Scope_Num (N : Entity_Id) return Nat is
 423       begin
 424          return Scopes.Get (N).Num;
 425       end Get_Scope_Num;
 426
 427       ------------------------
 428       -- Is_SPARK_Reference --
 429       ------------------------
 430
 431       function Is_SPARK_Reference
 432         (E   : Entity_Id;
 433          Typ : Character) return Boolean
 434       is
 435       begin
 436          --  The only references of interest on callable entities are calls. On
 437          --  non-callable entities, the only references of interest are reads
 438          --  and writes.
 439
 440          if Ekind (E) in Overloadable_Kind then
 441             return Typ = 's';
 442
 443          --  References to constant objects are not considered in SPARK
 444          --  section, as these will be translated as constants in the
 445          --  intermediate language for formal verification, and should
 446          --  therefore never appear in frame conditions.
 447
 448          elsif Is_Constant_Object (E) then
 449             return False;
 450
 451          --  Objects of Task type or protected type are not SPARK references
 452
 453          elsif Present (Etype (E))
 454            and then Ekind (Etype (E)) in Concurrent_Kind
 455          then
 456             return False;
 457
 458          --  In all other cases, result is true for reference/modify cases,
 459          --  and false for all other cases.
 460
 461          else
 462             return Typ = 'r' or else Typ = 'm';
 463          end if;
 464       end Is_SPARK_Reference;
 465
 466       --------------------
 467       -- Is_SPARK_Scope --
 468       --------------------
 469
 470       function Is_SPARK_Scope (E : Entity_Id) return Boolean is
 471       begin
 472          return Present (E)
 473            and then not Is_Generic_Unit (E)
 474            and then Renamed_Entity (E) = Empty
 475            and then Get_Scope_Num (E) /= No_Scope;
 476       end Is_SPARK_Scope;
 477
 478       ----------------------------
 479       -- Is_Future_Scope_Entity --
 480       ----------------------------
 481
 482       function Is_Future_Scope_Entity
 483         (E : Entity_Id;
 484          S : Scope_Index) return Boolean
 485       is
 486          function Is_Past_Scope_Entity return Boolean;
 487          --  Check whether entity E is in SPARK_Scope_Table at index strictly
 488          --  lower than S.
 489
 490          --------------------------
 491          -- Is_Past_Scope_Entity --
 492          --------------------------
 493
 494          function Is_Past_Scope_Entity return Boolean is
 495          begin
 496             for Index in SPARK_Scope_Table.First .. S - 1 loop
 497                if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
 498                   declare
 499                      Dummy : constant SPARK_Scope_Record :=
 500                                SPARK_Scope_Table.Table (Index);
 501                      pragma Unreferenced (Dummy);
 502                   begin
 503                      return True;
 504                   end;
 505                end if;
 506             end loop;
 507
 508             return False;
 509          end Is_Past_Scope_Entity;
 510
 511       --  Start of processing for Is_Future_Scope_Entity
 512
 513       begin
 514          for Index in S .. SPARK_Scope_Table.Last loop
 515             if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
 516                return True;
 517             end if;
 518          end loop;
 519
 520          --  If this assertion fails, this means that the scope which we are
 521          --  looking for has been treated already, which reveals a problem in
 522          --  the order of cross-references.
 523
 524          pragma Assert (not Is_Past_Scope_Entity);
 525
 526          return False;
 527       end Is_Future_Scope_Entity;
 528
 529       ------------------------
 530       -- Is_Global_Constant --
 531       ------------------------
 532
 533       function Is_Global_Constant (E : Entity_Id) return Boolean is
 534       begin
 535          return Ekind (E) = E_Constant
 536            and then Ekind_In (Scope (E), E_Package, E_Package_Body);
 537       end Is_Global_Constant;
 538
 539       --------
 540       -- Lt --
 541       --------
 542
 543       function Lt (Op1, Op2 : Natural) return Boolean is
 544          T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
 545          T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
 546
 547       begin
 548          --  First test: if entity is in different unit, sort by unit. Note:
 549          --  that we use Ent_Scope_File rather than Eun, as Eun may refer to
 550          --  the file where the generic scope is defined, which may differ from
 551          --  the file where the enclosing scope is defined. It is the latter
 552          --  which matters for a correct order here.
 553
 554          if T1.Ent_Scope_File /= T2.Ent_Scope_File then
 555             return Dependency_Num (T1.Ent_Scope_File) <
 556                    Dependency_Num (T2.Ent_Scope_File);
 557
 558          --  Second test: within same unit, sort by location of the scope of
 559          --  the entity definition.
 560
 561          elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
 562                Get_Scope_Num (T2.Key.Ent_Scope)
 563          then
 564             return Get_Scope_Num (T1.Key.Ent_Scope) <
 565                    Get_Scope_Num (T2.Key.Ent_Scope);
 566
 567          --  Third test: within same unit and scope, sort by location of
 568          --  entity definition.
 569
 570          elsif T1.Def /= T2.Def then
 571             return T1.Def < T2.Def;
 572
 573          else
 574             --  Both entities must be equal at this point
 575
 576             pragma Assert (T1.Key.Ent = T2.Key.Ent);
 577
 578             --  Fourth test: if reference is in same unit as entity definition,
 579             --  sort first.
 580
 581             if T1.Key.Lun /= T2.Key.Lun
 582               and then T1.Ent_Scope_File = T1.Key.Lun
 583             then
 584                return True;
 585
 586             elsif T1.Key.Lun /= T2.Key.Lun
 587               and then T2.Ent_Scope_File = T2.Key.Lun
 588             then
 589                return False;
 590
 591             --  Fifth test: if reference is in same unit and same scope as
 592             --  entity definition, sort first.
 593
 594             elsif T1.Ent_Scope_File = T1.Key.Lun
 595               and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
 596               and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
 597             then
 598                return True;
 599
 600             elsif T2.Ent_Scope_File = T2.Key.Lun
 601               and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
 602               and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
 603             then
 604                return False;
 605
 606             --  Sixth test: for same entity, sort by reference location unit
 607
 608             elsif T1.Key.Lun /= T2.Key.Lun then
 609                return Dependency_Num (T1.Key.Lun) <
 610                       Dependency_Num (T2.Key.Lun);
 611
 612             --  Seventh test: for same entity, sort by reference location scope
 613
 614             elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
 615                   Get_Scope_Num (T2.Key.Ref_Scope)
 616             then
 617                return Get_Scope_Num (T1.Key.Ref_Scope) <
 618                       Get_Scope_Num (T2.Key.Ref_Scope);
 619
 620             --  Eighth test: order of location within referencing unit
 621
 622             elsif T1.Key.Loc /= T2.Key.Loc then
 623                return T1.Key.Loc < T2.Key.Loc;
 624
 625             --  Finally, for two locations at the same address prefer the one
 626             --  that does NOT have the type 'r', so that a modification or
 627             --  extension takes preference, when there are more than one
 628             --  reference at the same location. As a result, in the case of
 629             --  entities that are in-out actuals, the read reference follows
 630             --  the modify reference.
 631
 632             else
 633                return T2.Key.Typ = 'r';
 634             end if;
 635          end if;
 636       end Lt;
 637
 638       ----------
 639       -- Move --
 640       ----------
 641
 642       procedure Move (From : Natural; To : Natural) is
 643       begin
 644          Rnums (Nat (To)) := Rnums (Nat (From));
 645       end Move;
 646
 647       -------------------
 648       -- Set_Scope_Num --
 649       -------------------
 650
 651       procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
 652       begin
 653          Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N));
 654       end Set_Scope_Num;
 655
 656       ------------------------
 657       -- Update_Scope_Range --
 658       ------------------------
 659
 660       procedure Update_Scope_Range
 661         (S    : Scope_Index;
 662          From : Xref_Index;
 663          To   : Xref_Index)
 664       is
 665       begin
 666          SPARK_Scope_Table.Table (S).From_Xref := From;
 667          SPARK_Scope_Table.Table (S).To_Xref := To;
 668       end Update_Scope_Range;
 669
 670       --  Local variables
 671
 672       Col        : Nat;
 673       From_Index : Xref_Index;
 674       Line       : Nat;
 675       Loc        : Source_Ptr;
 676       Prev_Typ   : Character;
 677       Ref_Count  : Nat;
 678       Ref_Id     : Entity_Id;
 679       Ref_Name   : String_Ptr;
 680       Scope_Id   : Scope_Index;
 681
 682    --  Start of processing for Add_SPARK_Xrefs
 683
 684    begin
 685       for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
 686          declare
 687             S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
 688          begin
 689             Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
 690          end;
 691       end loop;
 692
 693       --  Set up the pointer vector for the sort
 694
 695       for Index in 1 .. Nrefs loop
 696          Rnums (Index) := Index;
 697       end loop;
 698
 699       for Index in Drefs.First .. Drefs.Last loop
 700          Xrefs.Append (Drefs.Table (Index));
 701
 702          Nrefs         := Nrefs + 1;
 703          Rnums (Nrefs) := Xrefs.Last;
 704       end loop;
 705
 706       --  Capture the definition Sloc values. As in the case of normal cross
 707       --  references, we have to wait until now to get the correct value.
 708
 709       for Index in 1 .. Nrefs loop
 710          Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
 711       end loop;
 712
 713       --  Eliminate entries not appropriate for SPARK. Done prior to sorting
 714       --  cross-references, as it discards useless references which do not have
 715       --  a proper format for the comparison function (like no location).
 716
 717       Ref_Count := Nrefs;
 718       Nrefs     := 0;
 719
 720       for Index in 1 .. Ref_Count loop
 721          declare
 722             Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
 723
 724          begin
 725             if SPARK_Entities (Ekind (Ref.Ent))
 726               and then SPARK_References (Ref.Typ)
 727               and then Is_SPARK_Scope (Ref.Ent_Scope)
 728               and then Is_SPARK_Scope (Ref.Ref_Scope)
 729               and then not Is_Global_Constant (Ref.Ent)
 730               and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
 731
 732               --  Discard references from unknown scopes, e.g. generic scopes
 733
 734               and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
 735               and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
 736             then
 737                Nrefs         := Nrefs + 1;
 738                Rnums (Nrefs) := Rnums (Index);
 739             end if;
 740          end;
 741       end loop;
 742
 743       --  Sort the references
 744
 745       Sorting.Sort (Integer (Nrefs));
 746
 747       --  Eliminate duplicate entries
 748
 749       --  We need this test for Ref_Count because if we force ALI file
 750       --  generation in case of errors detected, it may be the case that
 751       --  Nrefs is 0, so we should not reset it here.
 752
 753       if Nrefs >= 2 then
 754          Ref_Count := Nrefs;
 755          Nrefs     := 1;
 756
 757          for Index in 2 .. Ref_Count loop
 758             if Xrefs.Table (Rnums (Index)) /=
 759                Xrefs.Table (Rnums (Nrefs))
 760             then
 761                Nrefs := Nrefs + 1;
 762                Rnums (Nrefs) := Rnums (Index);
 763             end if;
 764          end loop;
 765       end if;
 766
 767       --  Eliminate the reference if it is at the same location as the previous
 768       --  one, unless it is a read-reference indicating that the entity is an
 769       --  in-out actual in a call.
 770
 771       Ref_Count := Nrefs;
 772       Nrefs     := 0;
 773       Loc       := No_Location;
 774       Prev_Typ  := 'm';
 775
 776       for Index in 1 .. Ref_Count loop
 777          declare
 778             Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
 779
 780          begin
 781             if Ref.Loc /= Loc
 782               or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
 783             then
 784                Loc           := Ref.Loc;
 785                Prev_Typ      := Ref.Typ;
 786                Nrefs         := Nrefs + 1;
 787                Rnums (Nrefs) := Rnums (Index);
 788             end if;
 789          end;
 790       end loop;
 791
 792       --  The two steps have eliminated all references, nothing to do
 793
 794       if SPARK_Scope_Table.Last = 0 then
 795          return;
 796       end if;
 797
 798       Ref_Id     := Empty;
 799       Scope_Id   := 1;
 800       From_Index := 1;
 801
 802       --  Loop to output references
 803
 804       for Refno in 1 .. Nrefs loop
 805          declare
 806             Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
 807             Ref       : Xref_Key   renames Ref_Entry.Key;
 808
 809          begin
 810             --  If this assertion fails, the scope which we are looking for is
 811             --  not in SPARK scope table, which reveals either a problem in the
 812             --  construction of the scope table, or an erroneous scope for the
 813             --  current cross-reference.
 814
 815             pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
 816
 817             --  Update the range of cross references to which the current scope
 818             --  refers to. This may be the empty range only for the first scope
 819             --  considered.
 820
 821             if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
 822                Update_Scope_Range
 823                  (S    => Scope_Id,
 824                   From => From_Index,
 825                   To   => SPARK_Xref_Table.Last);
 826
 827                From_Index := SPARK_Xref_Table.Last + 1;
 828             end if;
 829
 830             while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
 831                Scope_Id := Scope_Id + 1;
 832                pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
 833             end loop;
 834
 835             if Ref.Ent /= Ref_Id then
 836                Ref_Name := new String'(Unique_Name (Ref.Ent));
 837             end if;
 838
 839             if Ref.Ent = Heap then
 840                Line := 0;
 841                Col  := 0;
 842             else
 843                Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
 844                Col  := Int (Get_Column_Number (Ref_Entry.Def));
 845             end if;
 846
 847             SPARK_Xref_Table.Append (
 848               (Entity_Name => Ref_Name,
 849                Entity_Line => Line,
 850                Etype       => Get_Entity_Type (Ref.Ent),
 851                Entity_Col  => Col,
 852                File_Num    => Dependency_Num (Ref.Lun),
 853                Scope_Num   => Get_Scope_Num (Ref.Ref_Scope),
 854                Line        => Int (Get_Logical_Line_Number (Ref.Loc)),
 855                Rtype       => Ref.Typ,
 856                Col         => Int (Get_Column_Number (Ref.Loc))));
 857          end;
 858       end loop;
 859
 860       --  Update the range of cross references to which the scope refers to
 861
 862       Update_Scope_Range
 863         (S    => Scope_Id,
 864          From => From_Index,
 865          To   => SPARK_Xref_Table.Last);
 866    end Add_SPARK_Xrefs;
 867
 868    -------------------------
 869    -- Collect_SPARK_Xrefs --
 870    -------------------------
 871
 872    procedure Collect_SPARK_Xrefs
 873      (Sdep_Table : Unit_Ref_Table;
 874       Num_Sdep   : Nat)
 875    is
 876       D1 : Nat;
 877       D2 : Nat;
 878
 879    begin
 880       --  Cross-references should have been computed first
 881
 882       pragma Assert (Xrefs.Last /= 0);
 883
 884       Initialize_SPARK_Tables;
 885
 886       --  Generate file and scope SPARK cross-reference information
 887
 888       D1 := 1;
 889       while D1 <= Num_Sdep loop
 890
 891          --  In rare cases, when treating the library-level instantiation of a
 892          --  generic, two consecutive units refer to the same compilation unit
 893          --  node and entity. In that case, treat them as a single unit for the
 894          --  sake of SPARK cross references by passing to Add_SPARK_File.
 895
 896          if D1 < Num_Sdep
 897            and then Cunit_Entity (Sdep_Table (D1)) =
 898                     Cunit_Entity (Sdep_Table (D1 + 1))
 899          then
 900             D2 := D1 + 1;
 901          else
 902             D2 := D1;
 903          end if;
 904
 905          Add_SPARK_File
 906            (Ubody => Sdep_Table (D1),
 907             Uspec => Sdep_Table (D2),
 908             Dspec => D2);
 909          D1 := D2 + 1;
 910       end loop;
 911
 912       --  Fill in the spec information when relevant
 913
 914       declare
 915          package Entity_Hash_Table is new
 916            GNAT.HTable.Simple_HTable
 917              (Header_Num => Entity_Hashed_Range,
 918               Element    => Scope_Index,
 919               No_Element => 0,
 920               Key        => Entity_Id,
 921               Hash       => Entity_Hash,
 922               Equal      => "=");
 923
 924       begin
 925          --  Fill in the hash-table
 926
 927          for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
 928             declare
 929                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
 930             begin
 931                Entity_Hash_Table.Set (Srec.Scope_Entity, S);
 932             end;
 933          end loop;
 934
 935          --  Use the hash-table to locate spec entities
 936
 937          for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
 938             declare
 939                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
 940
 941                Spec_Entity : constant Entity_Id :=
 942                                Unique_Entity (Srec.Scope_Entity);
 943                Spec_Scope  : constant Scope_Index :=
 944                                Entity_Hash_Table.Get (Spec_Entity);
 945
 946             begin
 947                --  Generic spec may be missing in which case Spec_Scope is zero
 948
 949                if Spec_Entity /= Srec.Scope_Entity
 950                  and then Spec_Scope /= 0
 951                then
 952                   Srec.Spec_File_Num :=
 953                     SPARK_Scope_Table.Table (Spec_Scope).File_Num;
 954                   Srec.Spec_Scope_Num :=
 955                     SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
 956                end if;
 957             end;
 958          end loop;
 959       end;
 960
 961       --  Generate SPARK cross-reference information
 962
 963       Add_SPARK_Xrefs;
 964    end Collect_SPARK_Xrefs;
 965
 966    --------------------------------
 967    -- Detect_And_Add_SPARK_Scope --
 968    --------------------------------
 969
 970    procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
 971    begin
 972       if Nkind_In (N, N_Subprogram_Declaration,
 973                       N_Subprogram_Body,
 974                       N_Subprogram_Body_Stub,
 975                       N_Package_Declaration,
 976                       N_Package_Body)
 977       then
 978          Add_SPARK_Scope (N);
 979       end if;
 980    end Detect_And_Add_SPARK_Scope;
 981
 982    -------------------------------------
 983    -- Enclosing_Subprogram_Or_Package --
 984    -------------------------------------
 985
 986    function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
 987       Result : Entity_Id;
 988
 989    begin
 990       --  If N is the defining identifier for a subprogram, then return the
 991       --  enclosing subprogram or package, not this subprogram.
 992
 993       if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
 994         and then Nkind (Parent (N)) in N_Subprogram_Specification
 995       then
 996          Result := Parent (Parent (Parent (N)));
 997       else
 998          Result := N;
 999       end if;
1000
1001       while Present (Result) loop
1002          case Nkind (Result) is
1003             when N_Package_Specification =>
1004                Result := Defining_Unit_Name (Result);
1005                exit;
1006
1007             when N_Package_Body =>
1008                Result := Defining_Unit_Name (Result);
1009                exit;
1010
1011             when N_Subprogram_Specification =>
1012                Result := Defining_Unit_Name (Result);
1013                exit;
1014
1015             when N_Subprogram_Declaration =>
1016                Result := Defining_Unit_Name (Specification (Result));
1017                exit;
1018
1019             when N_Subprogram_Body =>
1020                Result := Defining_Unit_Name (Specification (Result));
1021                exit;
1022
1023             --  The enclosing subprogram for a pre- or postconditions should be
1024             --  the subprogram to which the pragma is attached. This is not
1025             --  always the case in the AST, as the pragma may be declared after
1026             --  the declaration of the subprogram. Return Empty in this case.
1027
1028             when N_Pragma =>
1029                if Get_Pragma_Id (Result) = Pragma_Precondition
1030                     or else
1031                   Get_Pragma_Id (Result) = Pragma_Postcondition
1032                then
1033                   return Empty;
1034                else
1035                   Result := Parent (Result);
1036                end if;
1037
1038             when others =>
1039                Result := Parent (Result);
1040          end case;
1041       end loop;
1042
1043       if Nkind (Result) = N_Defining_Program_Unit_Name then
1044          Result := Defining_Identifier (Result);
1045       end if;
1046
1047       --  Do not return a scope without a proper location
1048
1049       if Present (Result)
1050         and then Sloc (Result) = No_Location
1051       then
1052          return Empty;
1053       end if;
1054
1055       return Result;
1056    end Enclosing_Subprogram_Or_Package;
1057
1058    -----------------
1059    -- Entity_Hash --
1060    -----------------
1061
1062    function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1063    begin
1064       return
1065         Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1066    end Entity_Hash;
1067
1068    --------------------------
1069    -- Generate_Dereference --
1070    --------------------------
1071
1072    procedure Generate_Dereference
1073      (N   : Node_Id;
1074       Typ : Character := 'r')
1075    is
1076       procedure Create_Heap;
1077       --  Create and decorate the special entity which denotes the heap
1078
1079       -----------------
1080       -- Create_Heap --
1081       -----------------
1082
1083       procedure Create_Heap is
1084       begin
1085          Name_Len := Name_Of_Heap_Variable'Length;
1086          Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1087
1088          Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1089
1090          Set_Ekind       (Heap, E_Variable);
1091          Set_Is_Internal (Heap, True);
1092          Set_Has_Fully_Qualified_Name (Heap);
1093       end Create_Heap;
1094
1095       --  Local variables
1096
1097       Loc       : constant Source_Ptr := Sloc (N);
1098       Index     : Nat;
1099       Ref_Scope : Entity_Id;
1100
1101    --  Start of processing for Generate_Dereference
1102
1103    begin
1104
1105       if Loc > No_Location then
1106          Drefs.Increment_Last;
1107          Index := Drefs.Last;
1108
1109          declare
1110             Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1111             Deref       : Xref_Key   renames Deref_Entry.Key;
1112
1113          begin
1114             if No (Heap) then
1115                Create_Heap;
1116             end if;
1117
1118             Ref_Scope := Enclosing_Subprogram_Or_Package (N);
1119
1120             Deref.Ent := Heap;
1121             Deref.Loc := Loc;
1122             Deref.Typ := Typ;
1123
1124             --  It is as if the special "Heap" was defined in every scope where
1125             --  it is referenced.
1126
1127             Deref.Eun := Get_Code_Unit (Loc);
1128             Deref.Lun := Get_Code_Unit (Loc);
1129
1130             Deref.Ref_Scope := Ref_Scope;
1131             Deref.Ent_Scope := Ref_Scope;
1132
1133             Deref_Entry.Def := No_Location;
1134
1135             Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1136          end;
1137       end if;
1138    end Generate_Dereference;
1139
1140    ------------------------------------
1141    -- Traverse_All_Compilation_Units --
1142    ------------------------------------
1143
1144    procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1145    begin
1146       for U in Units.First .. Last_Unit loop
1147          Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1148       end loop;
1149    end Traverse_All_Compilation_Units;
1150
1151    -------------------------------
1152    -- Traverse_Compilation_Unit --
1153    -------------------------------
1154
1155    procedure Traverse_Compilation_Unit
1156      (CU           : Node_Id;
1157       Process      : Node_Processing;
1158       Inside_Stubs : Boolean)
1159    is
1160       Lu : Node_Id;
1161
1162    begin
1163       --  Get Unit (checking case of subunit)
1164
1165       Lu := Unit (CU);
1166
1167       if Nkind (Lu) = N_Subunit then
1168          Lu := Proper_Body (Lu);
1169       end if;
1170
1171       --  Do not add scopes for generic units
1172
1173       if Nkind (Lu) = N_Package_Body
1174         and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1175       then
1176          return;
1177       end if;
1178
1179       --  Call Process on all declarations
1180
1181       if Nkind (Lu) in N_Declaration
1182         or else Nkind (Lu) in N_Later_Decl_Item
1183       then
1184          Process (Lu);
1185       end if;
1186
1187       --  Traverse the unit
1188
1189       if Nkind (Lu) = N_Subprogram_Body then
1190          Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1191
1192       elsif Nkind (Lu) = N_Subprogram_Declaration then
1193          null;
1194
1195       elsif Nkind (Lu) = N_Package_Declaration then
1196          Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1197
1198       elsif Nkind (Lu) = N_Package_Body then
1199          Traverse_Package_Body (Lu, Process, Inside_Stubs);
1200
1201       --  All other cases of compilation units (e.g. renamings), are not
1202       --  declarations, or else generic declarations which are ignored.
1203
1204       else
1205          null;
1206       end if;
1207    end Traverse_Compilation_Unit;
1208
1209    -----------------------------------------
1210    -- Traverse_Declarations_Or_Statements --
1211    -----------------------------------------
1212
1213    procedure Traverse_Declarations_Or_Statements
1214      (L            : List_Id;
1215       Process      : Node_Processing;
1216       Inside_Stubs : Boolean)
1217    is
1218       N : Node_Id;
1219
1220    begin
1221       --  Loop through statements or declarations
1222
1223       N := First (L);
1224       while Present (N) loop
1225          --  Call Process on all declarations
1226
1227          if Nkind (N) in N_Declaration
1228               or else
1229             Nkind (N) in N_Later_Decl_Item
1230          then
1231             Process (N);
1232          end if;
1233
1234          case Nkind (N) is
1235
1236             --  Package declaration
1237
1238             when N_Package_Declaration =>
1239                Traverse_Package_Declaration (N, Process, Inside_Stubs);
1240
1241             --  Package body
1242
1243             when N_Package_Body =>
1244                if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1245                   Traverse_Package_Body (N, Process, Inside_Stubs);
1246                end if;
1247
1248             when N_Package_Body_Stub =>
1249                if Present (Library_Unit (N)) then
1250                   declare
1251                      Body_N : constant Node_Id := Get_Body_From_Stub (N);
1252                   begin
1253                      if Inside_Stubs
1254                        and then
1255                          Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1256                      then
1257                         Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1258                      end if;
1259                   end;
1260                end if;
1261
1262             --  Subprogram declaration
1263
1264             when N_Subprogram_Declaration =>
1265                null;
1266
1267             --  Subprogram body
1268
1269             when N_Subprogram_Body =>
1270                if not Is_Generic_Subprogram (Defining_Entity (N)) then
1271                   Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1272                end if;
1273
1274             when N_Subprogram_Body_Stub =>
1275                if Present (Library_Unit (N)) then
1276                   declare
1277                      Body_N : constant Node_Id := Get_Body_From_Stub (N);
1278                   begin
1279                      if Inside_Stubs
1280                        and then
1281                          not Is_Generic_Subprogram (Defining_Entity (Body_N))
1282                      then
1283                         Traverse_Subprogram_Body
1284                           (Body_N, Process, Inside_Stubs);
1285                      end if;
1286                   end;
1287                end if;
1288
1289             --  Block statement
1290
1291             when N_Block_Statement =>
1292                Traverse_Declarations_Or_Statements
1293                  (Declarations (N), Process, Inside_Stubs);
1294                Traverse_Handled_Statement_Sequence
1295                  (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1296
1297             when N_If_Statement =>
1298
1299                --  Traverse the statements in the THEN part
1300
1301                Traverse_Declarations_Or_Statements
1302                  (Then_Statements (N), Process, Inside_Stubs);
1303
1304                --  Loop through ELSIF parts if present
1305
1306                if Present (Elsif_Parts (N)) then
1307                   declare
1308                      Elif : Node_Id := First (Elsif_Parts (N));
1309
1310                   begin
1311                      while Present (Elif) loop
1312                         Traverse_Declarations_Or_Statements
1313                           (Then_Statements (Elif), Process, Inside_Stubs);
1314                         Next (Elif);
1315                      end loop;
1316                   end;
1317                end if;
1318
1319                --  Finally traverse the ELSE statements if present
1320
1321                Traverse_Declarations_Or_Statements
1322                  (Else_Statements (N), Process, Inside_Stubs);
1323
1324             --  Case statement
1325
1326             when N_Case_Statement =>
1327
1328                --  Process case branches
1329
1330                declare
1331                   Alt : Node_Id;
1332                begin
1333                   Alt := First (Alternatives (N));
1334                   while Present (Alt) loop
1335                      Traverse_Declarations_Or_Statements
1336                        (Statements (Alt), Process, Inside_Stubs);
1337                      Next (Alt);
1338                   end loop;
1339                end;
1340
1341             --  Extended return statement
1342
1343             when N_Extended_Return_Statement =>
1344                Traverse_Handled_Statement_Sequence
1345                  (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1346
1347             --  Loop
1348
1349             when N_Loop_Statement =>
1350                Traverse_Declarations_Or_Statements
1351                  (Statements (N), Process, Inside_Stubs);
1352
1353             --  Generic declarations are ignored
1354
1355             when others =>
1356                null;
1357          end case;
1358
1359          Next (N);
1360       end loop;
1361    end Traverse_Declarations_Or_Statements;
1362
1363    -----------------------------------------
1364    -- Traverse_Handled_Statement_Sequence --
1365    -----------------------------------------
1366
1367    procedure Traverse_Handled_Statement_Sequence
1368      (N            : Node_Id;
1369       Process      : Node_Processing;
1370       Inside_Stubs : Boolean)
1371    is
1372       Handler : Node_Id;
1373
1374    begin
1375       if Present (N) then
1376          Traverse_Declarations_Or_Statements
1377            (Statements (N), Process, Inside_Stubs);
1378
1379          if Present (Exception_Handlers (N)) then
1380             Handler := First (Exception_Handlers (N));
1381             while Present (Handler) loop
1382                Traverse_Declarations_Or_Statements
1383                  (Statements (Handler), Process, Inside_Stubs);
1384                Next (Handler);
1385             end loop;
1386          end if;
1387       end if;
1388    end Traverse_Handled_Statement_Sequence;
1389
1390    ---------------------------
1391    -- Traverse_Package_Body --
1392    ---------------------------
1393
1394    procedure Traverse_Package_Body
1395      (N            : Node_Id;
1396       Process      : Node_Processing;
1397       Inside_Stubs : Boolean) is
1398    begin
1399       Traverse_Declarations_Or_Statements
1400         (Declarations (N), Process, Inside_Stubs);
1401       Traverse_Handled_Statement_Sequence
1402         (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1403    end Traverse_Package_Body;
1404
1405    ----------------------------------
1406    -- Traverse_Package_Declaration --
1407    ----------------------------------
1408
1409    procedure Traverse_Package_Declaration
1410      (N            : Node_Id;
1411       Process      : Node_Processing;
1412       Inside_Stubs : Boolean)
1413    is
1414       Spec : constant Node_Id := Specification (N);
1415    begin
1416       Traverse_Declarations_Or_Statements
1417         (Visible_Declarations (Spec), Process, Inside_Stubs);
1418       Traverse_Declarations_Or_Statements
1419         (Private_Declarations (Spec), Process, Inside_Stubs);
1420    end Traverse_Package_Declaration;
1421
1422    ------------------------------
1423    -- Traverse_Subprogram_Body --
1424    ------------------------------
1425
1426    procedure Traverse_Subprogram_Body
1427      (N            : Node_Id;
1428       Process      : Node_Processing;
1429       Inside_Stubs : Boolean)
1430    is
1431    begin
1432       Traverse_Declarations_Or_Statements
1433         (Declarations (N), Process, Inside_Stubs);
1434       Traverse_Handled_Statement_Sequence
1435         (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1436    end Traverse_Subprogram_Body;
1437
1438 end SPARK_Specific;