[Ada] Fix proof of runtime unit System.Value* and System.Image*

[Ada] Fix proof of runtime unit System.Value* and System.Image*

Refactor specification of the Value* and Image* units and fix proofs.

gcc/ada/

	* libgnat/a-nbnbig.ads: Add Always_Return annotation.
	* libgnat/s-vaispe.ads: New ghost unit for the specification of
	System.Value_I. Restore proofs.
	* libgnat/s-vauspe.ads: New ghost unit for the specification of
	System.Value_U. Restore proofs.
	* libgnat/s-valuei.adb: The specification only subprograms are
	moved to System.Value_I_Spec. Restore proofs.
	* libgnat/s-valueu.adb: The specification only subprograms are
	moved to System.Value_U_Spec. Restore proofs.
	* libgnat/s-valuti.ads
	(Uns_Params): Generic unit used to bundle together the
	specification functions of System.Value_U_Spec.
	(Int_Params): Generic unit used to bundle together the
	specification functions of System.Value_I_Spec.
	* libgnat/s-imagef.adb: It is now possible to instantiate the
	appropriate specification units instead of creating imported ghost
	subprograms.
	* libgnat/s-imagei.adb: Update to refactoring of specifications
	and fix proofs.
	* libgnat/s-imageu.adb: Likewise.
	* libgnat/s-imgint.ads: Ghost parameters are grouped together in a
	package now.
	* libgnat/s-imglli.ads: Likewise.
	* libgnat/s-imgllu.ads: Likewise.
	* libgnat/s-imgllli.ads: Likewise.
	* libgnat/s-imglllu.ads: Likewise.
	* libgnat/s-imguns.ads: Likewise.
	* libgnat/s-vallli.ads: Likewise.
	* libgnat/s-valllli.ads: Likewise.
	* libgnat/s-imagei.ads: Likewise.
	* libgnat/s-imageu.ads: Likewise.
	* libgnat/s-vaispe.adb: Likewise.
	* libgnat/s-valint.ads: Likewise.
	* libgnat/s-valuei.ads: Likewise.
	* libgnat/s-valueu.ads: Likewise.
	* libgnat/s-vauspe.adb: Likewise.