[Ada] Skip entity name qualification in GNATprove mode
authorYannick Moy <moy@adacore.com>
Wed, 18 Sep 2019 08:32:28 +0000 (08:32 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 18 Sep 2019 08:32:28 +0000 (08:32 +0000)
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

gcc/ada/ChangeLog
gcc/ada/exp_dbug.adb
gcc/ada/exp_dbug.ads
gcc/ada/frontend.adb
gcc/ada/sem_util.adb

index e77725c2c29a1ade3bb657b3774dc4669b4bf8c9..a6012fea00e60ad7c7330b657505bfc5703868c5 100644 (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.
index 3dbe9ad71519ec662b71a94808c63fd77dc02878..eb5e72b8ce7d3b11715896f0ec1e7770f5e8415e 100644 (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;
-
-         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;
 
@@ -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.
index 93b978378f9e5d4b4f4ad94bfc0c6eed654c80ce..b9f1fd6e7eb2f11b78e1f66e7d9a8f2764769037 100644 (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
index 2b3f377033cae5a4b4a8ba66b81c7dbc74ad5be1..1cc143a001245b088ba25c24b9374289cfd006b9 100644 (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.
index 99cdb8da0eb08c8b2892eda42e587fa73fd1c942..f66c77f71aebdf4c36c494d56ef490ea463aa9d4 100644 (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)