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 0cb879a7133a407ed58150494b57ae9b9ad243dc..3833af8e84a6c2a2fa790827ecba7c152dd7ca12 100644 (file)
--- 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