[Ada] Disable inlining of traversal function in GNATprove

[Ada] Disable inlining of traversal function in GNATprove

Traversal functions as defined in SPARK RM 3.10 should not be inlined
for analysis in GNATprove, as this changes the ownership behavior.
Disable the inlining performed in GNATprove on functions which could be
interpreted as such.

There is no impact on compilation and thus no test.

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

gcc/ada/

	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add special
	case for traversal functions.

From-SVN: r275948