[multiple changes]

2012-03-30  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Process_Declarations): Replace
	the call to Is_Null_Access_BIP_Func_Call with
	Is_Secondary_Stack_BIP_Func_Call. Update the related comment.
	* exp_util.adb (Is_Null_Access_BIP_Func_Call): Removed.
	(Is_Secondary_Stack_BIP_Func_Call): New routine.
	(Requires_Cleanup_Actions): Replace
	the call to Is_Null_Access_BIP_Func_Call with
	Is_Secondary_Stack_BIP_Func_Call. Update the related comment.
	* exp_util.ads (Is_Null_Access_BIP_Func_Call): Removed.
	(Is_Secondary_Stack_BIP_Func_Call): New routine.

2012-03-30  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb, lib-xref.adb: Code clean ups.

From-SVN: r186001

6 files changed, 537 insertions, 567 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9c10909..450239a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2012-03-30  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch7.adb (Process_Declarations): Replace
+	the call to Is_Null_Access_BIP_Func_Call with
+	Is_Secondary_Stack_BIP_Func_Call. Update the related comment.
+	* exp_util.adb (Is_Null_Access_BIP_Func_Call): Removed.
+	(Is_Secondary_Stack_BIP_Func_Call): New routine.
+	(Requires_Cleanup_Actions): Replace
+	the call to Is_Null_Access_BIP_Func_Call with
+	Is_Secondary_Stack_BIP_Func_Call. Update the related comment.
+	* exp_util.ads (Is_Null_Access_BIP_Func_Call): Removed.
+	(Is_Secondary_Stack_BIP_Func_Call): New routine.
+
+2012-03-30  Yannick Moy  <moy@adacore.com>
+
+	* lib-xref-alfa.adb, lib-xref.adb: Code clean ups.
+
 2012-03-30  Gary Dismukes  <dismukes@adacore.com>
 
 	* exp_ch5.adb (Expand_Iterator_Loop_Over_Array): For the case of a
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 0347dcc..525bae7 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -1824,15 +1824,14 @@ package body Exp_Ch7 is
                --    Obj : Access_Typ := Non_BIP_Function_Call'reference;
 
                --    Obj : Access_Typ :=
-               --            BIP_Function_Call
-               --              (..., BIPaccess => null, ...)'reference;
+               --            BIP_Function_Call (BIPalloc => 2, ...)'reference;
 
                elsif Is_Access_Type (Obj_Typ)
                  and then Needs_Finalization
                             (Available_View (Designated_Type (Obj_Typ)))
                  and then Present (Expr)
                  and then
