[Ada] Proof of Boolean'Image and Boolean'Value

[Ada] Proof of Boolean'Image and Boolean'Value

gcc/ada/

	* libgnat/s-imgboo.adb: Mark in SPARK.
	* libgnat/s-imgboo.ads: Mark in SPARK. Change from Pure to
	Preelaborate unit in order to be able to depend on
	System.Val_Bool.
	(Image_Boolean): Functionally specify the result of the
	procedure by calling System.Val_Bool.Value_Boolean on the
	result.
	* libgnat/s-valboo.adb: Mark in SPARK.
	(First_Non_Space_Ghost): New ghost function.
	(Value_Boolean): Change type of L and F to avoid possible range
	check failure on empty Str.
	* libgnat/s-valboo.ads: Mark in SPARK. Duplicate with-clause
	from body in the spec to be able to call
	System.Val_Util.Only_Space_Ghost in the contract.
	(First_Non_Space_Ghost): New ghost function computing the first
	non-space character in a string.
	(Is_Boolean_Image_Ghost): New ghost function computing whether a
	string is the image of a boolean value.
	(Value_Boolean): Add in precondition the conditions to avoid
	raising Constraint_Error. This precondition is never executed,
	and only used in proof, thanks to the use of pragma
	Assertion_Policy. Given that precondition, the postcondition can
	simply check the first non-space character to decide whether
	True or False is read.
	* libgnat/s-valuti.adb: Mark in SPARK, but use SPARK_Mode Off on
	all subprograms not yet proved.
	(Bad_Value): Annotate expected exception.
	(Normalize_String): Rewrite to avoid possible overflow when
	incrementing F in the first loop. Add loop invariants.
	* libgnat/s-valuti.ads: Mark in SPARK.
	(Bad_Value): Add Depends contract to avoid warning on unused S.
	(Only_Space_Ghost): New ghost function to query if string has
	only space in the specified range.
	(Normalize_String): Add functional contract.
	(Scan_Exponent): Mark spec as not in SPARK as this function has
	side-effects.