OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Skip entity name qualification in GNATprove mode 

GNATprove was using the qualification of names for entities with local
homonyms in the same scope, requiring the use of a suffix to
differentiate them. This caused problems for correctly identifying
primitive equality operators. This case is now handled like the rest of
entities in GNATprove, by instead updating Unique_Name to append the
suffix on-the-fly where needed.

There is no impact on compilation and hence no test.

2019-09-18  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* 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.

From-SVN: r275850
This commit is contained in:
Yannick Moy 2019-09-18 08:32:28 +00:00 committed by Pierre-Marie de Rodat
parent b67723ddee
commit d05586dce2
5 changed files with 91 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
gcc/ada/ChangeLog
View File

@ -1,3 +1,16 @@
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.

63
gcc/ada/exp_dbug.adb
View File

@ -219,26 +219,12 @@ package body Exp_Dbug is
begin
if Has_Homonym (E) then
declare
H : Entity_Id := Homonym (E);
Nr : Nat := 1;
if Homonym_Len > 0 then
Homonym_Len := Homonym_Len + 1;
Homonym_Numbers (Homonym_Len) := '_';
end if;
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;
Add_Nat_To_H (Nr);
end;
Add_Nat_To_H (Get_Homonym_Number (E));
end if;
end Append_Homonym_Number;
@ -1068,6 +1054,26 @@ package body Exp_Dbug is
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 --
------------------------------------
@ -1451,25 +1457,6 @@ package body Exp_Dbug is
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.

4
gcc/ada/exp_dbug.ads
View File

@ -460,6 +460,10 @@ package Exp_Dbug is
-- 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

4
gcc/ada/frontend.adb
View File

@ -492,7 +492,9 @@ begin
-- 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.

55
gcc/ada/sem_util.adb
View File

@ -33,6 +33,7 @@ with Elists; use Elists;
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;
@ -26154,24 +26155,59 @@ package body Sem_Util is
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
@ -26201,16 +26237,17 @@ package body Sem_Util is
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)