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