[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.

2019-09-17  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling
	for dispatching operations.

From-SVN: r275779

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 94877b24ea138fd545274c988598eb9895f3f12b..a2f7e27633497ade628a0eba1860750264ff9b63 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-09-17  Yannick Moy  <moy@adacore.com>
+
+       * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling
+       for dispatching operations.
+
 2019-09-17  Ed Schonberg  <schonberg@adacore.com>
 
        * sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): In a

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index e5ecb554075ccd938a48b09f441d84bfae3ad2ab..6e345d66aa727852177490fa9938f167da23daba 100644 (file)
--- a/gcc/ada/inline.adb
+++ b/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.