[Ada] Proof of 'Image support for unsigned integers

[Ada] Proof of 'Image support for unsigned integers

Prove System.Image_U, making the connection with the space available in
the string as computed with System.Width_U and the functions that
support the other direction of 'Value in System.Value_U.

The units that support 'Image cannot be marked Pure anymore, as they now
depend on non-pure units.

gcc/ada/

	* libgnat/s-imaged.ads: Remove Pure.
	* libgnat/s-imagef.ads: Remove Pure.
	* libgnat/s-imager.ads: Remove Pure.
	* libgnat/s-imageu.adb: Add ghost code.
	* libgnat/s-imageu.ads: Add contracts.
	* libgnat/s-imde128.ads: Remove Pure.
	* libgnat/s-imde32.ads: Remove Pure.
	* libgnat/s-imde64.ads: Remove Pure.
	* libgnat/s-imfi128.ads: Remove Pure.
	* libgnat/s-imfi32.ads: Remove Pure.
	* libgnat/s-imfi64.ads: Remove Pure.
	* libgnat/s-imgflt.ads: Remove Pure.
	* libgnat/s-imglfl.ads: Remove Pure.
	* libgnat/s-imgllf.ads: Remove Pure.
	* libgnat/s-imglllu.ads: Instantiate with ghost subprograms.
	* libgnat/s-imgllu.ads: Instantiate with ghost subprograms.
	* libgnat/s-imgrea.ads: Remove Pure.
	* libgnat/s-imguns.ads: Instantiate with ghost subprograms.
	* libgnat/s-imguti.ads: Remove Pure.
	* libgnat/s-valueu.adb (Prove_Iter_Scan_Based_Number_Ghost,
	Prove_Scan_Only_Decimal_Ghost): New lemmas.
	* libgnat/s-valueu.ads (Uns_Option): Do not make type ghost to
	be able to use it as formal in instantiations.
	(Only_Decimal_Ghost): New ghost query.
	(Prove_Iter_Scan_Based_Number_Ghost,
	Prove_Scan_Only_Decimal_Ghost): New lemmas.
	* libgnat/s-widlllu.ads: Adapt to changes in Width_U.
	* libgnat/s-widllu.ads: Adapt to changes in Width_U.
	* libgnat/s-widthu.adb: Change generic function in generic
	package in order to complete the postcondition. Tighten the
	upper bound on the result by 1.
	* libgnat/s-widthu.ads: Same.
	* libgnat/s-widuns.ads: Adapt to changes in Width_U.
	* gcc-interface/Make-lang.in: Add dependencies on a-nubinu,
	a-numeri.ads and a-widuns.ads.