Skip to content

Commit b7ca9fd

Browse files
Model for StringBuilder append of char array
1 parent bb7871b commit b7ca9fd

File tree

1 file changed

+8
-6
lines changed

1 file changed

+8
-6
lines changed

src/main/java/java/lang/StringBuilder.java

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -241,23 +241,25 @@ public StringBuilder append(CharSequence s, int start, int end) {
241241
*/
242242
@Override
243243
public StringBuilder append(char[] str) {
244-
// DIFFBLUE MODEL LIBRARY: Handled internally by CBMC
244+
// DIFFBLUE MODEL LIBRARY
245+
String string = CProverString.ofCharArray(str, 0, str.length);
246+
return append(string);
245247
// super.append(str);
246248
// return this;
247-
return CProver.nondetWithNullForNotModelled();
248249
}
249250

250251
/**
251252
* @throws IndexOutOfBoundsException {@inheritDoc}
252-
*
253-
* @diffblue.noSupport
253+
* @diffblue.fullSupport
254+
* @diffblue.untested
254255
*/
255256
@Override
256257
public StringBuilder append(char[] str, int offset, int len) {
258+
// DIFFBLUE MODEL LIBRARY
259+
String string = new String(str, offset, len);
260+
return append(string);
257261
// super.append(str, offset, len);
258262
// return this;
259-
CProver.notModelled();
260-
return CProver.nondetWithNullForNotModelled();
261263
}
262264

263265
/**

0 commit comments

Comments
 (0)