Expansion of Enum_Rep in GNATprove is meant to be a subset of the
expansion in GNAT, so it needs to be kept in sync with the frontend.
Semantics of the compiler is not affected.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-08 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Port
changes in frontend expander.--- gcc/ada/exp_spark.adb
+++ 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;
