[Ada] Proof of Interfaces.C with SPARK

[Ada] Proof of Interfaces.C with SPARK

gcc/ada/

	* libgnat/i-c.adb: Add ghost code.
	(C_Length_Ghost): New ghost functions to query the C length of a
	string.
	(To_Ada): Insert constant Count_Cst where needed to comply with
	SPARK.  Homogeneize code between variants for char, wchar_t,
	char16_t and char32_t. Use char16_nul and char32_nul
	systematically instead of their value. Fix the type of index To
	to be Integer instead of Positive, to avoid a possible range
	check failure on an empty Target. Insert an exit statement to
	avoid a possible overflow failure when the last index in Target
	is Natural'Last (possibly on a small string as well).
	* libgnat/i-c.ads: Add contracts.
	(C_Length_Ghost): New ghost functions to query the C length of a
	string.
	* libgnat/s-os_lib.adb: Remove pragma Compiler_Unit_Warning
	causing a spurious error during compilation of GNAT, as this
	pragma is not needed anymore now that we bootstrap (stage1) with
	the base compiler runtime.