| commit | 3fe35ab093de715e88fc837155954bbe74b326f3 | |
| author | Yannick Moy <moy@adacore.com> | |
| Wed, 23 Feb 2022 11:58:42 +0000 (23 12:58 +0100) | ||
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | |
| Fri, 13 May 2022 08:04:35 +0000 (13 08:04 +0000) | ||
| tree | 1cd89e77f24dad683f2219eb10781f42f016ed10 | treesnapshot (tar.gz zip) |
| parent | 9e5b1b076a57feee4057460aac8aae451b42431e | commitdiff |
[Ada] Facilitate proof of Overwrite in bounded strings library
Consistently use >= operator in both the code and contracts of
function/procedure Overwrite, to facilitate proof, instead of the strict
inequality > sometimes, as only New_Item remains in the result in the
case of equal size too.
gcc/ada/
* libgnat/a-strbou.ads (Overwrite): Switch to >= operator in
contracts.
* libgnat/a-strsup.adb (Super_Overwrite): Switch to >= operator
in code of procedure (function already uses it).
* libgnat/a-strsup.ads (Super_Overwrite): Switch to >= operator
in contracts.
Consistently use >= operator in both the code and contracts of
function/procedure Overwrite, to facilitate proof, instead of the strict
inequality > sometimes, as only New_Item remains in the result in the
case of equal size too.
gcc/ada/
* libgnat/a-strbou.ads (Overwrite): Switch to >= operator in
contracts.
* libgnat/a-strsup.adb (Super_Overwrite): Switch to >= operator
in code of procedure (function already uses it).
* libgnat/a-strsup.ads (Super_Overwrite): Switch to >= operator
in contracts.
| gcc/ada/libgnat/a-strbou.ads | diffblobblamehistory | |
| gcc/ada/libgnat/a-strsup.adb | diffblobblamehistory | |
| gcc/ada/libgnat/a-strsup.ads | diffblobblamehistory |