diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-09 07:54:10 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-09 07:54:10 +0000 |
| commit | dd9290ec5334de4426f4a510f4a32fd02e012f04 (patch) | |
| tree | 1f54e5a11b614ceeb8945d3f343e62788e98e341 /gcc/ada | |
| parent | a74d1bf6af0aaeb693cdbddf924c9af53f92b549 (diff) | |
| download | gcc-dd9290ec5334de4426f4a510f4a32fd02e012f04.zip gcc-dd9290ec5334de4426f4a510f4a32fd02e012f04.tar.gz gcc-dd9290ec5334de4426f4a510f4a32fd02e012f04.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/exp_spark.adb | 7 |
2 files changed, 12 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c80c9e4..948d0fa 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 b008c79..58f9243 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. |