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