-                   (Is_Null_Access_BIP_Func_Call (Expr)
+                   (Is_Secondary_Stack_BIP_Func_Call (Expr)
                      or else
                        (Is_Non_BIP_Func_Call (Expr)
                          and then not Is_Related_To_Func_Return (Obj_Id)))
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index ae7f2b9..f78442c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -4475,74 +4475,6 @@ package body Exp_Util is
         and then Is_Library_Level_Entity (Typ);
    end Is_Library_Level_Tagged_Type;
 
-   ----------------------------------
-   -- Is_Null_Access_BIP_Func_Call --
-   ----------------------------------
-
-   function Is_Null_Access_BIP_Func_Call (Expr : Node_Id) return Boolean is
-      Call : Node_Id := Expr;
-
-   begin
-      --  Build-in-place calls usually appear in 'reference format
-
-      if Nkind (Call) = N_Reference then
-         Call := Prefix (Call);
-      end if;
-
-      if Nkind_In (Call, N_Qualified_Expression,
-                         N_Unchecked_Type_Conversion)
-      then
-         Call := Expression (Call);
-      end if;
-
-      if Is_Build_In_Place_Function_Call (Call) then
-         declare
-            Access_Nam : Name_Id := No_Name;
-            Actual     : Node_Id;
-            Param      : Node_Id;
-            Formal     : Node_Id;
-
-         begin
-            --  Examine all parameter associations of the function call
-
-            Param := First (Parameter_Associations (Call));
-            while Present (Param) loop
-               if Nkind (Param) = N_Parameter_Association
-                 and then Nkind (Selector_Name (Param)) = N_Identifier
-               then
-                  Formal := Selector_Name (Param);
-                  Actual := Explicit_Actual_Parameter (Param);
-
-                  --  Construct the name of formal BIPaccess. It is much easier
-                  --  to extract the name of the function using an arbitrary
-                  --  formal's scope rather than the Name field of Call.
-
-                  if Access_Nam = No_Name
-                    and then Present (Entity (Formal))
-                  then
-                     Access_Nam :=
-                       New_External_Name
-                         (Chars (Scope (Entity (Formal))),
-                          BIP_Formal_Suffix (BIP_Object_Access));
-                  end if;
-
-                  --  A match for BIPaccess => null has been found
-
-                  if Chars (Formal) = Access_Nam
-                    and then Nkind (Actual) = N_Null
-                  then
-                     return True;
-                  end if;
-               end if;
-
-               Next (Param);
-            end loop;
-         end;
-      end if;
-
-      return False;
-   end Is_Null_Access_BIP_Func_Call;
-
    --------------------------
    -- Is_Non_BIP_Func_Call --
    --------------------------
@@ -4949,6 +4881,75 @@ package body Exp_Util is
       end if;
    end Is_Renamed_Object;
 
+   --------------------------------------
+   -- Is_Secondary_Stack_BIP_Func_Call --
+   --------------------------------------
+
+   function Is_Secondary_Stack_BIP_Func_Call (Expr : Node_Id) return Boolean is
+      Call : Node_Id := Expr;
+
+   begin
+      --  Build-in-place calls usually appear in 'reference format
+
+      if Nkind (Call) = N_Reference then
+         Call := Prefix (Call);
+      end if;
+
+      if Nkind_In (Call, N_Qualified_Expression,
+                         N_Unchecked_Type_Conversion)
+      then
+         Call := Expression (Call);
+      end if;
+
+      if Is_Build_In_Place_Function_Call (Call) then
+         declare
+            Access_Nam : Name_Id := No_Name;
+            Actual     : Node_Id;
+            Param      : Node_Id;
+            Formal     : Node_Id;
+
+         begin
+            --  Examine all parameter associations of the function call
+
+            Param := First (Parameter_Associations (Call));
+            while Present (Param) loop
+               if Nkind (Param) = N_Parameter_Association
+                 and then Nkind (Selector_Name (Param)) = N_Identifier
+               then
+                  Formal := Selector_Name (Param);
+                  Actual := Explicit_Actual_Parameter (Param);
+
+                  --  Construct the name of formal BIPalloc. It is much easier
+                  --  to extract the name of the function using an arbitrary
+                  --  formal's scope rather than the Name field of Call.
+
+                  if Access_Nam = No_Name
+                    and then Present (Entity (Formal))
+                  then
+                     Access_Nam :=
+                       New_External_Name
+                         (Chars (Scope (Entity (Formal))),
+                          BIP_Formal_Suffix (BIP_Alloc_Form));
+                  end if;
+
+                  --  A match for BIPalloc => 2 has been found
+
+                  if Chars (Formal) = Access_Nam
+                    and then Nkind (Actual) = N_Integer_Literal
+                    and then Intval (Actual) = Uint_2
+                  then
+                     return True;
+                  end if;
+               end if;
+
+               Next (Param);
+            end loop;
+         end;
+      end if;
+
+      return False;
+   end Is_Secondary_Stack_BIP_Func_Call;
+
    -------------------------------------
    -- Is_Tag_To_Class_Wide_Conversion --
    -------------------------------------
@@ -7123,18 +7124,17 @@ package body Exp_Util is
             --    Obj : Access_Typ := Non_BIP_Function_Call'reference;
             --
             --    Obj : Access_Typ :=
-            --            BIP_Function_Call
-            --              (..., BIPaccess => null, ...)'reference;
+            --            BIP_Function_Call (BIPalloc => 2, ...)'reference;
 
             elsif Is_Access_Type (Obj_Typ)
               and then Needs_Finalization
                          (Available_View (Designated_Type (Obj_Typ)))
               and then Present (Expr)
               and then
-                (Is_Null_Access_BIP_Func_Call (Expr)
-                   or else
-                (Is_Non_BIP_Func_Call (Expr)
-                   and then not Is_Related_To_Func_Return (Obj_Id)))
+                (Is_Secondary_Stack_BIP_Func_Call (Expr)
+                  or else
+                    (Is_Non_BIP_Func_Call (Expr)
+                      and then not Is_Related_To_Func_Return (Obj_Id)))
             then
                return True;
 
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 97e9b5c..535a4ff 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -548,13 +548,20 @@ package Exp_Util is
    --  Return True if Typ is a library level tagged type. Currently we use
    --  this information to build statically allocated dispatch tables.
 
-   function Is_Null_Access_BIP_Func_Call (Expr : Node_Id) return Boolean;
-   --  Determine whether node Expr denotes a build-in-place function call with
-   --  a value of "null" for extra formal BIPaccess.
-
    function Is_Non_BIP_Func_Call (Expr : Node_Id) return Boolean;
    --  Determine whether node Expr denotes a non build-in-place function call
 
+   function Is_Possibly_Unaligned_Object (N : Node_Id) return Boolean;
+   --  Node N is an object reference. This function returns True if it is
+   --  possible that the object may not be aligned according to the normal
+   --  default alignment requirement for its type (e.g. if it appears in a
+   --  packed record, or as part of a component that has a component clause.)
+
+   function Is_Possibly_Unaligned_Slice (N : Node_Id) return Boolean;
+   --  Determine whether the node P is a slice of an array where the slice
+   --  result may cause alignment problems because it has an alignment that
+   --  is not compatible with the type. Return True if so.
+
    function Is_Ref_To_Bit_Packed_Array (N : Node_Id) return Boolean;
    --  Determine whether the node P is a reference to a bit packed array, i.e.
    --  whether the designated object is a component of a bit packed array, or a
@@ -571,17 +578,6 @@ package Exp_Util is
    --  Determine whether object Id is related to an expanded return statement.
    --  The case concerned is "return Id.all;".
 
-   function Is_Possibly_Unaligned_Slice (N : Node_Id) return Boolean;
-   --  Determine whether the node P is a slice of an array where the slice
-   --  result may cause alignment problems because it has an alignment that
-   --  is not compatible with the type. Return True if so.
-
-   function Is_Possibly_Unaligned_Object (N : Node_Id) return Boolean;
-   --  Node N is an object reference. This function returns True if it is
-   --  possible that the object may not be aligned according to the normal
-   --  default alignment requirement for its type (e.g. if it appears in a
-   --  packed record, or as part of a component that has a component clause.)
-
    function Is_Renamed_Object (N : Node_Id) return Boolean;
    --  Returns True if the node N is a renamed object. An expression is
    --  considered to be a renamed object if either it is the Name of an object
@@ -593,6 +589,10 @@ package Exp_Util is
    --  We consider that a (1 .. 2) is a renamed object since it is the prefix
    --  of the name in the renaming declaration.
 
+   function Is_Secondary_Stack_BIP_Func_Call (Expr : Node_Id) return Boolean;
+   --  Determine whether Expr denotes a build-in-place function which returns
+   --  its result on the secondary stack.
+
    function Is_Tag_To_Class_Wide_Conversion
      (Obj_Id : Entity_Id) return Boolean;
    --  Determine whether object Obj_Id is the result of a tag-to-class-wide
diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb
index 588213c..f454463 100644
--- a/gcc/ada/lib-xref-alfa.adb
+++ b/gcc/ada/lib-xref-alfa.adb
@@ -40,100 +40,16 @@ package body Alfa is
    --  Table of Alfa_Entities, True for each entity kind used in Alfa
 
    Alfa_Entities : constant array (Entity_Kind) of Boolean :=
-     (E_Void                                       => False,
-      E_Variable                                   => True,
-      E_Component                                  => False,
-      E_Constant                                   => True,
-      E_Discriminant                               => False,
-
-      E_Loop_Parameter                             => True,
-      E_In_Parameter                               => True,
-      E_Out_Parameter                              => True,
-      E_In_Out_Parameter                           => True,
-      E_Generic_In_Out_Parameter                   => False,
-
-      E_Generic_In_Parameter                       => False,
-      E_Named_Integer                              => False,
-      E_Named_Real                                 => False,
-      E_Enumeration_Type                           => False,
-      E_Enumeration_Subtype                        => False,
-
-      E_Signed_Integer_Type                        => False,
-      E_Signed_Integer_Subtype                     => False,
-      E_Modular_Integer_Type                       => False,
-      E_Modular_Integer_Subtype                    => False,
-      E_Ordinary_Fixed_Point_Type                  => False,
-
-      E_Ordinary_Fixed_Point_Subtype               => False,
-      E_Decimal_Fixed_Point_Type                   => False,
-      E_Decimal_Fixed_Point_Subtype                => False,
-      E_Floating_Point_Type                        => False,
-      E_Floating_Point_Subtype                     => False,
-
-      E_Access_Type                                => False,
-      E_Access_Subtype                             => False,
-      E_Access_Attribute_Type                      => False,
-      E_Allocator_Type                             => False,
-      E_General_Access_Type                        => False,
-
-      E_Access_Subprogram_Type                     => False,
-      E_Access_Protected_Subprogram_Type           => False,
-      E_Anonymous_Access_Subprogram_Type           => False,
-      E_Anonymous_Access_Protected_Subprogram_Type => False,
-      E_Anonymous_Access_Type                      => False,
-
-      E_Array_Type                                 => False,
-      E_Array_Subtype                              => False,
-      E_String_Type                                => False,
-      E_String_Subtype                             => False,
-      E_String_Literal_Subtype                     => False,
-
-      E_Class_Wide_Type                            => False,
-      E_Class_Wide_Subtype                         => False,
-      E_Record_Type                                => False,
-      E_Record_Subtype                             => False,
-      E_Record_Type_With_Private                   => False,
-
-      E_Record_Subtype_With_Private                => False,
-      E_Private_Type                               => False,
-      E_Private_Subtype                            => False,
-      E_Limited_Private_Type                       => False,
-      E_Limited_Private_Subtype                    => False,
-
-      E_Incomplete_Type                            => False,
-      E_Incomplete_Subtype                         => False,
-      E_Task_Type                                  => False,
-      E_Task_Subtype                               => False,
-      E_Protected_Type                             => False,
-
-      E_Protected_Subtype                          => False,
-      E_Exception_Type                             => False,
-      E_Subprogram_Type                            => False,
-      E_Enumeration_Literal                        => False,
-      E_Function                                   => True,
-
-      E_Operator                                   => True,
-      E_Procedure                                  => True,
-      E_Entry                                      => False,
-      E_Entry_Family                               => False,
-      E_Block                                      => False,
-
-      E_Entry_Index_Parameter                      => False,
-      E_Exception                                  => False,
-      E_Generic_Function                           => False,
-      E_Generic_Package                            => False,
-      E_Generic_Procedure                          => False,
-
-      E_Label                                      => False,
-      E_Loop                                       => False,
-      E_Return_Statement                           => False,
-      E_Package                                    => False,
-
-      E_Package_Body                               => False,
-      E_Protected_Object                           => False,
-      E_Protected_Body                             => False,
-      E_Task_Body                                  => False,
-      E_Subprogram_Body                            => False);
+     (E_Constant         => 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 Alfa
    Alfa_References : constant array (Character) of Boolean :=
@@ -149,6 +65,9 @@ package body Alfa is
    -- 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,
@@ -210,8 +129,8 @@ package body Alfa is
    -------------------
 
    procedure Add_Alfa_File (U : Unit_Number_Type; D : Nat) is
+      File : constant Source_File_Index := Source_Index (U);
       From : Scope_Index;
-      S    : constant Source_File_Index := Source_Index (U);
 
       File_Name      : String_Ptr;
       Unit_File_Name : String_Ptr;
@@ -220,7 +139,7 @@ package body Alfa is
       --  Source file could be inexistant as a result of an error, if option
       --  gnatQ is used.
 
-      if S = No_Source_File then
+      if File = No_Source_File then
          return;
       end if;
 
@@ -230,67 +149,64 @@ package body Alfa is
       --  filling Sdep_Table in Write_ALI.
 
       if Present (Cunit (U)) then
-         Traverse_Compilation_Unit (Cunit (U),
-                                    Detect_And_Add_Alfa_Scope'Access,
-                                    Inside_Stubs => False);
+         Traverse_Compilation_Unit
+           (CU           => Cunit (U),
+            Process      => Detect_And_Add_Alfa_Scope'Access,
+            Inside_Stubs => False);
       end if;
 
       --  Update scope numbers
 
       declare
-         Count : Nat;
+         Scope_Id : Int;
 
       begin
-         Count := 1;
-         for S in From .. Alfa_Scope_Table.Last loop
+         Scope_Id := 1;
+         for Index in From .. Alfa_Scope_Table.Last loop
             declare
-               E : Entity_Id renames Alfa_Scope_Table.Table (S).Scope_Entity;
+               S : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Index);
 
             begin
-               if Lib.Get_Source_Unit (E) = U then
-                  Alfa_Scope_Table.Table (S).Scope_Num := Count;
-                  Alfa_Scope_Table.Table (S).File_Num  := D;
-                  Count                                := Count + 1;
-
-               else
-                  --  Mark for removal a scope S which is not located in unit
-                  --  U, for example for scope inside generics that get
-                  --  instantiated.
-
-                  Alfa_Scope_Table.Table (S).Scope_Num := 0;
-               end if;
+               S.Scope_Num := Scope_Id;
+               S.File_Num  := D;
+               Scope_Id    := Scope_Id + 1;
             end;
          end loop;
       end;
 
+      --  Remove those scopes previously marked for removal
+
       declare
-         Snew : Scope_Index;
+         Scope_Id : Scope_Index;
 
       begin
-         Snew := From;
-         for S in From .. Alfa_Scope_Table.Last loop
-            --  Remove those scopes previously marked for removal
+         Scope_Id := From;
+         for Index in From .. Alfa_Scope_Table.Last loop
+            declare
+               S : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Index);
 
