projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c7199fb) | patch
[Ada] Fix expansion of "for X of Y loop" in GNATprove
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 8 Apr 2020 21:38:51 +0000 (23:38 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 17 Jun 2020 08:13:58 +0000 (04:13 -0400)
commit6be763897bcabab90eeae0dfda963531802a4ae9
treee8c528e0082e2ccbd0e945ca96dc1eacc3ea3106tree
parentc7199fb6e694d1a0964351200648c24c3ee97973commit | diff
[Ada] Fix expansion of "for X of Y loop" in GNATprove

2020-06-17  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

* sem_ch5.adb (Analyze_Iterator_Specification): Enable expansion
that creates a renaming that removes side effects from the
iterated object in the GNATprove mode; then analyze reference to
this renaming (it is required for GNATprove and harmless for
GNAT).
gcc/ada/sem_ch5.adb diff | blob | history