From 9afbf898ce89f6bcb314ddf03da20abdf0ac79cd Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 7 Dec 2023 00:27:16 +0100 Subject: ada: More aggressive inlining of subprogram calls in GNATprove mode Previously if a subprogram call could not be inlined in GNATprove mode, then all subsequent calls to the same subprogram were not inlined either (because a failed attempt to inline clears flag Is_Inlined_Always and we tested this flag when attempting to inline subsequent calls). Now a failure in inlining of a particular call does not prevent inlining of subsequent calls to the same subprogram, except when inlining failed because the subprogram was detected to be recursive (which clears the Is_Inlined flag that we now examine). This change allows more checks to be proved and reduces interactions between inlining and SPARK legality checks. gcc/ada/ * sem_ch6.adb (Analyze_Subprogram_Specification): Set Is_Inlined flag by default in GNATprove mode. * sem_res.adb (Resolve_Call): Only look at flag which is cleared when inlined subprogram is detected to be recursive. --- gcc/ada/sem_ch6.adb | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'gcc/ada/sem_ch6.adb') diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index da6f6c4..bdfe446 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -5325,10 +5325,13 @@ package body Sem_Ch6 is -- Flag Is_Inlined_Always is True by default, and reversed to False for -- those subprograms which could be inlined in GNATprove mode (because - -- Body_To_Inline is non-Empty) but should not be inlined. + -- Body_To_Inline is non-Empty) but should not be inlined. Flag + -- Is_Inlined is True by default and reversed to False when inlining + -- fails because the subprogram is detected to be recursive. if GNATprove_Mode then Set_Is_Inlined_Always (Designator); + Set_Is_Inlined (Designator); end if; -- Introduce new scope for analysis of the formals and the return type -- cgit v1.1