[Ada] Proof of System.Val_Util utilities for 'Value support

[Ada] Proof of System.Val_Util utilities for 'Value support

gcc/ada/

	* libgnat/s-valboo.adb (First_Non_Space_Ghost): Move to
	utilities.
	(Value_Boolean): Prefix call to First_Non_Space_Ghost.
	* libgnat/s-valboo.ads (First_Non_Space_Ghost): Move to
	utilities.
	(Is_Boolean_Image_Ghost, Value_Boolean): Prefix call to
	First_Non_Space_Ghost.
	* libgnat/s-valuer.adb (Scan_Raw_Real): Adapt to change of
	function Scan_Exponent to procedure.
	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Adapt to change of
	function Scan_Exponent to procedure.
	* libgnat/s-valuti.adb (First_Non_Space_Ghost): Function moved
	here.
	(Last_Number_Ghost): New ghost query function.
	(Scan_Exponent): Change function with side-effects into
	procedure, to mark in SPARK. Prove procedure wrt contract.
	Change type of local P to avoid possible range check failure (it
	is not known whether this can be activated by callers).
	(Scan_Plus_Sign, Scan_Sign): Change type of local P to avoid
	possible range check failure. Add loop invariants and assertions
	for proof.
	(Scan_Trailing_Blanks): Add loop invariant.
	(Scan_Underscore): Remove SPARK_Mode Off.
	* libgnat/s-valuti.ads (First_Non_Space_Ghost): Function moved
	here.
	(Last_Number_Ghost, Only_Number_Ghost, Is_Natural_Format_Ghost,
	Scan_Natural_Ghost): New ghost query functions.
	(Scan_Plus_Sign, Scan_Sign, Scan_Exponent, Scan_Trailing_Blanks,
	Scan_Underscore): Add functional contracts.