Changes in GNATprove (translation to Why3 and provers) result in proofs
being much less automatic, and requiring ghost code to detail
intermediate steps. In some cases, it is better to use the new By
mechanism to prove assertions in steps, as this avoids polluting the
proof context for other proofs. For that reason, add units s-spark.ads
and s-spcuop.ads/b to the runtime sources.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* Makefile.rtl: Add new units.
	* libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers.
	* libgnat/s-spcuop.adb: New unit for ghost cut operations.
	* libgnat/s-spcuop.ads: New unit for ghost cut operations.
	* libgnat/s-spark.ads: New unit.