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.

1 files changed, 4 insertions, 1 deletions

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