[Ada] Adapt ownership checking in SPARK to traversal functions

[Ada] Adapt ownership checking in SPARK to traversal functions

A traversal function, especially when implemented as an expression
function, may need to return an if-expression or case-expression, while
still respecting Legality Rule SPARK RM 3.10(5). This case is now
allowed in GNATprove.

There is no impact on compilation.

2019-07-22  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb (Get_Root_Object, Is_Path_Expression,
	Is_Subpath_Expression): Add parameter Is_Traversal to adapt
	these functions to the case of paths returned from a traversal
	function.
	(Read_Indexes): Handle the case of an if-expression or
	case-expression.
	(Check_Statement): Check Emit_Messages only when issuing an
	error message. This is important as Emit_Messages may store the
	information that an error was detected.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@273693 138bc75d-0d04-0410-961f-82ee72b054a4