aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-08-12 08:59:37 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-08-12 08:59:37 +0000
commit08c8696d4884425839fc5cd14a8788fe53f031e4 (patch)
treec73fa96b43f78ae4049239e197a1d844430813d4
parent33defa7c6c36c0671b81b4785fbb250430a4a953 (diff)
downloadgcc-08c8696d4884425839fc5cd14a8788fe53f031e4.zip
gcc-08c8696d4884425839fc5cd14a8788fe53f031e4.tar.gz
gcc-08c8696d4884425839fc5cd14a8788fe53f031e4.tar.bz2
[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
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/exp_spark.adb26
2 files changed, 30 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 07166c6..f6ce931 100644
--- 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 63f2dad..d6ed3d4 100644
--- 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.