[Ada] SPARK: disable expansion of Enum_Rep

Disable expansion of Enum_Rep into a type conversion as it is incorrect
in SPARK.

2019-08-12  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Only
	expand Enum_Rep attribute when its parameter is a literal.

From-SVN: r274289

gcc/ada/ChangeLog

+2019-08-12  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Only
+	expand Enum_Rep attribute when its parameter is a literal.
+
 2019-08-12  Justin Squirek  <squirek@adacore.com>
 
 	* sem_eval.adb (Check_Non_Static_Context): Add a condition to

gcc/ada/exp_spark.adb

@@ -201,7 +201,31 @@ package body Exp_SPARK is
       --  by the corresponding literal value.
 
       elsif Attr_Id = Attribute_Enum_Rep then
-         Exp_Attr.Expand_N_Attribute_Reference (N);
+         declare
+            Exprs : constant List_Id := Expressions (N);
+         begin
+            if Is_Non_Empty_List (Exprs) then
+               Expr := First (Exprs);
+            else
+               Expr := Prefix (N);
+            end if;
+
+            --  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))
+            then
+               Exp_Attr.Expand_N_Attribute_Reference (N);
+            end if;
+         end;
 
       --  For attributes which return Universal_Integer, introduce a conversion
       --  to the expected type with the appropriate check flags set.