===================================================================
@@ -1534,6 +1534,12 @@
elsif In_Package_Visible_Spec (Id) then
return False;
+ -- Do not inline subprograms marked No_Return, possibly used for
+ -- signaling errors, which GNATprove handles specially.
+
+ elsif No_Return (Id) then
+ return False;
+
-- Do not inline subprograms that have a contract on the spec or the
-- body. Use the contract(s) instead in GNATprove.
===================================================================
@@ -532,7 +532,8 @@
-- Returns the closest ancestor of Typ that is a CPP type.
function Enclosing_Declaration (N : Node_Id) return Node_Id;
- -- Returns the declaration node enclosing N, if any, or Empty otherwise
+ -- Returns the declaration node enclosing N (including possibly N itself),
+ -- if any, or Empty otherwise
function Enclosing_Generic_Body
(N : Node_Id) return Node_Id;