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