From: Piotr Trojanek <[email protected]>
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.
Tested on x86_64-pc-linux-gnu (before the recent bootstrap breakage), committed
on master.
---
gcc/ada/inline.adb | 11 +++++++++++
1 file changed, 11 insertions(+)
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
--
2.51.0
