diff mbox

[Ada] Correct possible double qualification of names in formal mode

Message ID 20121106094930.GA4055@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 6, 2012, 9:49 a.m. UTC 
In the special mode for formal verification, the entity was not marked as
having a qualified name after being passed to Qualify_Entity_Name, which lead
to multiple qualification when Qualify_Entity_Name was called multiple times
on the same entity. The assumptions that it is called only once on each entity
is wrong, because scopes (containing entities) may be put more than once on
the qualification stack, once every time they are expanded, and expansion may
be called multiple times on the same node. The fact that names are marked as
qualified does not break the behavior of Unique_Name to fully qualify names
based on scope names, because this function looks at the other flag
Has_Fully_Qualified_Name, not set in formal verification mode.

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

2012-11-06  Yannick Moy  <moy@adacore.com>

	* exp_dbug.adb (Qualify_Entity_Name): Mark entity as having a qualified
	name after being treated, in formal verification mode.
diff mbox

Patch

Index: exp_dbug.adb
===================================================================
--- exp_dbug.adb	(revision 193208)
+++ exp_dbug.adb	(working copy)
@@ -1307,12 +1307,13 @@ 
       if Has_Qualified_Name (Ent) then
          return;
 
-      --  In formal verification mode, simply append a suffix for homonyms, but
-      --  do not mark the name as being qualified. We used to qualify entity
-      --  names as full expansion does, but this was removed as this prevents
-      --  the verification back-end from using a short name for debugging and
-      --  user interaction. The verification back-end already takes care of
-      --  qualifying names when needed.
+      --  In formal verification mode, simply append a suffix for homonyms.
+      --  We used to qualify entity names as full expansion does, but this was
+      --  removed as this prevents the verification back-end from using a short
+      --  name for debugging and user interaction. The verification back-end
+      --  already takes care of qualifying names when needed. Still mark the
+      --  name as being qualified, as Qualify_Entity_Name may be called more
+      --  than once on the same entity.
 
       elsif Alfa_Mode then
          if Has_Homonym (Ent) then
@@ -1322,6 +1323,7 @@ 
             Set_Chars (Ent, Name_Enter);
          end if;
 
+         Set_Has_Qualified_Name (Ent);
          return;
 
       --  If the entity is a variable encoding the debug name for an object