[Ada] SPARK proof of the Ada.Strings.Fixed library

[Ada] SPARK proof of the Ada.Strings.Fixed library

gcc/ada/

	* libgnat/a-strfix.adb ("*"): Added loop invariants and lemmas
	for proof.
	(Delete): Added assertions for proof, and conditions to avoid
	overflow.
	(Head): Added loop invariant.
	(Insert): Same as Delete.
	(Move): Declared with SPARK_Mode Off.
	(Overwrite): Added assertions for proof, and conditions to avoid
	overflow.
	(Replace_Slice): Added assertions for proof, and conditions to
	avoid overflow.
	(Tail): Added loop invariant and avoided overflows.
	(Translate): Added loop invariants.
	(Trim): Ensured empty strings returned start at 1.
	* libgnat/a-strfix.ads (Index): Rewrote contract cases for
	easier proof.
	(Index_Non_Blank): Separated the null string case.
	(Count): Specified Mapping shouldn't be null.
	(Find_Token): Specified Source'First should be Positive when no
	From is given.
	(Translate): Specified Mapping shouldn't be null.
	("*"): Rewrote postcondition for easier proof.
	* libgnat/a-strsea.adb (Belongs): Added postcondition.
	(Count): Rewrote loops and added loop invariants to avoid
	overflows.
	(Find_Token): Added loop invariants.
	(Index): Rewrote loops to avoid overflows and added loop
	invariants for proof.
	(Index_Non_Blank): Added loop invariants.
	(Is_Identity): New function isolated without SPARK_Mode.
	* libgnat/a-strsea.ads: Fix starting comment as package is no
	longer private.
	(Match): Declared ghost expression function Match.
	(Is_Identity): Described identity in the postcondition.
	(Index, Index_Non_Blank, Count, Find_Token): Added contract from
	a-strfix.ads.