[gcc(refs/users/guojiufu/heads/personal-branch)] [Ada] Port a modified expansion of Enum_Rep from GNAT to GNATprove

[Jiu Fu Guo]

https://gcc.gnu.org/g:5351d617ec82bc2795a514e9de815484fb8cd0fc

commit 5351d617ec82bc2795a514e9de815484fb8cd0fc
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Mon Feb 17 18:00:41 2020 +0100

    [Ada] Port a modified expansion of Enum_Rep from GNAT to GNATprove
    
    2020-06-08  Piotr Trojanek  <trojanek@adacore.com>
    
    gcc/ada/
    
            * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Port
            changes in frontend expander.

Diff:
---
 gcc/ada/exp_spark.adb | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index a54a16235a8..c115a453228 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -200,7 +200,8 @@ package body Exp_SPARK is
          Analyze_And_Resolve (N, Typ);
 
       --  Whenever possible, replace a prefix which is an enumeration literal
-      --  by the corresponding literal value.
+      --  by the corresponding literal value, just like it happens in the GNAT
+      --  expander.
 
       elsif Attr_Id = Attribute_Enum_Rep then
          declare
@@ -215,15 +216,7 @@ package body Exp_SPARK is
             --  If the argument is a literal, expand it
 
             if Nkind (Expr) in N_Has_Entity
-              and then
-                (Ekind (Entity (Expr)) = E_Enumeration_Literal
-                 or else
-                   (Nkind (Expr) in N_Has_Entity
-                    and then Ekind (Entity (Expr)) = E_Constant
-                    and then Present (Renamed_Object (Entity (Expr)))
-                    and then Is_Entity_Name (Renamed_Object (Entity (Expr)))
-                    and then Ekind (Entity (Renamed_Object (Entity (Expr)))) =
-                      E_Enumeration_Literal))
+              and then Ekind (Entity (Expr)) = E_Enumeration_Literal
             then
                Exp_Attr.Expand_N_Attribute_Reference (N);
             end if;