]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef8a3d9) | patch
[Ada] Add contracts to Strings libraries
authorJoffrey Huguet <huguet@adacore.com>
Wed, 10 Jul 2019 09:01:28 +0000 (09:01 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 10 Jul 2019 09:01:28 +0000 (09:01 +0000)
commit0b6694b4e41d394df12d159c319be4b1326745ca
treeb6b1671197753eafa5230593976443fa82782351tree | snapshot
parentef8a3d9ef0ace5479d42f7a5382393b5a1a79d96commit | diff
[Ada] Add contracts to Strings libraries

This patch adds contracts to Ada.Strings libraries, in order to remove
warnings when using these libraries in SPARK.

2019-07-10  Joffrey Huguet  <huguet@adacore.com>

gcc/ada/

* libgnat/a-strbou.ads, libgnat/a-strfix.ads,
libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads: Add global
contracts, contract cases, preconditions and postconditions to
procedures and functions.

From-SVN: r273334
gcc/ada/ChangeLog diff | blob | blame | history
gcc/ada/libgnat/a-strbou.ads diff | blob | blame | history
gcc/ada/libgnat/a-strfix.ads diff | blob | blame | history
gcc/ada/libgnat/a-strunb.ads diff | blob | blame | history
gcc/ada/libgnat/a-strunb__shared.ads diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git