+2019-09-18 Yannick Moy <moy@adacore.com>
+
+ * exp_dbug.adb (Append_Homonym_Number): Use new function
+ Get_Homonym_Number.
+ (Get_Homonym_Number): New function to return the homonym number.
+ (Qualify_Entity_Name): Remove special case for GNATprove.
+ * exp_dbug.ads (Get_Homonym_Number): Make the new function
+ public for use in GNATprove.
+ * frontend.adb (Frontend): Do not qualify names in GNATprove
+ mode.
+ * sem_util.adb (Unique_Name): Append homonym suffix where needed
+ for entities which have local homonyms in the same scope.
+
2019-09-18 Nicolas Roche <roche@adacore.com>
* libgnat/s-valrea.adb (Scan_Integral_Digits): New procedure.
begin
if Has_Homonym (E) then
- declare
- H : Entity_Id := Homonym (E);
- Nr : Nat := 1;
-
- begin
- while Present (H) loop
- if Scope (H) = Scope (E) then
- Nr := Nr + 1;
- end if;
-
- H := Homonym (H);
- end loop;
-
- if Homonym_Len > 0 then
- Homonym_Len := Homonym_Len + 1;
- Homonym_Numbers (Homonym_Len) := '_';
- end if;
+ if Homonym_Len > 0 then
+ Homonym_Len := Homonym_Len + 1;
+ Homonym_Numbers (Homonym_Len) := '_';
+ end if;
- Add_Nat_To_H (Nr);
- end;
+ Add_Nat_To_H (Get_Homonym_Number (E));
end if;
end Append_Homonym_Number;
end loop;
end Build_Subprogram_Instance_Renamings;
+ ------------------------
+ -- Get_Homonym_Number --
+ ------------------------
+
+ function Get_Homonym_Number (E : Entity_Id) return Nat is
+ H : Entity_Id := Homonym (E);
+ Nr : Nat := 1;
+
+ begin
+ while Present (H) loop
+ if Scope (H) = Scope (E) then
+ Nr := Nr + 1;
+ end if;
+
+ H := Homonym (H);
+ end loop;
+
+ return Nr;
+ end Get_Homonym_Number;
+
------------------------------------
-- Get_Secondary_DT_External_Name --
------------------------------------
if Has_Qualified_Name (Ent) then
return;
- -- 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 GNATprove_Mode then
- if Has_Homonym (Ent) then
- Get_Name_String (Chars (Ent));
- Append_Homonym_Number (Ent);
- Output_Homonym_Numbers_Suffix;
- 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
-- renaming, then the qualified name of the entity associated with the
-- renamed object can now be incorporated in the debug name.
-- Subprograms for Handling Qualification --
--------------------------------------------
+ function Get_Homonym_Number (E : Entity_Id) return Nat;
+ -- Return the homonym number for E, which is its position in the homonym
+ -- chain starting at 1. This is exported for use in GNATprove.
+
procedure Qualify_Entity_Names (N : Node_Id);
-- Given a node N, that represents a block, subprogram body, or package
-- body or spec, or protected or task type, sets a fully qualified name
-- Qualify all entity names in inner packages, package bodies, etc
- Exp_Dbug.Qualify_All_Entity_Names;
+ if not GNATprove_Mode then
+ Exp_Dbug.Qualify_All_Entity_Names;
+ end if;
-- SCIL backend requirement. Check that SCIL nodes associated with
-- dispatching calls reference subprogram calls.
with Errout; use Errout;
with Erroutc; use Erroutc;
with Exp_Ch11; use Exp_Ch11;
+with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
function Unique_Name (E : Entity_Id) return String is
- -- Names in E_Subprogram_Body or E_Package_Body entities are not
- -- reliable, as they may not include the overloading suffix. Instead,
- -- when looking for the name of E or one of its enclosing scope, we get
- -- the name of the corresponding Unique_Entity.
+ -- Local subprograms
- U : constant Entity_Id := Unique_Entity (E);
+ function Add_Homonym_Suffix (E : Entity_Id) return String;
function This_Name return String;
+ ------------------------
+ -- Add_Homonym_Suffix --
+ ------------------------
+
+ function Add_Homonym_Suffix (E : Entity_Id) return String is
+
+ -- Names in E_Subprogram_Body or E_Package_Body entities are not
+ -- reliable, as they may not include the overloading suffix.
+ -- Instead, when looking for the name of E or one of its enclosing
+ -- scope, we get the name of the corresponding Unique_Entity.
+
+ U : constant Entity_Id := Unique_Entity (E);
+ Nam : constant String := Get_Name_String (Chars (U));
+
+ begin
+ -- If E has homonyms but is not fully qualified, as done in
+ -- GNATprove mode, append the homonym number on the fly. Strip the
+ -- leading space character in the image of natural numbers. Also do
+ -- not print the homonym value of 1.
+
+ if Has_Homonym (U) then
+ declare
+ N : constant Nat := Get_Homonym_Number (U);
+ S : constant String := N'Img;
+ begin
+ if N > 1 then
+ return Nam & "__" & S (2 .. S'Last);
+ end if;
+ end;
+ end if;
+
+ return Nam;
+ end Add_Homonym_Suffix;
+
---------------
-- This_Name --
---------------
function This_Name return String is
begin
- return Get_Name_String (Chars (U));
+ return Add_Homonym_Suffix (E);
end This_Name;
+ -- Local variables
+
+ U : constant Entity_Id := Unique_Entity (E);
+
-- Start of processing for Unique_Name
begin
end if;
-- For intances of generic subprograms use the name of the related
- -- instace and skip the scope of its wrapper package.
+ -- instance and skip the scope of its wrapper package.
elsif Is_Wrapper_Package (S) then
pragma Assert (Scope (S) = Scope (Related_Instance (S)));
-- Wrapper package and the instantiation are in the same scope
declare
+ Related_Name : constant String :=
+ Add_Homonym_Suffix (Related_Instance (S));
Enclosing_Name : constant String :=
- Unique_Name (Scope (S)) & "__" &
- Get_Name_String (Chars (Related_Instance (S)));
+ Unique_Name (Scope (S)) & "__" & Related_Name;
begin
if Is_Subprogram (U)