diff mbox

[Ada] Correct unique name of entities for formal verification

Message ID 20110805155035.GA27802@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 5, 2011, 3:50 p.m. UTC 
As some entities end up with an unqualified name, for example for the
declaration of a library-level subprogram, the name given by Unique_Name should
match the qualified name. Now corrected.

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

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

	* sem_util.adb (Unique_Name): only prefix with "standard" the names of
	entities directly in package Standard, otherwise skip the standard
	prefix.
diff mbox

Patch

Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 177448)
+++ sem_util.adb	(working copy)
@@ -12357,14 +12357,37 @@ 
    -----------------
 
    function Unique_Name (E : Entity_Id) return String is
-      Name : constant String := Get_Name_String (Chars (E));
+
+      function Get_Scoped_Name (E : Entity_Id) return String;
+      --  Return the name of E prefixed by all the names of the scopes to which
+      --  E belongs, except for Standard.
+
+      ---------------------
+      -- Get_Scoped_Name --
+      ---------------------
+
+      function Get_Scoped_Name (E : Entity_Id) return String is
+         Name : constant String := Get_Name_String (Chars (E));
+      begin
+         if Has_Fully_Qualified_Name (E)
+           or else Scope (E) = Standard_Standard
+         then
+            return Name;
+         else
+            return Get_Scoped_Name (Scope (E)) & "__" & Name;
+         end if;
+      end Get_Scoped_Name;
+
    begin
-      if Has_Fully_Qualified_Name (E)
-        or else E = Standard_Standard
-      then
-         return Name;
+      if E = Standard_Standard then
+         return Get_Name_String (Name_Standard);
+
+      elsif Scope (E) = Standard_Standard then
+         return Get_Name_String (Name_Standard) & "__" &
+           Get_Name_String (Chars (E));
+
       else
-         return Unique_Name (Scope (E)) & "__" & Name;
+         return Get_Scoped_Name (E);
       end if;
    end Unique_Name;
 
@@ -12478,7 +12501,7 @@ 
    --  Start of processing for Unit_Is_Visible
 
    begin
-      --  The currrent unit is directly visible.
+      --  The currrent unit is directly visible
 
       if Curr = U then
          return True;
@@ -12486,7 +12509,7 @@ 
       elsif Unit_In_Context (Curr) then
          return True;
 
-      --  If the current unit is a body, check the context of the spec.
+      --  If the current unit is a body, check the context of the spec
 
       elsif Nkind (Unit (Curr)) = N_Package_Body
         or else
@@ -12498,7 +12521,7 @@ 
          end if;
       end if;
 
-      --  If the spec is a child unit, examine the parents.
+      --  If the spec is a child unit, examine the parents
 
       if Is_Child_Unit (Curr_Entity) then
          if Nkind (Unit (Curr)) in N_Unit_Body then
@@ -12670,7 +12693,7 @@ 
             if Comes_From_Source (Expec_Type) then
                Matching_Field := Expec_Type;
 
-            --  For an assignment, use name of target.
+            --  For an assignment, use name of target
 
             elsif Nkind (Parent (Expr)) = N_Assignment_Statement
               and then Is_Entity_Name (Name (Parent (Expr)))