This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Do not inline dispatching operations in GNATprove mode
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Tue, 17 Sep 2019 04:06:33 -0400
- Subject: [Ada] Do not inline dispatching operations in GNATprove mode
In GNATprove, local subprograms without contracts are candidates for
inlining, so that they are only analyzed in the context of their calls.
This does not apply to dispatching operations, which may be called
through dispatching, in an unknown calling context. Hence such
operations should not be considered as candidates for inlining.
There is no test as this has no effect on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling
for dispatching operations.
--- gcc/ada/inline.adb
+++ gcc/ada/inline.adb
@@ -1681,6 +1681,12 @@ package body Inline is
elsif not In_Extended_Main_Code_Unit (Id) then
return False;
+ -- Do not inline dispatching operations, as only their static calls
+ -- can be analyzed in context, and not their dispatching calls.
+
+ elsif Is_Dispatching_Operation (Id) then
+ return False;
+
-- Do not inline subprograms marked No_Return, possibly used for
-- signaling errors, which GNATprove handles specially.