[gcc r16-6599] ada: Do not inline calls to ghost functions

[Marc Poulhies]

https://gcc.gnu.org/g:ccf9af9d274ed9536d67868259191b96e82f8625

commit r16-6599-gccf9af9d274ed9536d67868259191b96e82f8625
Author: Piotr Trojanek <trojanek@adacore.com>
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