diff options
| author | Joffrey Huguet <huguet@adacore.com> | 2023-01-16 16:44:14 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-22 10:44:08 +0200 |
| commit | 561b239327842ca4f21bdbb6535e629b907355e4 (patch) | |
| tree | 3ca867eb8d837cf5497a09bfc4a9b30821ec0b34 /gcc/ada/sem_util.ads | |
| parent | f23d4b88f5beffd8430b6b75088775614ed13980 (diff) | |
| download | gcc-561b239327842ca4f21bdbb6535e629b907355e4.zip gcc-561b239327842ca4f21bdbb6535e629b907355e4.tar.gz gcc-561b239327842ca4f21bdbb6535e629b907355e4.tar.bz2 | |
ada: Add contracts to Ada.Strings.Unbounded library
This patch adds contracts to the conversions between
Unbounded_String and String, the Element function and the
equality between two Unbounded_String, or between
Unbounded_String and String.
This patch also disallows the use of a function in SPARK, because
it returns an uninitialized Unbounded_String.
gcc/ada/
* libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads
(To_Unbounded_String): Add postcondition. Add aspect SPARK_Mode
Off on the version that takes a Natural as parameter.
(To_String): Complete postcondition.
(Set_Unbounded_String): Add postcondition.
(Element): Likewise.
("="): Likewise.
Diffstat (limited to 'gcc/ada/sem_util.ads')
0 files changed, 0 insertions, 0 deletions