-            if Alfa_Scope_Table.Table (S).Scope_Num /= 0 then
-               Alfa_Scope_Table.Table (Snew) := Alfa_Scope_Table.Table (S);
-               Snew := Snew + 1;
-            end if;
+            begin
+               if S.Scope_Num /= 0 then
+                  Alfa_Scope_Table.Table (Scope_Id) := S;
+                  Scope_Id := Scope_Id + 1;
+               end if;
+            end;
          end loop;
 
-         Alfa_Scope_Table.Set_Last (Snew - 1);
+         Alfa_Scope_Table.Set_Last (Scope_Id - 1);
       end;
 
       --  Make entry for new file in file table
 
-      Get_Name_String (Reference_Name (S));
+      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 U has an associated compilation unit.
 
       if Present (Cunit (U))
-        and then Present (Cunit (Unit (S)))
-        and then Nkind (Unit (Cunit (Unit (S)))) = N_Subunit
+        and then 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));
@@ -384,10 +300,44 @@ package body Alfa is
    --------------------
 
    procedure Add_Alfa_Xrefs is
-      Cur_Scope_Idx   : Scope_Index;
-      From_Xref_Idx   : Xref_Index;
-      Cur_Entity      : Entity_Id;
-      Cur_Entity_Name : String_Ptr;
+      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_Alfa_Reference
+        (E   : Entity_Id;
+         Typ : Character) return Boolean;
+      --  Return whether entity reference E meets Alfa requirements. Typ is the
+      --  reference type.
+
+      function Is_Alfa_Scope (E : Entity_Id) return Boolean;
+      --  Return whether the entity or reference scope meets requirements for
+      --  being an Alfa scope.
+
+      function Is_Future_Scope_Entity
+        (E : Entity_Id;
+         S : Scope_Index) return Boolean;
+      --  Check whether entity E is in Alfa_Scope_Table at index S or higher
+
+      function Is_Global_Constant (E : Entity_Id) return Boolean;
+      --  Return True if E is a global constant for which we should ignore
+      --  reads in Alfa.
+
+      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);
 
       package Scopes is
          No_Scope : constant Nat := 0;
