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