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.

0 files changed, 0 insertions, 0 deletions