diff mbox

[Ada] Deal with references for Alfa mode through multiple renamings

Message ID 20110919083251.GA16377@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 19, 2011, 8:32 a.m. UTC
Get the enclosing entity through possible multiple renamings, not only once, 
which may come from source or from the translation of generic instantiations.
Only for the Alfa mode for formal verification.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-19  Yannick Moy  <moy@adacore.com>

	* lib-xref.adb (Generate_Reference): Take into account multiple
	renamings for Alfa refs.
diff mbox

Patch

Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 178956)
+++ lib-xref.adb	(working copy)
@@ -391,6 +391,10 @@ 
       Kind : Entity_Kind;
       --  If Formal is non-Empty, then its Ekind, otherwise E_Void
 
+      function Get_Through_Renamings (E : Entity_Id) return Entity_Id;
+      --  Get the enclosing entity through renamings, which may come from
+      --  source or from the translation of generic instantiations.
+
       function Is_On_LHS (Node : Node_Id) return Boolean;
       --  Used to check if a node is on the left hand side of an assignment.
       --  The following cases are handled:
@@ -412,6 +416,22 @@ 
       --  exceptions where we do not want to set this flag, see body for
       --  details of these exceptional cases.
 
+      ---------------------------
+      -- Get_Through_Renamings --
+      ---------------------------
+
+      function Get_Through_Renamings (E : Entity_Id) return Entity_Id is
+         Result : Entity_Id := E;
+      begin
+         while Present (Result)
+           and then Is_Object (Result)
+           and then Present (Renamed_Object (Result))
+         loop
+            Result := Get_Enclosing_Object (Renamed_Object (Result));
+         end loop;
+         return Result;
+      end Get_Through_Renamings;
+
       ---------------
       -- Is_On_LHS --
       ---------------
@@ -955,11 +975,8 @@ 
          --  the renaming, which is needed to compute a valid set of effects
          --  (reads, writes) for the enclosing subprogram.
 
-         if Alfa_Mode
-           and then Is_Object (Ent)
-           and then Present (Renamed_Object (Ent))
-         then
-            Ent := Get_Enclosing_Object (Renamed_Object (Ent));
+         if Alfa_Mode then
+            Ent := Get_Through_Renamings (Ent);
 
             --  If no enclosing object, then it could be a reference to any
             --  location not tracked individually, like heap-allocated data.