diff options
| author | Yannick Moy <moy@adacore.com> | 2019-09-19 08:14:03 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-09-19 08:14:03 +0000 |
| commit | 231ef54b96d6022bc844107f50490ba5c96f4a50 (patch) | |
| tree | 34ead3fe4f6594bef2dbb93f2dce6de0f53bf2fa /gcc/tree-vectorizer.h | |
| parent | 09709b4781192f7724e2bb2977d3610ae727260f (diff) | |
| download | gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.zip gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.tar.gz gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.tar.bz2 | |
[Ada] Disable inlining of traversal function in GNATprove
Traversal functions as defined in SPARK RM 3.10 should not be inlined
for analysis in GNATprove, as this changes the ownership behavior.
Disable the inlining performed in GNATprove on functions which could be
interpreted as such.
There is no impact on compilation and thus no test.
2019-09-19 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add special
case for traversal functions.
From-SVN: r275948
Diffstat (limited to 'gcc/tree-vectorizer.h')
0 files changed, 0 insertions, 0 deletions