[Ada] Refine pointer support in SPARK

[Ada] Refine pointer support in SPARK

Refine the implementation of pointer support for SPARK analysis.

There is no impact on compilation.

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

gcc/ada/

	* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): New function to
	return go through traversal function call.
	(Check_Type): Consistently use underlying type.
	(Get_Perm): Adapt for case of elaboration code where variables
	are not declared in the environment. Remove incorrect handling
	of borrow and observe.

From-SVN: r272981