diff options
| author | Yannick Moy <moy@adacore.com> | 2024-04-23 13:16:51 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-06-13 15:30:29 +0200 |
| commit | df9d6153e1981676b08109fbe3371ca6e9d5f755 (patch) | |
| tree | a5d32939469266cf1f0cec304aa6b3ea871aba8c /gcc/cp/parser.cc | |
| parent | 2afa7fd8c6d32264d4d3d917318fbac9f7f38508 (diff) | |
| download | gcc-df9d6153e1981676b08109fbe3371ca6e9d5f755.zip gcc-df9d6153e1981676b08109fbe3371ca6e9d5f755.tar.gz gcc-df9d6153e1981676b08109fbe3371ca6e9d5f755.tar.bz2 | |
ada: Do not inline subprogram which could cause SPARK violation
Inlining in GNATprove a subprogram containing a constant declaration with
an address clause/aspect might lead to a spurious error if the address
expression is based on a constant view of a mutable object at call site.
Do not allow such inlining in GNATprove.
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
when constant with address clause is found.
Diffstat (limited to 'gcc/cp/parser.cc')
0 files changed, 0 insertions, 0 deletions