@@ -447,13 +397,144 @@ package body Alfa is
       --  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.
 
-      function Lt (Op1, Op2 : Natural) return Boolean;
-      --  Comparison function for Sort call
+      ---------------------
+      -- Entity_Of_Scope --
+      ---------------------
 
-      procedure Move (From : Natural; To : Natural);
-      --  Move procedure for Sort call
+      function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
+      begin
+         return Alfa_Scope_Table.Table (S).Scope_Entity;
+      end Entity_Of_Scope;
 
-      package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
+      ---------------------
+      -- Get_Entity_Type --
+      ---------------------
+
+      function Get_Entity_Type (E : Entity_Id) return Character is
+         C : Character;
+
+      begin
+         case Ekind (E) is
+            when E_Out_Parameter    => C := '<';
+            when E_In_Out_Parameter => C := '=';
+            when E_In_Parameter     => C := '>';
+            when others             => C := '*';
+         end case;
+
+         return C;
+      end Get_Entity_Type;
+
+      -----------------------
+      -- Is_Alfa_Reference --
+      -----------------------
+
+      function Is_Alfa_Reference
+        (E   : Entity_Id;
+         Typ : Character) return Boolean
+      is
+      begin
+         --  The only references of interest on callable entities are calls. On
+         --  non-callable entities, the only references of interest are reads
+         --  and writes.
+
+         if Ekind (E) in Overloadable_Kind then
+            return Typ = 's';
+
+         --  References to constant objects are not considered in Alfa section,
+         --  as these will be translated as constants in the intermediate
+         --  language for formal verification, and should therefore never
+         --  appear in frame conditions.
+
+         elsif Is_Constant_Object (E) then
+            return False;
+
+         --  Objects of Task type or protected type are not Alfa 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_Alfa_Reference;
+
+      -------------------
+      -- Is_Alfa_Scope --
+      -------------------
+
+      function Is_Alfa_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_Alfa_Scope;
+
+      ----------------------------
+      -- 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 Alfa_Scope_Table at index strictly
+         --  lower than S.
+
+         --------------------------
+         -- Is_Past_Scope_Entity --
+         --------------------------
+
+         function Is_Past_Scope_Entity return Boolean is
+         begin
+            for Index in Alfa_Scope_Table.First .. S - 1 loop
+               if Alfa_Scope_Table.Table (Index).Scope_Entity = E then
+                  declare
+                     Dummy : constant Alfa_Scope_Record :=
+                               Alfa_Scope_Table.Table (Index);
+                     pragma Unreferenced (Dummy);
+                  begin
+                     return True;
+                  end;
+               end if;
+            end loop;
+
+            return False;
+         end Is_Past_Scope_Entity;
+
+      --  Start of processing for Is_Future_Scope_Entity
+
+      begin
+         for Index in S .. Alfa_Scope_Table.Last loop
+            if Alfa_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_Global_Constant --
+      ------------------------
+
+      function Is_Global_Constant (E : Entity_Id) return Boolean is
+      begin
+         return Ekind (E) = E_Constant
+           and then Ekind_In (Scope (E), E_Package, E_Package_Body);
+      end Is_Global_Constant;
 
       --------
       -- Lt --
