From: Piotr Trojanek <trojanek@adacore.com>
Date: Mon, 24 Nov 2025 13:38:32 +0000 (+0100)
Subject: ada: Do not inline calls to ghost functions
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ccf9af9d274ed9536d67868259191b96e82f8625;p=thirdparty%2Fgcc.git

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 --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 0cb879a7133..3833af8e84a 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