ada: Add annotations for proof of termination of runtime units

ada: Add annotations for proof of termination of runtime units

String-manipulating functions should always terminate. Add justification
for the termination of Mapping function parameter, and loop variants
where needed. This is needed for GNATprove to prove termination.

gcc/ada/

	* libgnat/a-strbou.ads: Add justifications for Mapping.
	* libgnat/a-strfix.adb: Same.
	* libgnat/a-strfix.ads: Same.
	* libgnat/a-strsea.adb: Same.
	* libgnat/a-strsea.ads: Same.
	* libgnat/a-strsup.adb: Same and add loop variants.
	* libgnat/a-strsup.ads: Same and add specification of termination.