| commit | cbb0b55385692dca6898a2668766f17ea42c4d2e | |
| author | Yannick Moy <moy@adacore.com> | |
| Tue, 17 Sep 2019 08:01:10 +0000 (17 08:01 +0000) | ||
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | |
| Tue, 17 Sep 2019 08:01:10 +0000 (17 08:01 +0000) | ||
| tree | 713135b4be8b9de962ed05acc58babf7ed7a5a1f | treesnapshot (tar.gz zip) |
| parent | a9a08e6d331cb454741d2b089cdedaefedfd5271 | commitdiff |
[Ada] Do not inline dispatching operations in GNATprove mode
In GNATprove, local subprograms without contracts are candidates for
inlining, so that they are only analyzed in the context of their calls.
This does not apply to dispatching operations, which may be called
through dispatching, in an unknown calling context. Hence such
operations should not be considered as candidates for inlining.
There is no test as this has no effect on compilation.
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling
for dispatching operations.
From-SVN: r275779
In GNATprove, local subprograms without contracts are candidates for
inlining, so that they are only analyzed in the context of their calls.
This does not apply to dispatching operations, which may be called
through dispatching, in an unknown calling context. Hence such
operations should not be considered as candidates for inlining.
There is no test as this has no effect on compilation.
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling
for dispatching operations.
From-SVN: r275779
| gcc/ada/ChangeLog | diffblobblamehistory | |
| gcc/ada/inline.adb | diffblobblamehistory |