@@ -492,13 +573,13 @@ package body Alfa is
          --  Fourth test: if reference is in same unit as entity definition,
          --  sort first.
 
-         elsif
-           T1.Key.Lun /= T2.Key.Lun and then T1.Ent_Scope_File = T1.Key.Lun
+         elsif 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
+         elsif T1.Key.Lun /= T2.Key.Lun
+           and then T2.Ent_Scope_File = T2.Key.Lun
          then
             return False;
 
@@ -510,6 +591,7 @@ package body Alfa is
            and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
          then
             return True;
+
          elsif T1.Ent_Scope_File = T1.Key.Lun
            and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
            and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
@@ -554,44 +636,52 @@ package body Alfa is
          Rnums (Nat (To)) := Rnums (Nat (From));
       end Move;
 
-      Heap : Entity_Id;
+      ------------------------
+      -- Update_Scope_Range --
+      ------------------------
+
+      procedure Update_Scope_Range
+        (S    : Scope_Index;
+         From : Xref_Index;
+         To   : Xref_Index)
+      is
+      begin
+         Alfa_Scope_Table.Table (S).From_Xref := From;
+         Alfa_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_Alfa_Xrefs
 
    begin
-      for J in Alfa_Scope_Table.First .. Alfa_Scope_Table.Last loop
-         Set_Scope_Num (N   => Alfa_Scope_Table.Table (J).Scope_Entity,
-                        Num => Alfa_Scope_Table.Table (J).Scope_Num);
+      for Index in Alfa_Scope_Table.First .. Alfa_Scope_Table.Last loop
+         declare
+            S : Alfa_Scope_Record renames Alfa_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 J in 1 .. Nrefs loop
-         Rnums (J) := J;
+      for Index in 1 .. Nrefs loop
+         Rnums (Index) := Index;
       end loop;
 
-      --  Add dereferences to the set of regular references, by creating a
-      --  special "Heap" variable for these special references.
-
-      Name_Len := Name_Of_Heap_Variable'Length;
-      Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
-
-      Atree.Unlock;
-      Nlists.Unlock;
-      Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
-      Atree.Lock;
-      Nlists.Lock;
-
-      Set_Ekind         (Heap, E_Variable);
-      Set_Is_Internal   (Heap, True);
-      Set_Has_Fully_Qualified_Name (Heap);
-
-      for J in Drefs.First .. Drefs.Last loop
-         Xrefs.Append (Drefs.Table (J));
-
-         --  Set entity at this point with newly created "Heap" variable
-
-         Xrefs.Table (Xrefs.Last).Key.Ent := Heap;
+      for Index in Drefs.First .. Drefs.Last loop
+         Xrefs.Append (Drefs.Table (Index));
 
          Nrefs         := Nrefs + 1;
          Rnums (Nrefs) := Xrefs.Last;
@@ -601,261 +691,99 @@ package body Alfa is
       --  cross-references, as it discards useless references which do not have
       --  a proper format for the comparison function (like no location).
 
-      Eliminate_Before_Sort : declare
-         NR : Nat;
-
-         function Is_Alfa_Reference
-           (E   : Entity_Id;
-            Typ : Character) return Boolean;
-         --  Return whether entity reference E meets Alfa requirements. Typ
-         --  is the reference type.
-
-         function Is_Alfa_Scope (E : Entity_Id) return Boolean;
-         --  Return whether the entity or reference scope meets requirements
-         --  for being an Alfa scope.
+      Ref_Count := Nrefs;
+      Nrefs     := 0;
 
-         function Is_Global_Constant (E : Entity_Id) return Boolean;
-         --  Return True if E is a global constant for which we should ignore
-         --  reads in Alfa.
+      for Index in 1 .. Ref_Count loop
+         declare
+            Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
 
-         -----------------------
-         -- Is_Alfa_Reference --
-         -----------------------
-
-         function Is_Alfa_Reference
-           (E   : Entity_Id;
-            Typ : Character) return Boolean
-         is
          begin
