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

[Pierre-Marie de Rodat via Gcc-patches]

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.

patch.diff.gz
Description: application/gzip