But sometimes in the string s the final char 0X (which signals the end) is lost, and the postcondition (not explicitly checked) does not hold. The bug is detected afterwards, for example when trying to print the resulted string. For example:PROCEDURE Replace (VAR s: ARRAY OF CHAR; pos, len: INTEGER; IN rep: ARRAY OF CHAR)
Replaces the stretch [pos, MIN(pos+len, Len(s))) in s with the string in rep. The characters after the replaced stretch are moved if necessary. The result is truncated if s is not large enough.
Hint: if len = 0 then rep is inserted in s at position pos. If LEN(rep$) = 0 then the stretch [pos, MIN(pos+len, LEN(s$))) is deleted from s.
Pre
len >= 0 20
pos >= 0 21
Valid(s) & Valid(rep) (not checked)
Post
Valid(s)
Code: Select all
VAR a: ARRAY 5 OF CHAR;
ERROR 1:
a := "ABCD";
Strings.Replace(a, 1, 1, "xy");
StdLog.String(a); <-- index out of range
ERROR 2:
a := "ABCD";
Strings.Replace(a, 1, 0, "x");
StdLog.String(a); <-- index out of range
Code: Select all
PROCEDURE Replace* (VAR s: ARRAY OF CHAR; pos, len: INTEGER; IN rep: ARRAY OF CHAR);
...
ELSE (* insert the remaining part of rep *)
len := LEN(rep$) - j; k := lenS + len;
IF k > max THEN k := max END;
s[k] := 0X; DEC(k); <--- DEC(k) is added
WHILE k - len >= i DO s[k] := s[k-len]; DEC(k) END;
WHILE (rep[j] # 0X) & (i < max) DO s[i] := rep[j]; INC(i); INC(j) END
END
END
END Replace;
Regards