-            --  The only references of interest on callable entities are calls.
-            --  On non-callable entities, the only references of interest are
-            --  reads and writes.
-
-            if Ekind (E) in Overloadable_Kind then
-               return Typ = 's';
-
-            --  References to constant objects are not considered in Alfa
-            --  section, as these will be translated as constants in the
-            --  intermediate language for formal verification, and should
-            --  therefore never appear in frame conditions.
-
-            elsif Is_Constant_Object (E) then
-                  return False;
-
-            --  Objects of Task type or protected type are not Alfa 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_Alfa_Reference;
-
-         -------------------
-         -- Is_Alfa_Scope --
-         -------------------
-
-         function Is_Alfa_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_Alfa_Scope;
-
-         ------------------------
-         -- Is_Global_Constant --
-         ------------------------
-
-         function Is_Global_Constant (E : Entity_Id) return Boolean is
-         begin
-            return Ekind (E) = E_Constant
-              and then Ekind_In (Scope (E), E_Package, E_Package_Body);
-         end Is_Global_Constant;
-
-      --  Start of processing for Eliminate_Before_Sort
-
-      begin
-         NR    := Nrefs;
-         Nrefs := 0;
-
-         for J in 1 .. NR loop
-            if Alfa_Entities (Ekind (Xrefs.Table (Rnums (J)).Key.Ent))
-              and then Alfa_References (Xrefs.Table (Rnums (J)).Key.Typ)
-              and then Is_Alfa_Scope (Xrefs.Table (Rnums (J)).Key.Ent_Scope)
-              and then Is_Alfa_Scope (Xrefs.Table (Rnums (J)).Key.Ref_Scope)
-              and then not Is_Global_Constant (Xrefs.Table (Rnums (J)).Key.Ent)
-              and then Is_Alfa_Reference (Xrefs.Table (Rnums (J)).Key.Ent,
-                                          Xrefs.Table (Rnums (J)).Key.Typ)
+            if Alfa_Entities (Ekind (Ref.Ent))
+              and then Alfa_References (Ref.Typ)
+              and then Is_Alfa_Scope (Ref.Ent_Scope)
+              and then Is_Alfa_Scope (Ref.Ref_Scope)
+              and then not Is_Global_Constant (Ref.Ent)
+              and then Is_Alfa_Reference (Ref.Ent, Ref.Typ)
+
+              --  Discard references from unknown scopes, such as 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 (J);
+               Rnums (Nrefs) := Rnums (Index);
             end if;
-         end loop;
-      end Eliminate_Before_Sort;
+         end;
+      end loop;
 
       --  Sort the references
 
       Sorting.Sort (Integer (Nrefs));
 
-      Eliminate_After_Sort : declare
-         NR : Nat;
-
-         Crloc : Source_Ptr;
-         --  Current reference location
+      --  Eliminate duplicate entries
 
-         Prevt : Character;
-         --  reference kind of previous reference
+      --  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.
 
-      begin
-         --  Eliminate duplicate entries
+      if Nrefs >= 2 then
+         Ref_Count := Nrefs;
+         Nrefs     := 1;
 
-         --  We need this test for NR 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
-            NR    := 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;
 
-            for J in 2 .. NR loop
-               if Xrefs.Table (Rnums (J)) /=
-                 Xrefs.Table (Rnums (Nrefs))
-               then
-                  Nrefs := Nrefs + 1;
-                  Rnums (Nrefs) := Rnums (J);
-               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.
 
-         --  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';
 
-         NR    := Nrefs;
-         Nrefs := 0;
-         Crloc := No_Location;
-         Prevt := 'm';
+      for Index in 1 .. Ref_Count loop
+         declare
+            Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
 
-         for J in 1 .. NR loop
-            if Xrefs.Table (Rnums (J)).Key.Loc /= Crloc
-              or else (Prevt = 'm'
-                        and then Xrefs.Table (Rnums (J)).Key.Typ = 'r')
+         begin
+            if Ref.Loc /= Loc
+              or else (Prev_Typ = 'm'
+                        and then Ref.Typ = 'r')
             then
-               Crloc         := Xrefs.Table (Rnums (J)).Key.Loc;
-               Prevt         := Xrefs.Table (Rnums (J)).Key.Typ;
+               Loc           := Ref.Loc;
+               Prev_Typ      := Ref.Typ;
                Nrefs         := Nrefs + 1;
-               Rnums (Nrefs) := Rnums (J);
+               Rnums (Nrefs) := Rnums (Index);
             end if;
-         end loop;
-      end Eliminate_After_Sort;
-
-      --  Initialize loop
+         end;
+      end loop;
 
-      Cur_Scope_Idx  := 1;
-      From_Xref_Idx  := 1;
-      Cur_Entity     := Empty;
+      --  The two steps have eliminated all references, nothing to do
 
       if Alfa_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
-         Add_One_Xref : declare
-
-            -----------------------
-            -- Local Subprograms --
-            -----------------------
-
-            function Cur_Scope return Node_Id;
-            --  Return scope entity which corresponds to index Cur_Scope_Idx in
-            --  table Alfa_Scope_Table.
-
-            function Get_Entity_Type (E : Entity_Id) return Character;
-            --  Return a character representing the type of entity
-
-            function Is_Future_Scope_Entity (E : Entity_Id) return Boolean;
-            --  Check whether entity E is in Alfa_Scope_Table at index
-            --  Cur_Scope_Idx or higher.
-
-            function Is_Past_Scope_Entity (E : Entity_Id) return Boolean;
-            --  Check whether entity E is in Alfa_Scope_Table at index strictly
-            --  lower than Cur_Scope_Idx.
-
-            ---------------
-            -- Cur_Scope --
-            ---------------
-
-            function Cur_Scope return Node_Id is
-            begin
-               return Alfa_Scope_Table.Table (Cur_Scope_Idx).Scope_Entity;
-            end Cur_Scope;
-
-            ---------------------
-            -- Get_Entity_Type --
-            ---------------------
-
-            function Get_Entity_Type (E : Entity_Id) return Character is
-               C : Character;
-            begin
-               case Ekind (E) is
-                  when E_Out_Parameter    => C := '<';
-                  when E_In_Out_Parameter => C := '=';
-                  when E_In_Parameter     => C := '>';
-                  when others             => C := '*';
-               end case;
-               return C;
-            end Get_Entity_Type;
-
-            ----------------------------
-            -- Is_Future_Scope_Entity --
-            ----------------------------
-
-            function Is_Future_Scope_Entity (E : Entity_Id) return Boolean is
-            begin
-               for J in Cur_Scope_Idx .. Alfa_Scope_Table.Last loop
-                  if E = Alfa_Scope_Table.Table (J).Scope_Entity 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 (E));
-
-               return False;
-            end Is_Future_Scope_Entity;
-
-            --------------------------
-            -- Is_Past_Scope_Entity --
-            --------------------------
-
-            function Is_Past_Scope_Entity (E : Entity_Id) return Boolean is
-            begin
-               for J in Alfa_Scope_Table.First .. Cur_Scope_Idx - 1 loop
-                  if E = Alfa_Scope_Table.Table (J).Scope_Entity then
-                     return True;
-                  end if;
-               end loop;
-
-               return False;
-            end Is_Past_Scope_Entity;
-
-            ---------------------
-            -- Local Variables --
-            ---------------------
-
-            XE  : Xref_Entry renames Xrefs.Table (Rnums (Refno));
+         declare
+            Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
+            Ref       : Xref_Key   renames Ref_Entry.Key;
 
          begin
             --  If this assertion fails, the scope which we are looking for is
