diff mbox

[Ada] Correct references in Alfa mode for use of renamings

Message ID 20110919082259.GA11481@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 19, 2011, 8:22 a.m. UTC 
In Alfa mode, consider the underlying entity renamed instead of the renaming
for the reference, because the latter is needed to compute a valid set of
effects for the enclosing subprogram. If no such enclosing object, then it
could be a reference to any location not tracked individually, like
heap-allocated data. Conservatively approximate this possibility by generating
a reference to the special HEAP variable.

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

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

	* lib-xref.adb (Generate_Reference): Change entity referenced
	to underlying object if any, or else reference to the HEAP.
diff mbox

Patch

Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 178955)
+++ lib-xref.adb	(working copy)
@@ -951,6 +951,33 @@ 
             return;
          end if;
 
+         --  In Alfa mode, consider the underlying entity renamed instead of
+         --  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 no enclosing object, then it could be a reference to any
+            --  location not tracked individually, like heap-allocated data.
+            --  Conservatively approximate this possibility by generating a
+            --  dereference, and return.
+
+            if No (Ent) then
+               if Actual_Typ = 'w' then
+                  Alfa.Generate_Dereference (Nod, 'r');
+                  Alfa.Generate_Dereference (Nod, 'w');
+               else
+                  Alfa.Generate_Dereference (Nod, 'r');
+               end if;
+
+               return;
+            end if;
+         end if;
+
          --  Record reference to entity
 
          Ref := Original_Location (Sloc (Nod));