ada: Add contracts to Ada.Strings.Unbounded and adapt implementation

Add complete functional contracts to all subprograms in
Ada.Strings.Unbounded, except Count, following the specification from
Ada RM A.4.5. These contracts are similar to the contracts found in
Ada.Strings.Fixed and Ada.Strings.Bounded.

A difference is that type Unbounded_String is controlled, thus we avoid
performing copies of a parameter Source with Source'Old, and instead
apply 'Old attribute on the enclosing call, such as Length(Source)'Old.

As Unbounded_String is controlled, the implementation is not in SPARK.
Instead, we have separately proved a slightly different implementation
for which Unbounded_String is not controlled, against the same
specification. This ensures that the specification is consistent.

To minimize differences between this test from the SPARK testsuite and
the actual implementation (the one in a-strunb.adb), and to avoid
overflows in the actual implementation, some code is slightly rewritten.
Delete and Insert are modified to return the correct result in all
cases allowed by the standard.

The same contracts are added to the version in a-strunb__shared.ads and
similar implementation patches are applied to the body
a-strunb__shared.adb. In particular, tests are added to avoid overflows
on strings for which the last index is Natural'Last, and the computations
that involve Sum to guarantee that an exception is raised in case of
overflow are rewritten to guarantee correct detection and no intermediate
overflows (and such tests are applied consistently between the procedure
and the function when both exist).

gcc/ada/

	* libgnat/a-strunb.adb (Sum, Saturated_Sum, Saturated_Mul): Adapt
	function signatures to more precise types that allow proof.
	(function "&"): Conditionally assign a slice to avoid possible
	overflow which only occurs when the assignment is a noop (because
	the slice is empty in that case).
	(Append): Same.
	(function "*"): Retype K to avoid a possible overflow. Add early
	return on null length for proof.
	(Delete): Fix implementation to return the correct result in all
	cases allowed by the Ada standard.
	(Insert): Same. Also avoid possible overflows.
	(Length): Rewrite as expression function for proof.
	(Overwrite): Avoid possible overflows.
	(Slice): Same.
	(To_String): Rewrite as expression function for proof.
	* libgnat/a-strunb.ads: Extend Assertion_Policy to new contracts
	used. Add complete functional contracts to all subprograms of the
	public API except Count.
	* libgnat/a-strunb__shared.adb (Sum): Adapt function signature to
	more precise types that allow proof.
	(function "&"): Conditionally assign a slice to avoid possible
	overflow.
	(function "*"): Retype K to avoid a possible overflow.
	(Delete): Fix implementation to return the correct result in all
	cases allowed by the Ada standard.
	(Insert): Avoid possible overflows.
	(Overwrite): Avoid possible overflows.
	(Replace_Slice): Same.
	(Slice): Same.
	(To_String): Rewrite as expression function for proof.
	* libgnat/a-strunb__shared.ads: Extend Assertion_Policy to new
	contracts used. Add complete functional contracts to all
	subprograms of the public API except Count. Mark public part of
	spec as in SPARK.

0 files changed, 0 insertions, 0 deletions