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 <m...@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.
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 (
