diff options
| author | Pierre-Alexandre Bazin <bazin@adacore.com> | 2021-07-02 15:43:44 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-22 15:01:48 +0000 |
| commit | 1647bc2a78b2182007f011ff0a43f872086ee512 (patch) | |
| tree | 670c2c96daf0797b252ea5787c729194d78a676a /libvtv | |
| parent | 5f325f5e6fd091f73f5be6ef30d27e22e4b59a74 (diff) | |
| download | gcc-1647bc2a78b2182007f011ff0a43f872086ee512.zip gcc-1647bc2a78b2182007f011ff0a43f872086ee512.tar.gz gcc-1647bc2a78b2182007f011ff0a43f872086ee512.tar.bz2 | |
[Ada] Contracts written for the Ada.Strings.Bounded library
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.
Diffstat (limited to 'libvtv')
0 files changed, 0 insertions, 0 deletions