diff mbox

[Ada] Use unique names in ALFA cross reference in ALI files

Message ID 20110804133140.GA8048@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 1:31 p.m. UTC 
The formal verification backend relies on unique names for the variables named
in ALFA sections of ALI files. Thus, generate these unique names with a new
function.

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

2011-08-04  Yannick Moy  <moy@adacore.com>

	* frontend.adb (Frontend): remove previous patch to avoid full
	qualification in ALFA mode.
	* lib-xref-alfa.adb (Add_ALFA_Xrefs): use unique name for variables.
	* sem_util.adb, sem_util.ads (Unique_Name): new function to define a
	unique name for an entity, which could be used to identify the entity
	across compilation units.
diff mbox

Patch

Index: frontend.adb
===================================================================
--- frontend.adb	(revision 177377)
+++ frontend.adb	(working copy)
@@ -372,11 +372,9 @@ 
    --  Qualify all entity names in inner packages, package bodies, etc.,
    --  except when compiling for the VM back-ends, which depend on having
    --  unqualified names in certain cases and handles the generation of
-   --  qualified names when needed, and when compiling for formal verification,
-   --  in which the back-end calls directly Qualify_All_Entity_Names after some
-   --  preprocessing which uses the non-qualified names.
+   --  qualified names when needed.
 
-   if VM_Target = No_VM and then not ALFA_Mode then
+   if VM_Target = No_VM then
       Exp_Dbug.Qualify_All_Entity_Names;
    end if;
 
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 177361)
+++ sem_util.adb	(working copy)
@@ -12201,6 +12201,22 @@ 
       end case;
    end Unique_Defining_Entity;
 
+   -----------------
+   -- Unique_Name --
+   -----------------
+
+   function Unique_Name (E : Entity_Id) return String is
+      Name : constant String := Get_Name_String (Chars (E));
+   begin
+      if Has_Fully_Qualified_Name (E)
+        or else E = Standard_Standard
+      then
+         return Name;
+      else
+         return Unique_Name (Scope (E)) & "__" & Name;
+      end if;
+   end Unique_Name;
+
    --------------------------
    -- Unit_Declaration_Node --
    --------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 177361)
+++ sem_util.ads	(working copy)
@@ -1372,6 +1372,10 @@ 
    --  Return the entity which represents declaration N, so that matching
    --  declaration and body have the same entity.
 
+   function Unique_Name (E : Entity_Id) return String;
+   --  Return a unique name for entity E, which could be used to identify E
+   --  across compilation units.
+
    function Unit_Declaration_Node (Unit_Id : Entity_Id) return Node_Id;
    --  Unit_Id is the simple name of a program unit, this function returns the
    --  corresponding xxx_Declaration node for the entity. Also applies to the
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb	(revision 177382)
+++ lib-xref-alfa.adb	(working copy)
@@ -738,7 +738,7 @@ 
 
             if XE.Ent /= Cur_Entity then
                Cur_Entity_Name :=
-                 new String'(Exact_Source_Name (Sloc (XE.Ent)));
+                 new String'(Unique_Name (XE.Ent));
             end if;
 
             ALFA_Xref_Table.Append (