]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48d7a59) | patch
ada: Prevent inlining in GNATprove for memory leaks
authorYannick Moy <moy@adacore.com>
Wed, 13 Dec 2023 16:40:03 +0000 (17:40 +0100)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 6 May 2024 09:11:25 +0000 (11:11 +0200)
commitcdf15b4b661c5fa1a210642e0b2a508969faf197
treea28c6c59671691b07b02721070fd9f0b5b640e82tree
parent48d7a599ecd141f7936deff6170dd5199edb2d98commit | diff
ada: Prevent inlining in GNATprove for memory leaks

In some cases, inlining a call in GNATprove could lead to
missing a memory leak. Recognize such cases and do not inline
such calls.

gcc/ada/

* inline.adb (Call_Can_Be_Inlined_In_GNATprove_Mode):
Add case to prevent inlining of call.
* inline.ads: Likewise.
* sem_res.adb (Resolve_Call): Update comment and message.
gcc/ada/inline.adb diff | blob | blame | history
gcc/ada/inline.ads diff | blob | blame | history
gcc/ada/sem_res.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git