[multiple changes]

2012-10-29  Thomas Quinot  <quinot@adacore.com>

	* xoscons.adb: Minor reformatting.

2012-10-29  Yannick Moy  <moy@adacore.com>

	* exp_alfa.adb (Expand_Alfa): Backtrack change that removed
	qualification of names in formal verification mode. Instead,
	the qualification should be modified.
	* exp_dbug.adb (Qualify_Entity_Name): Modify qualification in formal
	verification mode, so that only a suffix is added to distinguish
	homonyms from the same scope.

From-SVN: r192940

gcc/ada/ChangeLog

@@ -1,3 +1,16 @@
+2012-10-29  Thomas Quinot  <quinot@adacore.com>
+
+	* xoscons.adb: Minor reformatting.
+
+2012-10-29  Yannick Moy  <moy@adacore.com>
+
+	* exp_alfa.adb (Expand_Alfa): Backtrack change that removed
+	qualification of names in formal verification mode. Instead,
+	the qualification should be modified.
+	* exp_dbug.adb (Qualify_Entity_Name): Modify qualification in formal
+	verification mode, so that only a suffix is added to distinguish
+	homonyms from the same scope.
+
 2012-10-29  Robert Dewar  <dewar@adacore.com>
 
 	* gnat_rm.texi: Document that pragma Optimize_Alignment (Space) is

gcc/ada/exp_alfa.adb

@@ -28,6 +28,7 @@ with Einfo;    use Einfo;
 with Exp_Attr; use Exp_Attr;
 with Exp_Ch4;  use Exp_Ch4;
 with Exp_Ch6;  use Exp_Ch6;
+with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
 with Nlists;   use Nlists;
 with Rtsfind;  use Rtsfind;
@@ -80,17 +81,19 @@ package body Exp_Alfa is
          when N_Attribute_Reference =>
             Expand_Alfa_N_Attribute_Reference (N);
 
-         --  Note: we used to qualify entity names in the following constructs
-         --  (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.
+         --  Qualification of entity names in formal verification mode
+         --  is limited to the addition of a suffix for homonyms (see
+         --  Exp_Dbug.Qualify_Entity_Name). 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.
 
          when N_Block_Statement     |
               N_Package_Body        |
               N_Package_Declaration |
               N_Subprogram_Body     =>
-            null;
+            Qualify_Entity_Names (N);
 
          when N_Subprogram_Call     =>
             Expand_Alfa_Call (N);

gcc/ada/exp_dbug.adb

@@ -1307,6 +1307,20 @@ package body Exp_Dbug is
       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.
+
+      elsif Alfa_Mode then
+         Get_Name_String (Chars (Ent));
+         Append_Homonym_Number (Ent);
+         Output_Homonym_Numbers_Suffix;
+         Set_Chars (Ent, Name_Enter);
+         return;
+
       --  If the entity is a variable encoding the debug name for an object
       --  renaming, then the qualified name of the entity associated with the
       --  renamed object can now be incorporated in the debug name.

gcc/ada/xoscons.adb

@@ -314,8 +314,8 @@ procedure XOSCons is
         (S : String;
          K : Asm_Int_Kind) return Int_Value_Type
       is
-         First    : Integer := S'First;
-         Result   : Int_Value_Type;
+         First  : Integer := S'First;
+         Result : Int_Value_Type;
 
       begin
          --  On some platforms, immediate integer values are prefixed with