[Ada] Add contracts to Strings libraries

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 10 July 2019 09:01 EDT

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

2019-07-10 Joffrey Huguet

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.

2e7929f0fe0 [Ada] Add contracts to Strings libraries
gcc/ada/ChangeLog | 7 +
gcc/ada/libgnat/a-strbou.ads | 521 +++++++++++++++++++++++++++++------
gcc/ada/libgnat/a-strfix.ads | 246 ++++++++++++++---
gcc/ada/libgnat/a-strunb.ads | 403 ++++++++++++++++++++++-----
gcc/ada/libgnat/a-strunb__shared.ads | 405 ++++++++++++++++++++++-----
5 files changed, 1328 insertions(+), 254 deletions(-)

Upstream: gcc.gnu.org


  • Share