From: Yannick Moy <moy@adacore.com>
Date: Tue, 9 Jul 2019 07:54:10 +0000 (+0000)
Subject: [Ada] Expand Enum_Rep attribute reference in GNATprove mode
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd9290ec5334de4426f4a510f4a32fd02e012f04;p=gcc.git

[Ada] Expand Enum_Rep attribute reference in GNATprove mode

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.

2019-07-09  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
	attribute reference on Enum_Rep.

From-SVN: r273276
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c80c9e46f23..948d0fa30d1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-09  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
+	attribute reference on Enum_Rep.
+
 2019-07-09  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch12.adb (Instantiate_Formal_Package): Handle properly the
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index b008c793e3d..58f924376a7 100644
--- a/gcc/ada/exp_spark.adb
+++ b/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.