[thirdparty/gcc.git] / gcc / ada / lib-xref-spark_specific.adb

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--              L I B . X R E F . S P A R K _ S P E C I F I C               --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--          Copyright (C) 2011-2016, Free Software Foundation, Inc.         --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

with Einfo;       use Einfo;
with Nmake;       use Nmake;
with SPARK_Xrefs; use SPARK_Xrefs;

with GNAT.HTable;

separate (Lib.Xref)
package body SPARK_Specific is

   ---------------------
   -- Local Constants --
   ---------------------

   --  Table of SPARK_Entities, True for each entity kind used in SPARK

   SPARK_Entities : constant array (Entity_Kind) of Boolean :=
     (E_Constant         => True,
      E_Entry            => True,
      E_Function         => True,
      E_In_Out_Parameter => True,
      E_In_Parameter     => True,
      E_Loop_Parameter   => True,
      E_Operator         => True,
      E_Out_Parameter    => True,
      E_Procedure        => True,
      E_Variable         => True,
      others             => False);

   --  True for each reference type used in SPARK

   SPARK_References : constant array (Character) of Boolean :=
     ('m' => True,
      'r' => True,
      's' => True,
      others => False);

   type Entity_Hashed_Range is range 0 .. 255;
   --  Size of hash table headers

   ---------------------
   -- Local Variables --
   ---------------------

   Heap : Entity_Id := Empty;
   --  A special entity which denotes the heap object

   package Drefs is new Table.Table (
     Table_Component_Type => Xref_Entry,
     Table_Index_Type     => Xref_Entry_Number,
     Table_Low_Bound      => 1,
     Table_Initial        => Alloc.Drefs_Initial,
     Table_Increment      => Alloc.Drefs_Increment,
     Table_Name           => "Drefs");
   --  Table of cross-references for reads and writes through explicit
   --  dereferences, that are output as reads/writes to the special variable
   --  "Heap". These references are added to the regular references when
   --  computing SPARK cross-references.

   -----------------------
   -- Local Subprograms --
   -----------------------

   procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat);
   --  Add file and corresponding scopes for unit to the tables
   --  SPARK_File_Table and SPARK_Scope_Table. When two units are present for
   --  the same compilation unit, as it happens for library-level
   --  instantiations of generics, then Ubody /= Uspec, and all scopes are
   --  added to the same SPARK file. Otherwise Ubody = Uspec.

   procedure Add_SPARK_Scope (N : Node_Id);
   --  Add scope N to the table SPARK_Scope_Table

   procedure Add_SPARK_Xrefs;
   --  Filter table Xrefs to add all references used in SPARK to the table
   --  SPARK_Xref_Table.

   procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
   --  Call Add_SPARK_Scope on scopes

   function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
   --  Hash function for hash table

   procedure Traverse_Declaration_Or_Statement
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   procedure Traverse_Declarations_Or_Statements
     (L            : List_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   procedure Traverse_Handled_Statement_Sequence
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   procedure Traverse_Protected_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   procedure Traverse_Package_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   procedure Traverse_Subprogram_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean);
   --  Traverse corresponding construct, calling Process on all declarations

   --------------------
   -- Add_SPARK_File --
   --------------------

   procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat) is
      File : constant Source_File_Index := Source_Index (Uspec);
      From : Scope_Index;

      File_Name      : String_Ptr;
      Unit_File_Name : String_Ptr;

   begin
      --  Source file could be inexistant as a result of an error, if option
      --  gnatQ is used.

      if File = No_Source_File then
         return;
      end if;

      --  Subunits are traversed as part of the top-level unit to which they
      --  belong.

      if Nkind (Unit (Cunit (Ubody))) = N_Subunit then
         return;
      end if;

      From := SPARK_Scope_Table.Last + 1;

      Traverse_Compilation_Unit
        (CU           => Cunit (Ubody),
         Process      => Detect_And_Add_SPARK_Scope'Access,
         Inside_Stubs => True);

      --  When two units are present for the same compilation unit, as it
      --  happens for library-level instantiations of generics, then add all
      --  scopes to the same SPARK file.

      if Ubody /= Uspec then
         Traverse_Compilation_Unit
           (CU           => Cunit (Uspec),
            Process      => Detect_And_Add_SPARK_Scope'Access,
            Inside_Stubs => True);
      end if;

      --  Update scope numbers

      declare
         Scope_Id : Pos;
      begin
         Scope_Id := 1;
         for Index in From .. SPARK_Scope_Table.Last loop
            declare
               S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
            begin
               S.Scope_Num := Scope_Id;
               S.File_Num  := Dspec;
               Scope_Id    := Scope_Id + 1;
            end;
         end loop;
      end;

      --  Make entry for new file in file table

      Get_Name_String (Reference_Name (File));
      File_Name := new String'(Name_Buffer (1 .. Name_Len));

      --  For subunits, also retrieve the file name of the unit. Only do so if
      --  unit has an associated compilation unit.

      if Present (Cunit (Unit (File)))
        and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
      then
         Get_Name_String (Reference_Name (Main_Source_File));
         Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
      else
         Unit_File_Name := null;
      end if;

      SPARK_File_Table.Append (
        (File_Name      => File_Name,
         Unit_File_Name => Unit_File_Name,
         File_Num       => Dspec,
         From_Scope     => From,
         To_Scope       => SPARK_Scope_Table.Last));
   end Add_SPARK_File;

   ---------------------
   -- Add_SPARK_Scope --
   ---------------------

   procedure Add_SPARK_Scope (N : Node_Id) is
      E   : constant Entity_Id  := Defining_Entity (N);
      Loc : constant Source_Ptr := Sloc (E);

      --  The character describing the kind of scope is chosen to be the same
      --  as the one describing the corresponding entity in cross references,
      --  see Xref_Entity_Letters in lib-xrefs.ads

      Typ : Character;

   begin
      --  Ignore scopes without a proper location

      if Sloc (N) = No_Location then
         return;
      end if;

      case Ekind (E) is
         when E_Entry
            | E_Entry_Family
            | E_Generic_Function
            | E_Generic_Package
            | E_Generic_Procedure
            | E_Package
            | E_Protected_Type
            | E_Task_Type
         =>
            Typ := Xref_Entity_Letters (Ekind (E));

         when E_Function
            | E_Procedure
         =>
            --  In SPARK we need to distinguish protected functions and
            --  procedures from ordinary subprograms, but there are no special
            --  Xref letters for them. Since this distiction is only needed
            --  to detect protected calls, we pretend that such calls are entry
            --  calls.

            if Ekind (Scope (E)) = E_Protected_Type then
               Typ := Xref_Entity_Letters (E_Entry);
            else
               Typ := Xref_Entity_Letters (Ekind (E));
            end if;

         when E_Package_Body
            | E_Protected_Body
            | E_Subprogram_Body
            | E_Task_Body
         =>
            Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));

         when E_Void =>

            --  Compilation of prj-attr.adb with -gnatn creates a node with
            --  entity E_Void for the package defined at a-charac.ads16:13.
            --  ??? TBD

            return;

         when others =>
            raise Program_Error;
      end case;

      --  File_Num and Scope_Num are filled later. From_Xref and To_Xref are
      --  filled even later, but are initialized to represent an empty range.

      SPARK_Scope_Table.Append (
        (Scope_Name     => new String'(Unique_Name (E)),
         File_Num       => 0,
         Scope_Num      => 0,
         Spec_File_Num  => 0,
         Spec_Scope_Num => 0,
         Line           => Nat (Get_Logical_Line_Number (Loc)),
         Stype          => Typ,
         Col            => Nat (Get_Column_Number (Loc)),
         From_Xref      => 1,
         To_Xref        => 0,
         Scope_Entity   => E));
   end Add_SPARK_Scope;

   ---------------------
   -- Add_SPARK_Xrefs --
   ---------------------

   procedure Add_SPARK_Xrefs is
      function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
      --  Return the entity which maps to the input scope index

      function Get_Entity_Type (E : Entity_Id) return Character;
      --  Return a character representing the type of entity

      function Is_Constant_Object_Without_Variable_Input
        (E : Entity_Id) return Boolean;
      --  Return True if E is known to have no variable input, as defined in
      --  SPARK RM.

      function Is_Future_Scope_Entity
        (E : Entity_Id;
         S : Scope_Index) return Boolean;
      --  Check whether entity E is in SPARK_Scope_Table at index S or higher

      function Is_SPARK_Reference
        (E   : Entity_Id;
         Typ : Character) return Boolean;
      --  Return whether entity reference E meets SPARK requirements. Typ is
      --  the reference type.

      function Is_SPARK_Scope (E : Entity_Id) return Boolean;
      --  Return whether the entity or reference scope meets requirements for
      --  being a SPARK scope.

      function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
      --  Comparison function for Sort call

      procedure Move (From : Natural; To : Natural);
      --  Move procedure for Sort call

      procedure Update_Scope_Range
        (S    : Scope_Index;
         From : Xref_Index;
         To   : Xref_Index);
      --  Update the scope which maps to S with the new range From .. To

      package Sorting is new GNAT.Heap_Sort_G (Move, Lt);

      function Get_Scope_Num (N : Entity_Id) return Nat;
      --  Return the scope number associated to entity N

      procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
      --  Associate entity N to scope number Num

      No_Scope : constant Nat := 0;
      --  Initial scope counter

      type Scope_Rec is record
         Num    : Nat;
         Entity : Entity_Id;
      end record;
      --  Type used to relate an entity and a scope number

      package Scopes is new GNAT.HTable.Simple_HTable
        (Header_Num => Entity_Hashed_Range,
         Element    => Scope_Rec,
         No_Element => (Num => No_Scope, Entity => Empty),
         Key        => Entity_Id,
         Hash       => Entity_Hash,
         Equal      => "=");
      --  Package used to build a correspondence between entities and scope
      --  numbers used in SPARK cross references.

      Nrefs : Nat := Xrefs.Last;
      --  Number of references in table. This value may get reset (reduced)
      --  when we eliminate duplicate reference entries as well as references
      --  not suitable for local cross-references.

      Nrefs_Add : constant Nat := Drefs.Last;
      --  Number of additional references which correspond to dereferences in
      --  the source code.

      Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
      --  This array contains numbers of references in the Xrefs table. This
      --  list is sorted in output order. The extra 0'th entry is convenient
      --  for the call to sort. When we sort the table, we move the entries in
      --  Rnums around, but we do not move the original table entries.

      ---------------------
      -- Entity_Of_Scope --
      ---------------------

      function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
      begin
         return SPARK_Scope_Table.Table (S).Scope_Entity;
      end Entity_Of_Scope;

      ---------------------
      -- Get_Entity_Type --
      ---------------------

      function Get_Entity_Type (E : Entity_Id) return Character is
      begin
         case Ekind (E) is
            when E_Out_Parameter    => return '<';
            when E_In_Out_Parameter => return '=';
            when E_In_Parameter     => return '>';
            when others             => return '*';
         end case;
      end Get_Entity_Type;

      -------------------
      -- Get_Scope_Num --
      -------------------

      function Get_Scope_Num (N : Entity_Id) return Nat is
      begin
         return Scopes.Get (N).Num;
      end Get_Scope_Num;

      -----------------------------------------------
      -- Is_Constant_Object_Without_Variable_Input --
      -----------------------------------------------

      function Is_Constant_Object_Without_Variable_Input
        (E : Entity_Id) return Boolean
      is
         Result : Boolean;

      begin
         case Ekind (E) is

            --  A constant is known to have no variable input if its
            --  initializing expression is static (a value which is
            --  compile-time-known is not guaranteed to have no variable input
            --  as defined in the SPARK RM). Otherwise, the constant may or not
            --  have variable input.

            when E_Constant =>
               declare
                  Decl : Node_Id;
               begin
                  if Present (Full_View (E)) then
                     Decl := Parent (Full_View (E));
                  else
                     Decl := Parent (E);
                  end if;

                  if Is_Imported (E) then
                     Result := False;
                  else
                     pragma Assert (Present (Expression (Decl)));
                     Result := Is_Static_Expression (Expression (Decl));
                  end if;
               end;

            when E_Loop_Parameter | E_In_Parameter =>
               Result := True;

            when others =>
               Result := False;
         end case;

         return Result;
      end Is_Constant_Object_Without_Variable_Input;

      ----------------------------
      -- Is_Future_Scope_Entity --
      ----------------------------

      function Is_Future_Scope_Entity
        (E : Entity_Id;
         S : Scope_Index) return Boolean
      is
         function Is_Past_Scope_Entity return Boolean;
         --  Check whether entity E is in SPARK_Scope_Table at index strictly
         --  lower than S.

         --------------------------
         -- Is_Past_Scope_Entity --
         --------------------------

         function Is_Past_Scope_Entity return Boolean is
         begin
            for Index in SPARK_Scope_Table.First .. S - 1 loop
               if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
                  return True;
               end if;
            end loop;

            return False;
         end Is_Past_Scope_Entity;

      --  Start of processing for Is_Future_Scope_Entity

      begin
         for Index in S .. SPARK_Scope_Table.Last loop
            if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
               return True;
            end if;
         end loop;

         --  If this assertion fails, this means that the scope which we are
         --  looking for has been treated already, which reveals a problem in
         --  the order of cross-references.

         pragma Assert (not Is_Past_Scope_Entity);

         return False;
      end Is_Future_Scope_Entity;

      ------------------------
      -- Is_SPARK_Reference --
      ------------------------

      function Is_SPARK_Reference
        (E   : Entity_Id;
         Typ : Character) return Boolean
      is
      begin
         --  The only references of interest on callable entities are calls. On
         --  uncallable entities, the only references of interest are reads and
         --  writes.

         if Ekind (E) in Overloadable_Kind then
            return Typ = 's';

         --  Objects of task or protected types are not SPARK references

         elsif Present (Etype (E))
           and then Ekind (Etype (E)) in Concurrent_Kind
         then
            return False;

         --  In all other cases, result is true for reference/modify cases,
         --  and false for all other cases.

         else
            return Typ = 'r' or else Typ = 'm';
         end if;
      end Is_SPARK_Reference;

      --------------------
      -- Is_SPARK_Scope --
      --------------------

      function Is_SPARK_Scope (E : Entity_Id) return Boolean is
      begin
         return Present (E)
           and then not Is_Generic_Unit (E)
           and then Renamed_Entity (E) = Empty
           and then Get_Scope_Num (E) /= No_Scope;
      end Is_SPARK_Scope;

      --------
      -- Lt --
      --------

      function Lt (Op1, Op2 : Natural) return Boolean is
         T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
         T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));

      begin
         --  First test: if entity is in different unit, sort by unit. Note:
         --  that we use Ent_Scope_File rather than Eun, as Eun may refer to
         --  the file where the generic scope is defined, which may differ from
         --  the file where the enclosing scope is defined. It is the latter
         --  which matters for a correct order here.

         if T1.Ent_Scope_File /= T2.Ent_Scope_File then
            return Dependency_Num (T1.Ent_Scope_File) <
                   Dependency_Num (T2.Ent_Scope_File);

         --  Second test: within same unit, sort by location of the scope of
         --  the entity definition.

         elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
               Get_Scope_Num (T2.Key.Ent_Scope)
         then
            return Get_Scope_Num (T1.Key.Ent_Scope) <
                   Get_Scope_Num (T2.Key.Ent_Scope);

         --  Third test: within same unit and scope, sort by location of
         --  entity definition.

         elsif T1.Def /= T2.Def then
            return T1.Def < T2.Def;

         else
            --  Both entities must be equal at this point

            pragma Assert (T1.Key.Ent = T2.Key.Ent);
            pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
            pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);

            --  Fourth test: if reference is in same unit as entity definition,
            --  sort first.

            if T1.Key.Lun /= T2.Key.Lun
              and then T1.Ent_Scope_File = T1.Key.Lun
            then
               return True;

            elsif T1.Key.Lun /= T2.Key.Lun
              and then T2.Ent_Scope_File = T2.Key.Lun
            then
               return False;

            --  Fifth test: if reference is in same unit and same scope as
            --  entity definition, sort first.

            elsif T1.Ent_Scope_File = T1.Key.Lun
              and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
              and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
            then
               return True;

            elsif T2.Ent_Scope_File = T2.Key.Lun
              and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
              and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
            then
               return False;

            --  Sixth test: for same entity, sort by reference location unit

            elsif T1.Key.Lun /= T2.Key.Lun then
               return Dependency_Num (T1.Key.Lun) <
                      Dependency_Num (T2.Key.Lun);

            --  Seventh test: for same entity, sort by reference location scope

            elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
                  Get_Scope_Num (T2.Key.Ref_Scope)
            then
               return Get_Scope_Num (T1.Key.Ref_Scope) <
                      Get_Scope_Num (T2.Key.Ref_Scope);

            --  Eighth test: order of location within referencing unit

            elsif T1.Key.Loc /= T2.Key.Loc then
               return T1.Key.Loc < T2.Key.Loc;

            --  Finally, for two locations at the same address prefer the one
            --  that does NOT have the type 'r', so that a modification or
            --  extension takes preference, when there are more than one
            --  reference at the same location. As a result, in the case of
            --  entities that are in-out actuals, the read reference follows
            --  the modify reference.

            else
               return T2.Key.Typ = 'r';
            end if;
         end if;
      end Lt;

      ----------
      -- Move --
      ----------

      procedure Move (From : Natural; To : Natural) is
      begin
         Rnums (Nat (To)) := Rnums (Nat (From));
      end Move;

      -------------------
      -- Set_Scope_Num --
      -------------------

      procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
      begin
         Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N));
      end Set_Scope_Num;

      ------------------------
      -- Update_Scope_Range --
      ------------------------

      procedure Update_Scope_Range
        (S    : Scope_Index;
         From : Xref_Index;
         To   : Xref_Index)
      is
      begin
         SPARK_Scope_Table.Table (S).From_Xref := From;
         SPARK_Scope_Table.Table (S).To_Xref := To;
      end Update_Scope_Range;

      --  Local variables

      Col        : Nat;
      From_Index : Xref_Index;
      Line       : Nat;
      Loc        : Source_Ptr;
      Prev_Typ   : Character;
      Ref_Count  : Nat;
      Ref_Id     : Entity_Id;
      Ref_Name   : String_Ptr;
      Scope_Id   : Scope_Index;

   --  Start of processing for Add_SPARK_Xrefs

   begin
      for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
         declare
            S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
         begin
            Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
         end;
      end loop;

      --  Set up the pointer vector for the sort

      for Index in 1 .. Nrefs loop
         Rnums (Index) := Index;
      end loop;

      for Index in Drefs.First .. Drefs.Last loop
         Xrefs.Append (Drefs.Table (Index));

         Nrefs         := Nrefs + 1;
         Rnums (Nrefs) := Xrefs.Last;
      end loop;

      --  Capture the definition Sloc values. As in the case of normal cross
      --  references, we have to wait until now to get the correct value.

      for Index in 1 .. Nrefs loop
         Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
      end loop;

      --  Eliminate entries not appropriate for SPARK. Done prior to sorting
      --  cross-references, as it discards useless references which do not have
      --  a proper format for the comparison function (like no location).

      Ref_Count := Nrefs;
      Nrefs     := 0;

      for Index in 1 .. Ref_Count loop
         declare
            Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;

         begin
            if SPARK_Entities (Ekind (Ref.Ent))
              and then SPARK_References (Ref.Typ)
              and then Is_SPARK_Scope (Ref.Ent_Scope)
              and then Is_SPARK_Scope (Ref.Ref_Scope)
              and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)

              --  Discard references from unknown scopes, e.g. generic scopes

              and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
              and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
            then
               Nrefs         := Nrefs + 1;
               Rnums (Nrefs) := Rnums (Index);
            end if;
         end;
      end loop;

      --  Sort the references

      Sorting.Sort (Integer (Nrefs));

      --  Eliminate duplicate entries

      --  We need this test for Ref_Count because if we force ALI file
      --  generation in case of errors detected, it may be the case that
      --  Nrefs is 0, so we should not reset it here.

      if Nrefs >= 2 then
         Ref_Count := Nrefs;
         Nrefs     := 1;

         for Index in 2 .. Ref_Count loop
            if Xrefs.Table (Rnums (Index)) /=
               Xrefs.Table (Rnums (Nrefs))
            then
               Nrefs := Nrefs + 1;
               Rnums (Nrefs) := Rnums (Index);
            end if;
         end loop;
      end if;

      --  Eliminate the reference if it is at the same location as the previous
      --  one, unless it is a read-reference indicating that the entity is an
      --  in-out actual in a call.

      Ref_Count := Nrefs;
      Nrefs     := 0;
      Loc       := No_Location;
      Prev_Typ  := 'm';

      for Index in 1 .. Ref_Count loop
         declare
            Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;

         begin
            if Ref.Loc /= Loc
              or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
            then
               Loc           := Ref.Loc;
               Prev_Typ      := Ref.Typ;
               Nrefs         := Nrefs + 1;
               Rnums (Nrefs) := Rnums (Index);
            end if;
         end;
      end loop;

      --  The two steps have eliminated all references, nothing to do

      if SPARK_Scope_Table.Last = 0 then
         return;
      end if;

      Ref_Id     := Empty;
      Scope_Id   := 1;
      From_Index := 1;

      --  Loop to output references

      for Refno in 1 .. Nrefs loop
         declare
            Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
            Ref       : Xref_Key   renames Ref_Entry.Key;
            Typ       : Character;

         begin
            --  If this assertion fails, the scope which we are looking for is
            --  not in SPARK scope table, which reveals either a problem in the
            --  construction of the scope table, or an erroneous scope for the
            --  current cross-reference.

            pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));

            --  Update the range of cross references to which the current scope
            --  refers to. This may be the empty range only for the first scope
            --  considered.

            if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
               Update_Scope_Range
                 (S    => Scope_Id,
                  From => From_Index,
                  To   => SPARK_Xref_Table.Last);

               From_Index := SPARK_Xref_Table.Last + 1;
            end if;

            while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
               Scope_Id := Scope_Id + 1;
               pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
            end loop;

            if Ref.Ent /= Ref_Id then
               Ref_Name := new String'(Unique_Name (Ref.Ent));
            end if;

            if Ref.Ent = Heap then
               Line := 0;
               Col  := 0;
            else
               Line := Nat (Get_Logical_Line_Number (Ref_Entry.Def));
               Col  := Nat (Get_Column_Number (Ref_Entry.Def));
            end if;

            --  References to constant objects without variable inputs (see
            --  SPARK RM 3.3.1) are considered specially in SPARK section,
            --  because these will be translated as constants in the
            --  intermediate language for formal verification, and should
            --  therefore never appear in frame conditions. Other constants may
            --  later be treated the same, up to GNATprove to decide based on
            --  its flow analysis.

            if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
               Typ := 'c';
            else
               Typ := Ref.Typ;
            end if;

            SPARK_Xref_Table.Append (
              (Entity_Name => Ref_Name,
               Entity_Line => Line,
               Etype       => Get_Entity_Type (Ref.Ent),
               Entity_Col  => Col,
               File_Num    => Dependency_Num (Ref.Lun),
               Scope_Num   => Get_Scope_Num (Ref.Ref_Scope),
               Line        => Nat (Get_Logical_Line_Number (Ref.Loc)),
               Rtype       => Typ,
               Col         => Nat (Get_Column_Number (Ref.Loc))));
         end;
      end loop;

      --  Update the range of cross references to which the scope refers to

      Update_Scope_Range
        (S    => Scope_Id,
         From => From_Index,
         To   => SPARK_Xref_Table.Last);
   end Add_SPARK_Xrefs;

   -------------------------
   -- Collect_SPARK_Xrefs --
   -------------------------

   procedure Collect_SPARK_Xrefs
     (Sdep_Table : Unit_Ref_Table;
      Num_Sdep   : Nat)
   is
      D1 : Pos;
      D2 : Pos;

   begin
      --  Cross-references should have been computed first

      pragma Assert (Xrefs.Last /= 0);

      Initialize_SPARK_Tables;

      --  Generate file and scope SPARK cross-reference information

      D1 := 1;
      while D1 <= Num_Sdep loop

         --  In rare cases, when treating the library-level instantiation of a
         --  generic, two consecutive units refer to the same compilation unit
         --  node and entity. In that case, treat them as a single unit for the
         --  sake of SPARK cross references by passing to Add_SPARK_File.

         if D1 < Num_Sdep
           and then Cunit_Entity (Sdep_Table (D1)) =
                    Cunit_Entity (Sdep_Table (D1 + 1))
         then
            declare
               Cunit1 : Node_Id renames Cunit (Sdep_Table (D1));
               Cunit2 : Node_Id renames Cunit (Sdep_Table (D1 + 1));
            begin
               --  Both Cunit point to compilation unit nodes
               pragma Assert (Nkind (Cunit1) = N_Compilation_Unit
                                and then
                              Nkind (Cunit2) = N_Compilation_Unit);

               --  Do not depend on the sorting order, which is based on
               --  Unit_Name and for library-level instances of nested
               --  generic-packages they are equal.

               --  If declaration comes before the body then just set D2
               if Nkind (Unit (Cunit1)) = N_Package_Declaration
                 and then
                  Nkind (Unit (Cunit2)) = N_Package_Body
               then
                  D2 := D1 + 1;

               --  If body comes before declaration then set D2 and adjust D1

               elsif Nkind (Unit (Cunit1)) = N_Package_Body
                       and then
                     Nkind (Unit (Cunit2)) = N_Package_Declaration
               then
                  D2 := D1;
                  D1 := D1 + 1;

               else

                  raise Program_Error;
               end if;
            end;
         else
            D2 := D1;
         end if;

         --  Skip dependencies with no entity node, e.g. configuration files
         --  with pragmas (.adc) or target description (.atp), since they
         --  present no interest for SPARK cross references.

         if Present (Cunit_Entity (Sdep_Table (D1))) then
            Add_SPARK_File
              (Ubody => Sdep_Table (D1),
               Uspec => Sdep_Table (D2),
               Dspec => D2);
         end if;

         D1 := Pos'Max (D1, D2) + 1;
      end loop;

      --  Fill in the spec information when relevant

      declare
         package Entity_Hash_Table is new
           GNAT.HTable.Simple_HTable
             (Header_Num => Entity_Hashed_Range,
              Element    => Scope_Index,
              No_Element => 0,
              Key        => Entity_Id,
              Hash       => Entity_Hash,
              Equal      => "=");

      begin
         --  Fill in the hash-table

         for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
            declare
               Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
            begin
               Entity_Hash_Table.Set (Srec.Scope_Entity, S);
            end;
         end loop;

         --  Use the hash-table to locate spec entities

         for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
            declare
               Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);

               Spec_Entity : constant Entity_Id :=
                               Unique_Entity (Srec.Scope_Entity);
               Spec_Scope  : constant Scope_Index :=
                               Entity_Hash_Table.Get (Spec_Entity);

            begin
               --  Generic spec may be missing in which case Spec_Scope is zero

               if Spec_Entity /= Srec.Scope_Entity
                 and then Spec_Scope /= 0
               then
                  Srec.Spec_File_Num :=
                    SPARK_Scope_Table.Table (Spec_Scope).File_Num;
                  Srec.Spec_Scope_Num :=
                    SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
               end if;
            end;
         end loop;
      end;

      --  Generate SPARK cross-reference information

      Add_SPARK_Xrefs;
   end Collect_SPARK_Xrefs;

   --------------------------------
   -- Detect_And_Add_SPARK_Scope --
   --------------------------------

   procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
   begin
      if Nkind_In (N, N_Entry_Body,             --  entries
                      N_Entry_Declaration)
           or else
         Nkind_In (N, N_Package_Body,           --  packages
                      N_Package_Body_Stub,
                      N_Package_Declaration)
           or else
         Nkind_In (N, N_Protected_Body,         --  protected objects
                      N_Protected_Body_Stub,
                      N_Protected_Type_Declaration)
           or else
         Nkind_In (N, N_Subprogram_Body,        --  subprograms
                      N_Subprogram_Body_Stub,
                      N_Subprogram_Declaration)
           or else
         Nkind_In (N, N_Task_Body,              --  tasks
                      N_Task_Body_Stub,
                      N_Task_Type_Declaration)
      then
         Add_SPARK_Scope (N);
      end if;
   end Detect_And_Add_SPARK_Scope;

   -------------------------------------
   -- Enclosing_Subprogram_Or_Package --
   -------------------------------------

   function Enclosing_Subprogram_Or_Library_Package
     (N : Node_Id) return Entity_Id
   is
      Context : Entity_Id;

   begin
      --  If N is the defining identifier for a subprogram, then return the
      --  enclosing subprogram or package, not this subprogram.

      if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
        and then (Ekind (N) in Entry_Kind
                   or else Ekind (N) = E_Subprogram_Body
                   or else Ekind (N) in Generic_Subprogram_Kind
                   or else Ekind (N) in Subprogram_Kind)
      then
         Context := Parent (Unit_Declaration_Node (N));

         --  If this was a library-level subprogram then replace Context with
         --  its Unit, which points to N_Subprogram_* node.

         if Nkind (Context) = N_Compilation_Unit then
            Context := Unit (Context);
         end if;
      else
         Context := N;
      end if;

      while Present (Context) loop
         case Nkind (Context) is
            when N_Package_Body          |
                 N_Package_Specification =>

               --  Only return a library-level package

               if Is_Library_Level_Entity (Defining_Entity (Context)) then
                  Context := Defining_Entity (Context);
                  exit;
               else
                  Context := Parent (Context);
               end if;

            when N_Pragma =>

               --  The enclosing subprogram for a precondition, postcondition,
               --  or contract case should be the declaration preceding the
               --  pragma (skipping any other pragmas between this pragma and
               --  this declaration.

               while Nkind (Context) = N_Pragma
                 and then Is_List_Member (Context)
                 and then Present (Prev (Context))
               loop
                  Context := Prev (Context);
               end loop;

               if Nkind (Context) = N_Pragma then
                  Context := Parent (Context);
               end if;

            when N_Entry_Body                 |
                 N_Entry_Declaration          |
                 N_Protected_Type_Declaration |
                 N_Subprogram_Body            |
                 N_Subprogram_Declaration     |
                 N_Subprogram_Specification   |
                 N_Task_Body                  |
                 N_Task_Type_Declaration      =>
               Context := Defining_Entity (Context);
               exit;

            when others =>
               Context := Parent (Context);
         end case;
      end loop;

      if Nkind (Context) = N_Defining_Program_Unit_Name then
         Context := Defining_Identifier (Context);
      end if;

      --  Do not return a scope without a proper location

      if Present (Context)
        and then Sloc (Context) = No_Location
      then
         return Empty;
      end if;

      return Context;
   end Enclosing_Subprogram_Or_Library_Package;

   -----------------
   -- Entity_Hash --
   -----------------

   function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
   begin
      return
        Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
   end Entity_Hash;

   --------------------------
   -- Generate_Dereference --
   --------------------------

   procedure Generate_Dereference
     (N   : Node_Id;
      Typ : Character := 'r')
   is
      procedure Create_Heap;
      --  Create and decorate the special entity which denotes the heap

      -----------------
      -- Create_Heap --
      -----------------

      procedure Create_Heap is
      begin
         Name_Len := Name_Of_Heap_Variable'Length;
         Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;

         Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);

         Set_Ekind       (Heap, E_Variable);
         Set_Is_Internal (Heap, True);
         Set_Has_Fully_Qualified_Name (Heap);
      end Create_Heap;

      --  Local variables

      Loc : constant Source_Ptr := Sloc (N);

   --  Start of processing for Generate_Dereference

   begin

      if Loc > No_Location then
         Drefs.Increment_Last;

         declare
            Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
            Deref       : Xref_Key   renames Deref_Entry.Key;

         begin
            if No (Heap) then
               Create_Heap;
            end if;

            Deref.Ent := Heap;
            Deref.Loc := Loc;
            Deref.Typ := Typ;

            --  It is as if the special "Heap" was defined in the main unit,
            --  in the scope of the entity for the main unit. This single
            --  definition point is required to ensure that sorting cross
            --  references works for "Heap" references as well.

            Deref.Eun := Main_Unit;
            Deref.Lun := Get_Top_Level_Code_Unit (Loc);

            Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
            Deref.Ent_Scope := Cunit_Entity (Main_Unit);

            Deref_Entry.Def := No_Location;

            Deref_Entry.Ent_Scope_File := Main_Unit;
         end;
      end if;
   end Generate_Dereference;

   -------------------------------
   -- Traverse_Compilation_Unit --
   -------------------------------

   procedure Traverse_Compilation_Unit
     (CU           : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean)
   is
      Lu : Node_Id;

   begin
      --  Get Unit (checking case of subunit)

      Lu := Unit (CU);

      if Nkind (Lu) = N_Subunit then
         Lu := Proper_Body (Lu);
      end if;

      --  Do not add scopes for generic units

      if Nkind (Lu) = N_Package_Body
        and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
      then
         return;
      end if;

      --  Call Process on all declarations

      if Nkind (Lu) in N_Declaration
        or else Nkind (Lu) in N_Later_Decl_Item
      then
         Process (Lu);
      end if;

      --  Traverse the unit

      Traverse_Declaration_Or_Statement (Lu, Process, Inside_Stubs);
   end Traverse_Compilation_Unit;

   ---------------------------------------
   -- Traverse_Declaration_Or_Statement --
   ---------------------------------------

   procedure Traverse_Declaration_Or_Statement
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean)
   is
   begin
      case Nkind (N) is
         when N_Package_Declaration =>
            declare
               Spec : constant Node_Id := Specification (N);
            begin
               Traverse_Declarations_Or_Statements
                 (Visible_Declarations (Spec), Process, Inside_Stubs);
               Traverse_Declarations_Or_Statements
                 (Private_Declarations (Spec), Process, Inside_Stubs);
            end;

         when N_Package_Body =>
            if Ekind (Defining_Entity (N)) /= E_Generic_Package then
               Traverse_Package_Body (N, Process, Inside_Stubs);
            end if;

         when N_Package_Body_Stub =>
            if Present (Library_Unit (N)) then
               declare
                  Body_N : constant Node_Id := Get_Body_From_Stub (N);
               begin
                  if Inside_Stubs
                    and then
                      Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
                  then
                     Traverse_Package_Body (Body_N, Process, Inside_Stubs);
                  end if;
               end;
            end if;

         when N_Subprogram_Declaration =>
            null;

         when N_Entry_Body | N_Subprogram_Body =>
            if not Is_Generic_Subprogram (Defining_Entity (N)) then
               Traverse_Subprogram_Body (N, Process, Inside_Stubs);
            end if;

         when N_Subprogram_Body_Stub =>
            if Present (Library_Unit (N)) then
               declare
                  Body_N : constant Node_Id := Get_Body_From_Stub (N);
               begin
                  if Inside_Stubs
                    and then
                      not Is_Generic_Subprogram (Defining_Entity (Body_N))
                  then
                     Traverse_Subprogram_Body (Body_N, Process, Inside_Stubs);
                  end if;
               end;
            end if;

         when N_Protected_Body =>
            Traverse_Protected_Body (N, Process, Inside_Stubs);

         when N_Protected_Body_Stub =>
            if Present (Library_Unit (N)) then
               declare
                  Body_N : constant Node_Id := Get_Body_From_Stub (N);
               begin
                  if Inside_Stubs then
                     Traverse_Declarations_Or_Statements
                       (Declarations (Body_N), Process, Inside_Stubs);
                  end if;
               end;
            end if;

         when N_Protected_Type_Declaration | N_Single_Protected_Declaration =>
            declare
               Def : constant Node_Id := Protected_Definition (N);
            begin
               Traverse_Declarations_Or_Statements
                 (Visible_Declarations (Def), Process, Inside_Stubs);
               Traverse_Declarations_Or_Statements
                 (Private_Declarations (Def), Process, Inside_Stubs);
            end;

         when N_Task_Definition =>
            Traverse_Declarations_Or_Statements
              (Visible_Declarations (N), Process, Inside_Stubs);
            Traverse_Declarations_Or_Statements
              (Private_Declarations (N), Process, Inside_Stubs);

         when N_Task_Body =>
            Traverse_Declarations_Or_Statements
              (Declarations (N), Process, Inside_Stubs);
            Traverse_Handled_Statement_Sequence
              (Handled_Statement_Sequence (N), Process, Inside_Stubs);

         when N_Task_Body_Stub =>
            if Present (Library_Unit (N)) then
               declare
                  Body_N : constant Node_Id := Get_Body_From_Stub (N);
               begin
                  if Inside_Stubs then
                     Traverse_Declarations_Or_Statements
                       (Declarations (Body_N), Process, Inside_Stubs);
                     Traverse_Handled_Statement_Sequence
                       (Handled_Statement_Sequence (Body_N), Process,
                        Inside_Stubs);
                  end if;
               end;
            end if;

         when N_Block_Statement =>
            Traverse_Declarations_Or_Statements
              (Declarations (N), Process, Inside_Stubs);
            Traverse_Handled_Statement_Sequence
              (Handled_Statement_Sequence (N), Process, Inside_Stubs);

         when N_If_Statement =>

            --  Traverse the statements in the THEN part

            Traverse_Declarations_Or_Statements
              (Then_Statements (N), Process, Inside_Stubs);

            --  Loop through ELSIF parts if present

            if Present (Elsif_Parts (N)) then
               declare
                  Elif : Node_Id := First (Elsif_Parts (N));

               begin
                  while Present (Elif) loop
                     Traverse_Declarations_Or_Statements
                       (Then_Statements (Elif), Process, Inside_Stubs);
                     Next (Elif);
                  end loop;
               end;
            end if;

            --  Finally traverse the ELSE statements if present

            Traverse_Declarations_Or_Statements
              (Else_Statements (N), Process, Inside_Stubs);

         when N_Case_Statement =>

            --  Process case branches

            declare
               Alt : Node_Id;
            begin
               Alt := First (Alternatives (N));
               while Present (Alt) loop
                  Traverse_Declarations_Or_Statements
                    (Statements (Alt), Process, Inside_Stubs);
                  Next (Alt);
               end loop;
            end;

         when N_Extended_Return_Statement =>
            Traverse_Handled_Statement_Sequence
              (Handled_Statement_Sequence (N), Process, Inside_Stubs);

         when N_Loop_Statement =>
            Traverse_Declarations_Or_Statements
              (Statements (N), Process, Inside_Stubs);

         --  Generic declarations are ignored

         when others =>
            null;
      end case;
   end Traverse_Declaration_Or_Statement;

   -----------------------------------------
   -- Traverse_Declarations_Or_Statements --
   -----------------------------------------

   procedure Traverse_Declarations_Or_Statements
     (L            : List_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean)
   is
      N : Node_Id;

   begin
      --  Loop through statements or declarations

      N := First (L);
      while Present (N) loop
         --  Call Process on all declarations

         if Nkind (N) in N_Declaration
              or else
            Nkind (N) in N_Later_Decl_Item
              or else
            Nkind (N) = N_Entry_Body
         then
            Process (N);
         end if;

         Traverse_Declaration_Or_Statement (N, Process, Inside_Stubs);

         Next (N);
      end loop;
   end Traverse_Declarations_Or_Statements;

   -----------------------------------------
   -- Traverse_Handled_Statement_Sequence --
   -----------------------------------------

   procedure Traverse_Handled_Statement_Sequence
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean)
   is
      Handler : Node_Id;

   begin
      if Present (N) then
         Traverse_Declarations_Or_Statements
           (Statements (N), Process, Inside_Stubs);

         if Present (Exception_Handlers (N)) then
            Handler := First (Exception_Handlers (N));
            while Present (Handler) loop
               Traverse_Declarations_Or_Statements
                 (Statements (Handler), Process, Inside_Stubs);
               Next (Handler);
            end loop;
         end if;
      end if;
   end Traverse_Handled_Statement_Sequence;

   ---------------------------
   -- Traverse_Package_Body --
   ---------------------------

   procedure Traverse_Package_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean) is
   begin
      Traverse_Declarations_Or_Statements
        (Declarations (N), Process, Inside_Stubs);
      Traverse_Handled_Statement_Sequence
        (Handled_Statement_Sequence (N), Process, Inside_Stubs);
   end Traverse_Package_Body;

   -----------------------------
   -- Traverse_Protected_Body --
   -----------------------------

   procedure Traverse_Protected_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean) is
   begin
      Traverse_Declarations_Or_Statements
        (Declarations (N), Process, Inside_Stubs);
   end Traverse_Protected_Body;

   ------------------------------
   -- Traverse_Subprogram_Body --
   ------------------------------

   procedure Traverse_Subprogram_Body
     (N            : Node_Id;
      Process      : Node_Processing;
      Inside_Stubs : Boolean)
   is
   begin
      Traverse_Declarations_Or_Statements
        (Declarations (N), Process, Inside_Stubs);
      Traverse_Handled_Statement_Sequence
        (Handled_Statement_Sequence (N), Process, Inside_Stubs);
   end Traverse_Subprogram_Body;

end SPARK_Specific;