@@ -863,61 +791,58 @@ package body Alfa is
             --  construction of the scope table, or an erroneous scope for the
             --  current cross-reference.
 
-            pragma Assert (Is_Future_Scope_Entity (XE.Key.Ent_Scope));
+            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 XE.Key.Ent_Scope /= Cur_Scope then
-               Alfa_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
-                 From_Xref_Idx;
-               Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
-                 Alfa_Xref_Table.Last;
-               From_Xref_Idx := Alfa_Xref_Table.Last + 1;
+            if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
+               Update_Scope_Range
+                 (S    => Scope_Id,
+                  From => From_Index,
+                  To   => Alfa_Xref_Table.Last);
+
+               From_Index := Alfa_Xref_Table.Last + 1;
             end if;
 
-            while XE.Key.Ent_Scope /= Cur_Scope loop
-               Cur_Scope_Idx := Cur_Scope_Idx + 1;
-               pragma Assert (Cur_Scope_Idx <= Alfa_Scope_Table.Last);
+            while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
+               Scope_Id := Scope_Id + 1;
+               pragma Assert (Scope_Id <= Alfa_Scope_Table.Last);
             end loop;
 
-            if XE.Key.Ent /= Cur_Entity then
-               Cur_Entity_Name :=
-                 new String'(Unique_Name (XE.Key.Ent));
+            if Ref.Ent /= Ref_Id then
+               Ref_Name := new String'(Unique_Name (Ref.Ent));
             end if;
 
-            if XE.Key.Ent = Heap then
-               Alfa_Xref_Table.Append (
-                 (Entity_Name => Cur_Entity_Name,
-                  Entity_Line => 0,
-                  Etype       => Get_Entity_Type (XE.Key.Ent),
-                  Entity_Col  => 0,
-                  File_Num    => Dependency_Num (XE.Key.Lun),
-                  Scope_Num   => Get_Scope_Num (XE.Key.Ref_Scope),
-                  Line        => Int (Get_Logical_Line_Number (XE.Key.Loc)),
-                  Rtype       => XE.Key.Typ,
-                  Col         => Int (Get_Column_Number (XE.Key.Loc))));
-
+            if Ref.Ent = Heap then
+               Line := 0;
+               Col  := 0;
             else
-               Alfa_Xref_Table.Append (
-                 (Entity_Name => Cur_Entity_Name,
-                  Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
-                  Etype       => Get_Entity_Type (XE.Key.Ent),
-                  Entity_Col  => Int (Get_Column_Number (XE.Def)),
-                  File_Num    => Dependency_Num (XE.Key.Lun),
-                  Scope_Num   => Get_Scope_Num (XE.Key.Ref_Scope),
-                  Line        => Int (Get_Logical_Line_Number (XE.Key.Loc)),
-                  Rtype       => XE.Key.Typ,
-                  Col         => Int (Get_Column_Number (XE.Key.Loc))));
+               Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
+               Col  := Int (Get_Column_Number (Ref_Entry.Def));
             end if;
-         end Add_One_Xref;
+
+            Alfa_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        => Int (Get_Logical_Line_Number (Ref.Loc)),
+               Rtype       => Ref.Typ,
+               Col         => Int (Get_Column_Number (Ref.Loc))));
+         end;
       end loop;
 
       --  Update the range of cross references to which the scope refers to
 
-      Alfa_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx;
-      Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref   := Alfa_Xref_Table.Last;
+      Update_Scope_Range
+        (S    => Scope_Id,
+         From => From_Index,
+         To   => Alfa_Xref_Table.Last);
    end Add_Alfa_Xrefs;
 
    ------------------
@@ -1028,9 +953,7 @@ package body Alfa is
          Result := N;
       end if;
 
-      loop
-         exit when No (Result);
-
+      while Present (Result) loop
          case Nkind (Result) is
             when N_Package_Specification =>
                Result := Defining_Unit_Name (Result);
@@ -1105,36 +1028,69 @@ package body Alfa is
      (N   : Node_Id;
       Typ : Character := 'r')
    is
-      Indx      : Nat;
+      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);
+      Index     : Nat;
       Ref       : Source_Ptr;
       Ref_Scope : Entity_Id;
 
+   --  Start of processing for Generate_Dereference
+
    begin
-      Ref := Original_Location (Sloc (N));
+      Ref := Original_Location (Loc);
 
       if Ref > No_Location then
          Drefs.Increment_Last;
