In the special GNATprove mode for proof of programs, expand the Enum_Rep
attribute reference so that a suitable static integer is in the AST
where required by the rest of analysis.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-09 Yannick Moy <m...@adacore.com>
gcc/ada/
* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
attribute reference on Enum_Rep.--- gcc/ada/exp_spark.adb
+++ gcc/ada/exp_spark.adb
@@ -26,6 +26,7 @@
with Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
+with Exp_Attr;
with Exp_Ch4;
with Exp_Ch5; use Exp_Ch5;
with Exp_Dbug; use Exp_Dbug;
@@ -196,6 +197,12 @@ package body Exp_SPARK is
Parameter_Associations => New_List (Expr)));
Analyze_And_Resolve (N, Typ);
+ -- Whenever possible, replace a prefix which is an enumeration literal
+ -- by the corresponding literal value.
+
+ elsif Attr_Id = Attribute_Enum_Rep then
+ Exp_Attr.Expand_N_Attribute_Reference (N);
+
-- For attributes which return Universal_Integer, introduce a conversion
-- to the expected type with the appropriate check flags set.
