[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)
commitd05586dce2ea2ac3bc6f645b7ad79290b327ccae
treeb791600e0a1e6ec7845a1b28bf2a695a7c61e95b
parentb67723ddeea0206e68f122a26b1a7b46382b79e7
[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
gcc/ada/ChangeLog
gcc/ada/exp_dbug.adb
gcc/ada/exp_dbug.ads
gcc/ada/frontend.adb
gcc/ada/sem_util.adb