[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 07166c6b3ea157f2b5237043185e806188c72335..f6ce93123eeacceeca21b2ca548e7da28d7da2f3 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+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

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 63f2dad209a9e31022ea99f61d5d70ca588a7e2d..d6ed3d44b1dc56d0a368a948f812fe012b212898 100644 (file)
--- a/gcc/ada/exp_spark.adb
+++ b/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.