[Ada] Proof of support units for 'Width on signed integers

[Ada] Proof of support units for 'Width on signed integers

gcc/ada/

	* libgnat/s-widint.ads: Mark in SPARK.
	* libgnat/s-widlli.ads: Likewise.
	* libgnat/s-widllli.ads: Likewise.
	* libgnat/s-widlllu.ads: Likewise.
	* libgnat/s-widllu.ads: Disable ghost/contract.
	* libgnat/s-widthi.adb: Replicate and adapt the proof from
	s-widthu.adb.
	* libgnat/s-widthi.ads: Add minimal postcondition.
	* libgnat/s-widthu.adb: Fix comments in the modular case.
	* libgnat/s-widthu.ads: Add minimal postcondition.
	* libgnat/s-widuns.ads: Disable ghost/contract.