From 269428bb41d535ea6c42eb5f6e9382f2f1d45dfc Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 29 Oct 2012 12:42:17 +0100 Subject: [PATCH] [multiple changes] 2012-10-29 Thomas Quinot * xoscons.adb: Minor reformatting. 2012-10-29 Yannick Moy * 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 | 13 +++++++++++++ gcc/ada/exp_alfa.adb | 15 +++++++++------ gcc/ada/exp_dbug.adb | 14 ++++++++++++++ gcc/ada/xoscons.adb | 4 ++-- 4 files changed, 38 insertions(+), 8 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1154f3f..f69e62f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2012-10-29 Thomas Quinot + + * xoscons.adb: Minor reformatting. + +2012-10-29 Yannick Moy + + * 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 * gnat_rm.texi: Document that pragma Optimize_Alignment (Space) is diff --git a/gcc/ada/exp_alfa.adb b/gcc/ada/exp_alfa.adb index 1aac781..69a6e2b 100644 --- a/gcc/ada/exp_alfa.adb +++ b/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); diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index b1db585..bcf6111 100644 --- a/gcc/ada/exp_dbug.adb +++ b/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. diff --git a/gcc/ada/xoscons.adb b/gcc/ada/xoscons.adb index 4c58eba..fc78205 100644 --- a/gcc/ada/xoscons.adb +++ b/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 -- 2.7.4