https://gcc.gnu.org/g:ccf9af9d274ed9536d67868259191b96e82f8625
commit r16-6599-gccf9af9d274ed9536d67868259191b96e82f8625 Author: Piotr Trojanek <[email protected]> Date: Mon Nov 24 14:38:32 2025 +0100 ada: Do not inline calls to ghost functions Instead of detecting exceptions by inlined ghost function calls we simply prevent ghost functions from being inlined. This change only affects SPARK. gcc/ada/ChangeLog: * inline.adb (Build_Body_To_Inline): Do not inline ghost functions. Diff: --- gcc/ada/inline.adb | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 0cb879a7133a..3833af8e84a6 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1224,6 +1224,17 @@ package body Inline is return; end if; + -- Do not inline ghost functions, because inlined functions are + -- difficult to detect and we must do it to reject exceptions propagated + -- from ghost calls to ordinary code. + + if Ekind (Spec_Id) = E_Function + and then Is_Ghost_Entity (Spec_Id) + then + Cannot_Inline ("cannot inline & (ghost function)?", N, Spec_Id); + return; + end if; + if Present (Handled_Statement_Sequence (N)) then if Present (Exception_Handlers (Handled_Statement_Sequence (N))) then Cannot_Inline
