diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-23 12:58:42 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-13 08:04:35 +0000 |
| commit | 3fe35ab093de715e88fc837155954bbe74b326f3 (patch) | |
| tree | 1cd89e77f24dad683f2219eb10781f42f016ed10 /gcc/ada/libgnat | |
| parent | 9e5b1b076a57feee4057460aac8aae451b42431e (diff) | |
| download | gcc-3fe35ab093de715e88fc837155954bbe74b326f3.zip gcc-3fe35ab093de715e88fc837155954bbe74b326f3.tar.gz gcc-3fe35ab093de715e88fc837155954bbe74b326f3.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/libgnat')
| -rw-r--r-- | gcc/ada/libgnat/a-strbou.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-strsup.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-strsup.ads | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index a9ee3b2..839760a 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -1898,7 +1898,7 @@ package Ada.Strings.Bounded with SPARK_Mode is -- some characters of Source are remaining at the left. and then - (if New_Item'Length > Max_Length then + (if New_Item'Length >= Max_Length then -- New_Item covers all Max_Length characters @@ -1984,7 +1984,7 @@ package Ada.Strings.Bounded with SPARK_Mode is -- some characters of Source are remaining at the left. and then - (if New_Item'Length > Max_Length then + (if New_Item'Length >= Max_Length then -- New_Item covers all Max_Length characters diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb index 2c1b4594..f1a40a2 100644 --- a/gcc/ada/libgnat/a-strsup.adb +++ b/gcc/ada/libgnat/a-strsup.adb @@ -1226,7 +1226,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is (New_Item (New_Item'First .. New_Item'Last - Droplen)); when Strings.Left => - if New_Item'Length > Max_Length then + if New_Item'Length >= Max_Length then Source.Data (1 .. Max_Length) := Super_String_Data (New_Item (New_Item'Last - Max_Length + 1 .. New_Item'Last)); diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 19e333c..416fa7b 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -2000,7 +2000,7 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- Source are remaining at the left. and then - (if New_Item'Length > Source.Max_Length then + (if New_Item'Length >= Source.Max_Length then -- New_Item covers all Max_Length characters @@ -2089,7 +2089,7 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- Source are remaining at the left. and then - (if New_Item'Length > Source.Max_Length then + (if New_Item'Length >= Source.Max_Length then -- New_Item covers all Max_Length characters |