From: Yannick Moy <m...@adacore.com>
The contracts of Ada.Strings.Bounded.To_String and
Ada.Strings.Fixed.Delete are updated to reflect the standard spec and to
allow proof of callers.
gcc/ada/
* libgnat/a-strbou.ads (To_String): Add a postcondition to state
the value of bounds of the returned string, which helps with proof
of callers.
* libgnat/a-strfix.adb (Delete): Fix implementation to produce
correct result in all cases. For example, returned string should
always have a lower bound of 1, which was not respected in one
case. This was not detected by proof, since this code was dead
according to the too strict precondition.
* libgnat/a-strfix.ads (Delete): State the correct precondition
from standard which allows a value of Through beyond the last
valid index, and also restricts values of From from below. Update
the Contract_Cases accordingly to allow new values of parameters.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/a-strbou.ads | 3 +++
gcc/ada/libgnat/a-strfix.adb | 33 ++++++++++++---------------------
gcc/ada/libgnat/a-strfix.ads | 20 ++++++++++++--------
3 files changed, 27 insertions(+), 29 deletions(-)
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index 827c0dc7448..a4830e56b78 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -127,6 +127,9 @@ is
-- * If Drop=Error, then Strings.Length_Error is propagated.
function To_String (Source : Bounded_String) return String with
+ Post =>
+ To_String'Result'First = 1
+ and then To_String'Result'Length = Length (Source),
Global => null;
-- To_String returns the String value with lower bound 1
-- represented by Source. If B is a Bounded_String, then
diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
index 901fd60284b..2da5367985b 100644
--- a/gcc/ada/libgnat/a-strfix.adb
+++ b/gcc/ada/libgnat/a-strfix.adb
@@ -266,36 +266,27 @@ package body Ada.Strings.Fixed with SPARK_Mode is
return Result_Type (Source);
end;
- elsif From not in Source'Range
- or else Through > Source'Last
- then
- pragma Annotate
- (CodePeer, False_Positive,
- "test always false", "self fullfilling prophecy");
-
- -- In most cases this raises an exception, but the case of deleting
- -- a null string at the end of the current one is a special-case, and
- -- reflects the equivalence with Replace_String (RM A.4.3 (86/3)).
-
- if From = Source'Last + 1 and then From = Through then
- return Source;
- else
- raise Index_Error;
- end if;
-
else
declare
- Front : constant Integer := From - Source'First;
+ Front_Len : constant Integer :=
+ Integer'Max (0, From - Source'First);
+ -- Length of prefix of Source copied to result
+ Back_Len : constant Integer :=
+ Integer'Max (0, Source'Last - Through);
+ -- Length of suffix of Source copied to result
+
+ Result_Length : constant Integer := Front_Len + Back_Len;
+ -- Length of result
begin
- return Result : String (1 .. Source'Length - (Through - From + 1))
+ return Result : String (1 .. Result_Length)
with Relaxed_Initialization
do
- Result (1 .. Front) :=
+ Result (1 .. Front_Len) :=
Source (Source'First .. From - 1);
if Through < Source'Last then
- Result (Front + 1 .. Result'Last) :=
+ Result (Front_Len + 1 .. Result'Last) :=
Source (Through + 1 .. Source'Last);
end if;
end return;
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 9d5e9d92341..aed0851493b 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -1061,9 +1061,9 @@ is
From : Positive;
Through : Natural) return String
with
- Pre => (if From <= Through
- then (From in Source'Range
- and then Through <= Source'Last)),
+ Pre => From > Through
+ or else (From - 1 <= Source'Last
+ and then Through >= Source'First - 1),
-- Lower bound of the returned string is 1
@@ -1079,12 +1079,14 @@ is
-- Length of the returned string
- Delete'Result'Length = Source'Length - (Through - From + 1)
+ Delete'Result'Length =
+ Integer'Max (0, From - Source'First)
+ + Integer'Max (Source'Last - Through, 0)
-- Elements before From are preserved
and then
- Delete'Result (1 .. From - Source'First)
+ Delete'Result (1 .. Integer'Max (0, From - Source'First))
= Source (Source'First .. From - 1)
-- If there are remaining characters after Through, they are
@@ -1092,9 +1094,11 @@ is
and then
(if Through < Source'Last
- then Delete'Result
- (From - Source'First + 1 .. Delete'Result'Last)
- = Source (Through + 1 .. Source'Last)),
+ then
+ Delete'Result
+ (Integer'Max (0, From - Source'First) + 1
+ .. Delete'Result'Last)
+ = Source (Through + 1 .. Source'Last)),
-- Otherwise, the returned string is Source with lower bound 1
--
2.45.2
