ada: Refactor the proof of the Value and Image runtime units

ada: Refactor the proof of the Value and Image runtime units

The aim of this refactoring is to avoid unnecessary dependencies
between Image and Value units even though they share the same
specification functions. These functions are grouped inside ghost
packages which are then withed by Image and Value units.

gcc/ada/

	* libgnat/s-vs_int.ads: Instance of Value_I_Spec for Integer.
	* libgnat/s-vs_lli.ads: Instance of Value_I_Spec for
	Long_Long_Integer.
	* libgnat/s-vsllli.ads: Instance of Value_I_Spec for
	Long_Long_Long_Integer.
	* libgnat/s-vs_uns.ads: Instance of Value_U_Spec for Unsigned.
	* libgnat/s-vs_llu.ads: Instance of Value_U_Spec for
	Long_Long_Unsigned.
	* libgnat/s-vslllu.ads: Instance of Value_U_Spec for
	Long_Long_Long_Unsigned.
	* libgnat/s-imagei.ads: Take instances of Value_*_Spec as
	parameters.
	* libgnat/s-imagei.adb: Idem.
	* libgnat/s-imageu.ads: Idem.
	* libgnat/s-imageu.adb: Idem.
	* libgnat/s-valuei.ads: Idem.
	* libgnat/s-valuei.adb: Idem.
	* libgnat/s-valueu.ads: Idem.
	* libgnat/s-valueu.adb: Idem.
	* libgnat/s-imgint.ads: Adapt instance to new ghost parameters.
	* libgnat/s-imglli.ads: Adapt instance to new ghost parameters.
	* libgnat/s-imgllli.ads: Adapt instance to new ghost parameters.
	* libgnat/s-imglllu.ads: Adapt instance to new ghost parameters.
	* libgnat/s-imgllu.ads: Adapt instance to new ghost parameters.
	* libgnat/s-imguns.ads: Adapt instance to new ghost parameters.
	* libgnat/s-valint.ads: Adapt instance to new ghost parameters.
	* libgnat/s-vallli.ads: Adapt instance to new ghost parameters.
	* libgnat/s-valllli.ads: Adapt instance to new ghost parameters.
	* libgnat/s-vallllu.ads: Adapt instance to new ghost parameters.
	* libgnat/s-valllu.ads: Adapt instance to new ghost parameters.
	* libgnat/s-valuns.ads: Adapt instance to new ghost parameters.
	* libgnat/s-vaispe.ads: Take instance of Value_U_Spec as parameter
	and remove unused declaration.
	* libgnat/s-vaispe.adb: Idem.
	* libgnat/s-vauspe.ads: Remove unused declaration.
	* libgnat/s-valspe.ads: Factor out the specification part of
	Val_Util.
	* libgnat/s-valspe.adb: Idem.
	* libgnat/s-valuti.ads: Move specification to Val_Spec.
	* libgnat/s-valuti.adb: Idem.
	* libgnat/s-valboo.ads: Use Val_Spec.
	* libgnat/s-valboo.adb: Idem.
	* libgnat/s-imgboo.adb: Idem.
	* libgnat/s-imagef.adb: Adapt instances to new ghost parameters.
	* Makefile.rtl: List new files.