ada: Complete contracts of SPARK units

ada: Complete contracts of SPARK units

SPARK units in the standard library (both Ada and GNAT ones) should have
subprograms correctly annotated with contracts, so that a SPARK subprogram
should always return (not fail or raise an exception) under the conditions
expressed in its precondition, unless it is a procedure annotated with
Might_Not_Return.

gcc/ada/

	* libgnat/a-calend.ads: Mark with SPARK_Mode=>Off the functions which may
	raise Time_Error.
	* libgnat/a-ngelfu.ads: Mark with SPARK_Mode=>Off the functions which may
	lead to an overflow (which is not the case of Tan with one parameter for
	example, or Arctanh or Arcoth, despite their mathematical range covering
	the reals).
	* libgnat/a-textio.ads: Remove Always_Return annotation from functions, as
	this is now compulsory for functions to always return in SPARK.
	* libgnat/i-cstrin.ads: Add Might_Not_Return annotation to Update procedure
	which may not return.