projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 60f66f3) | patch
[Ada] Fix inlining of subprograms with deep param/result in GNATprove
authorYannick Moy <moy@adacore.com>
Thu, 10 Oct 2019 15:25:22 +0000 (15:25 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 10 Oct 2019 15:25:22 +0000 (15:25 +0000)
commit5913d1b7c060ba061e912850bec290c83b06c7aa
tree820bcdf330f8f41adf461a456fef6f56a9de3a81tree
parent60f66f34a669f4f15c2fc178d95f12b081f83005commit | diff
[Ada] Fix inlining of subprograms with deep param/result in GNATprove

2019-10-10  Yannick Moy  <moy@adacore.com>

gcc/ada/

* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not peek
under private types whose completion is SPARK_Mode Off.

From-SVN: r276833
gcc/ada/ChangeLog diff | blob | history
gcc/ada/inline.adb diff | blob | history