From cbb0b55385692dca6898a2668766f17ea42c4d2e Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 17 Sep 2019 08:01:10 +0000 Subject: [PATCH] [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 gcc/ada/ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling for dispatching operations. From-SVN: r275779 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/inline.adb | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 94877b24ea1..a2f7e276334 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-09-17 Yannick Moy + + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add handling + for dispatching operations. + 2019-09-17 Ed Schonberg * sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): In a diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index e5ecb554075..6e345d66aa7 100644 --- 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. -- 2.30.2