[Ada] Contracts written for the Ada.Strings.Bounded library

[Ada] Contracts written for the Ada.Strings.Bounded library

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 1665 bytes --]

Written SPARK contracts describing the behaviours of all functions of
the Ada.Strings.Bounded library. All contracts are replicated in
Ada.Strings.Superbounded, the package that provides the explicit
implementation of bounded strings. The contracts (with the exception of
Trim, which uses search functions to determine the cutting points) only
use the functions Length, Element and Slice, which are expression
functions accessing the data of bounded strings. So far, all contracts
in Ada.Strings.Superbounded are proved, except the longest ones (Insert,
Overwrite, Replace_Slice), whose bodies are thus turned with SPARK_Mode
Off (but absence of runtime errors has been ensured before turning
SPARK_Mode Off). The contracts in Ada.Strings.Bounded are proved using
the contracts in Superbounded.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/a-strbou.adb: Turn SPARK_Mode on.
	* libgnat/a-strbou.ads: Write contracts.
	* libgnat/a-strfix.ads (Index): Fix grammar error in a comment.
	* libgnat/a-strsea.ads (Index): Likewise.
	* libgnat/a-strsup.adb: Rewrite the body to take into account
	the new definition of Super_String using Relaxed_Initialization
	and a predicate.
	(Super_Replicate, Super_Translate, Times): Added loop
	invariants, and ghost lemmas for Super_Replicate and Times.
	(Super_Trim): Rewrite the body using search functions to
	determine the cutting points.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Remove (now written as expression functions in a-strsup.ads).
	* libgnat/a-strsup.ads: Added contracts.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Rewrite as expression functions.

[-- Attachment #2: patch.diff.gz --]
[-- Type: application/gzip, Size: 29311 bytes --]