Commit dd9290ec by Yannick Moy Committed by Pierre-Marie de Rodat

[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
parent a74d1bf6
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> 2019-07-09 Ed Schonberg <schonberg@adacore.com>
* sem_ch12.adb (Instantiate_Formal_Package): Handle properly the * sem_ch12.adb (Instantiate_Formal_Package): Handle properly the
......
...@@ -26,6 +26,7 @@ ...@@ -26,6 +26,7 @@
with Atree; use Atree; with Atree; use Atree;
with Checks; use Checks; with Checks; use Checks;
with Einfo; use Einfo; with Einfo; use Einfo;
with Exp_Attr;
with Exp_Ch4; with Exp_Ch4;
with Exp_Ch5; use Exp_Ch5; with Exp_Ch5; use Exp_Ch5;
with Exp_Dbug; use Exp_Dbug; with Exp_Dbug; use Exp_Dbug;
...@@ -196,6 +197,12 @@ package body Exp_SPARK is ...@@ -196,6 +197,12 @@ package body Exp_SPARK is
Parameter_Associations => New_List (Expr))); Parameter_Associations => New_List (Expr)));
Analyze_And_Resolve (N, Typ); 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 -- For attributes which return Universal_Integer, introduce a conversion
-- to the expected type with the appropriate check flags set. -- to the expected type with the appropriate check flags set.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment