diff options
| author | Yannick Moy <moy@adacore.com> | 2023-07-21 06:43:10 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-08-01 10:06:45 +0200 |
| commit | 2c59b33838e796694f347bf4588351d25e4c3a6a (patch) | |
| tree | e165d6f34a3054c570dfce81e0864928c62840eb /gcc/tree-cfg.cc | |
| parent | 77604913b73e35b1b7f38725c526ac558ff165be (diff) | |
| download | gcc-2c59b33838e796694f347bf4588351d25e4c3a6a.zip gcc-2c59b33838e796694f347bf4588351d25e4c3a6a.tar.gz gcc-2c59b33838e796694f347bf4588351d25e4c3a6a.tar.bz2 | |
ada: Disable inlining of subprograms with Skip(_Flow_And)_Proof in GNATprove
Subprograms with these Skip(_Flow_And)_Proof annotations should not be
inlined in GNATprove, as we want to skip part of the analysis for their
body.
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check for
Skip_Proof and Skip_Flow_And_Proof annotations for deciding
whether a subprogram can be inlined.
Diffstat (limited to 'gcc/tree-cfg.cc')
0 files changed, 0 insertions, 0 deletions