[Ada] Fix crashes on ownership checking in SPARK

[Ada] Fix crashes on ownership checking in SPARK

Code that violates the conditions for ownership checking should lead to
error messages pointing to the violations instead of crashes.

There is no impact on compilation, only GNATprove.

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

gcc/ada/

	* sem_spark.adb (Get_Root_Object): Replace precondition by error
	message.
	(Read_Indexes): Replace precondition by error message.
	(Check_Callable_Body): Check only traversal function returns an
	anonymous access type.
	(Check_Expression): Issue error on unexpected expression as
	path.
	* sem_util.adb (First_Global): Fix access to global on
	entry/task.

From-SVN: r273329