ada: Remove references to Might_Not_Return and Always_Return

ada: Remove references to Might_Not_Return and Always_Return

The Might_Not_Return and Always_Return annotations for GNATprove
should now be replaced by the two more precise aspects
Exceptional_Cases and Always_Terminates.
They allow to specify whether a subprogram is allowed to raise
exceptions or fail to complete.

gcc/ada/

	* libgnat/a-strfix.ads: Replace Might_Not_Return annotations by
	Exceptional_Cases and Always_Terminates aspects.
	* libgnat/a-tideio.ads: Idem.
	* libgnat/a-tienio.ads: Idem.
	* libgnat/a-tifiio.ads: Idem.
	* libgnat/a-tiflio.ads: Idem.
	* libgnat/a-tiinio.ads: Idem.
	* libgnat/a-timoio.ads: Idem.
	* libgnat/a-textio.ads: Idem. Also mark functions Name, Col, Line,
	and Page as out of SPARK as they might raise Layout_Error.
	* libgnarl/a-reatim.ads: Replace Always_Return annotations by
	Always_Terminates aspects.
	* libgnat/a-chahan.ads: Idem.
	* libgnat/a-nbnbig.ads: Idem.
	* libgnat/a-nbnbin.ads: Idem.
	* libgnat/a-nbnbre.ads: Idem.
	* libgnat/a-ngelfu.ads: Idem.
	* libgnat/a-nlelfu.ads: Idem.
	* libgnat/a-nllefu.ads: Idem.
	* libgnat/a-nselfu.ads: Idem.
	* libgnat/a-nuelfu.ads: Idem.
	* libgnat/a-strbou.ads: Idem.
	* libgnat/a-strmap.ads: Idem.
	* libgnat/a-strsea.ads: Idem.
	* libgnat/a-strsup.ads: Idem.
	* libgnat/a-strunb.ads: Idem.
	* libgnat/a-strunb__shared.ads: Idem.
	* libgnat/g-souinf.ads: Idem.
	* libgnat/i-c.ads: Idem.
	* libgnat/interfac.ads: Idem.
	* libgnat/interfac__2020.ads: Idem.
	* libgnat/s-aridou.adb: Idem.
	* libgnat/s-arit32.adb: Idem.
	* libgnat/s-atacco.ads: Idem.
	* libgnat/s-spcuop.ads: Idem.
	* libgnat/s-stoele.ads: Idem.
	* libgnat/s-vaispe.ads: Idem.
	* libgnat/s-vauspe.ads: Idem.
	* libgnat/i-cstrin.ads: Add a precondition instead of a
	Might_Not_Return annotation.