projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a74d1bf) | patch
[Ada] Expand Enum_Rep attribute reference in GNATprove mode
authorYannick Moy <moy@adacore.com>
Tue, 9 Jul 2019 07:54:10 +0000 (07:54 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Jul 2019 07:54:10 +0000 (07:54 +0000)
commitdd9290ec5334de4426f4a510f4a32fd02e012f04
tree1f54e5a11b614ceeb8945d3f343e62788e98e341tree
parenta74d1bf6af0aaeb693cdbddf924c9af53f92b549commit | diff
[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
gcc/ada/ChangeLog diff | blob | history
gcc/ada/exp_spark.adb diff | blob | history