Inlining in GNATprove mode is made to improve results of formal
verification in GNATprove. It should not be done on procedures marked
No_Return, which are handled specially in GNATprove.
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-10-20 Yannick Moy <m...@adacore.com>
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Return
False for procedures marked No_Return.
* sem_util.ads (Enclosing_Declaration): Improve comment.
Index: inline.adb
===================================================================
--- inline.adb (revision 229023)
+++ inline.adb (working copy)
@@ -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.
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 229023)
+++ sem_util.ads (working copy)
@@ -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;
