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