-         Indx := Drefs.Last;
+         Index := Drefs.Last;
+
+         declare
+            Deref_Entry : Xref_Entry renames Drefs.Table (Index);
+            Deref       : Xref_Key   renames Deref_Entry.Key;
+
+         begin
+            if No (Heap) then
+               Create_Heap;
+            end if;
 
-         Ref_Scope := Enclosing_Subprogram_Or_Package (N);
+            Ref_Scope := Enclosing_Subprogram_Or_Package (N);
 
-         --  Entity is filled later on with the special "Heap" variable
+            Deref.Ent := Heap;
+            Deref.Loc := Ref;
+            Deref.Typ := Typ;
 
-         Drefs.Table (Indx).Key.Ent := Empty;
+            --  It is as if the special "Heap" was defined in every scope where
+            --  it is referenced.
 
-         Drefs.Table (Indx).Def := No_Location;
-         Drefs.Table (Indx).Key.Loc := Ref;
-         Drefs.Table (Indx).Key.Typ := Typ;
+            Deref.Eun := Get_Source_Unit (Ref);
+            Deref.Lun := Get_Source_Unit (Ref);
 
-         --  It is as if the special "Heap" was defined in every scope where it
-         --  is referenced.
+            Deref.Ref_Scope := Ref_Scope;
+            Deref.Ent_Scope := Ref_Scope;
 
-         Drefs.Table (Indx).Key.Eun := Get_Source_Unit (Ref);
-         Drefs.Table (Indx).Key.Lun := Get_Source_Unit (Ref);
+            Deref_Entry.Def := No_Location;
 
-         Drefs.Table (Indx).Key.Ref_Scope := Ref_Scope;
-         Drefs.Table (Indx).Key.Ent_Scope := Ref_Scope;
-         Drefs.Table (Indx).Ent_Scope_File := Get_Source_Unit (Ref_Scope);
+            Deref_Entry.Ent_Scope_File := Get_Source_Unit (Ref_Scope);
+         end;
       end if;
    end Generate_Dereference;
 
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 0e8337f..d02420b 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1998-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-2012, 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- --
@@ -161,6 +161,9 @@ package body Lib.Xref is
    --  Local Subprograms --
    ------------------------
 
+   procedure Add_Entry (Key : Xref_Key; Ent_Scope_File : Unit_Number_Type);
+   --  Add an entry to the tables of Xref_Entries, avoiding duplicates
+
    procedure Generate_Prim_Op_References (Typ : Entity_Id);
    --  For a tagged type, generate implicit references to its primitive
    --  operations, for source navigation. This is done right before emitting
@@ -170,9 +173,6 @@ package body Lib.Xref is
    function Lt (T1, T2 : Xref_Entry) return Boolean;
    --  Order cross-references
 
-   procedure Add_Entry (Key : Xref_Key; Ent_Scope_File : Unit_Number_Type);
-   --  Add an entry to the tables of Xref_Entries, avoiding duplicates
-
    ---------------
    -- Add_Entry --
    ---------------
@@ -373,23 +373,17 @@ package body Lib.Xref is
       Set_Ref : Boolean   := True;
       Force   : Boolean   := False)
    is
-      Nod : Node_Id;
-      Ref : Source_Ptr;
-      Def : Source_Ptr;
-      Ent : Entity_Id;
-
-      Actual_Typ : Character := Typ;
-
-      Ref_Scope      : Entity_Id;
+      Actual_Typ     : Character := Typ;
+      Call           : Node_Id;
+      Def            : Source_Ptr;
+      Ent            : Entity_Id;
       Ent_Scope      : Entity_Id;
       Ent_Scope_File : Unit_Number_Type;
-
-      Call   : Node_Id;
-      Formal : Entity_Id;
-      --  Used for call to Find_Actual
-
-      Kind : Entity_Kind;
-      --  If Formal is non-Empty, then its Ekind, otherwise E_Void
+      Formal         : Entity_Id;
+      Kind           : Entity_Kind;
+      Nod            : Node_Id;
+      Ref            : Source_Ptr;
+      Ref_Scope      : Entity_Id;
 
       function Get_Through_Renamings (E : Entity_Id) return Entity_Id;
       --  Get the enclosing entity through renamings, which may come from
@@ -884,11 +878,13 @@ package body Lib.Xref is
          and then Sloc (E) > No_Location
          and then Sloc (N) > No_Location
 
-         --  We ignore references from within an instance, except for default
-         --  subprograms, for which we generate an implicit reference.
+         --  Ignore references from within an instance. The only exceptions to
+         --  this are default subprograms, for which we generate an implicit
+         --  reference.
 
          and then
-           (Instantiation_Location (Sloc (N)) = No_Location or else Typ = 'i')
+           (Instantiation_Location (Sloc (N)) = No_Location
+              or else Typ = 'i')
 
          --  Ignore dummy references
 
@@ -1003,14 +999,14 @@ package body Lib.Xref is
          Def := Original_Location (Sloc (Ent));
 
          if Actual_Typ = 'p'
-           and then Is_Subprogram (N)
-           and then Present (Overridden_Operation (N))
+           and then Is_Subprogram (Nod)
+           and then Present (Overridden_Operation (Nod))
          then
             Actual_Typ := 'P';
          end if;
 
          if Alfa_Mode then
-            Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (N);
+            Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (Nod);
             Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent);
 
             --  Since we are reaching through renamings in Alfa mode, we may
@@ -2434,6 +2430,8 @@ package body Lib.Xref is
       end Output_Refs;
    end Output_References;
 
+--  Start of elaboration for Lib.Xref
+
 begin
    --  Reset is necessary because Elmt_Ptr does not default to Null_Ptr,
    --  because it's not an access type.