diff --git a/regression/jbmc-strings/cprover/CProverString.class b/regression/jbmc-strings/cprover/CProverString.class index c1cf5742e39..8eb78d4aaa4 100644 Binary files a/regression/jbmc-strings/cprover/CProverString.class and b/regression/jbmc-strings/cprover/CProverString.class differ diff --git a/regression/jbmc-strings/cprover/CProverString.java b/regression/jbmc-strings/cprover/CProverString.java index 572056b2100..0603aac5dc6 100644 --- a/regression/jbmc-strings/cprover/CProverString.java +++ b/regression/jbmc-strings/cprover/CProverString.java @@ -8,6 +8,29 @@ public static char charAt(String s, int i) { return '\u0000'; } + public static int codePointAt(String s, int index) { + return s.codePointAt(index); + } + + public static int codePointBefore(String s, int index) { + return s.codePointBefore(index); + } + + public static int codePointCount( + String s, int beginIndex, int endIndex) { + return s.codePointCount(beginIndex, endIndex); + } + + public static int offsetByCodePoints( + String s, int index, int codePointOffset) { + return s.offsetByCodePoints(index, codePointOffset); + } + + public static CharSequence subSequence( + String s, int beginIndex, int endIndex) { + return s.subSequence(beginIndex, endIndex); + } + public static String substring(String s, int i) { if (i <= 0) return s; @@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) { return ""; return s.substring(i, j); } + + public static StringBuilder append( + StringBuilder sb, CharSequence cs, int i, int j) { + return sb.append(cs, i, j); + } + + public static StringBuilder delete(StringBuilder sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuilder deleteCharAt(StringBuilder sb, int index) { + return sb.deleteCharAt(index); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, long l) { + return sb.insert(offset, l); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, float f) { + return sb.insert(offset, f); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, double d) { + return sb.insert(offset, d); + } + + public static void setLength(StringBuffer sb, int newLength) { + sb.setLength(newLength); + } + + public static char charAt(StringBuffer sb, int index) { + return sb.charAt(index); + } + + public static void setCharAt(StringBuffer sb, int index, char c) { + sb.setCharAt(index, c); + } + + public static StringBuffer delete( + StringBuffer sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuffer deleteCharAt(StringBuffer sb, int index) { + return sb.deleteCharAt(index); + } + + public static String substring(StringBuffer sb, int start, int end) { + return sb.substring(start, end); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, long l) { + return sb.insert(offset, l); + } } diff --git a/regression/jbmc-strings/java_delete/test_delete.class b/regression/jbmc-strings/java_delete/test_delete.class index 7036ce13c90..251aa67bc18 100644 Binary files a/regression/jbmc-strings/java_delete/test_delete.class and b/regression/jbmc-strings/java_delete/test_delete.class differ diff --git a/regression/jbmc-strings/java_delete/test_delete.java b/regression/jbmc-strings/java_delete/test_delete.java index ea846cd215a..62ea5dbf9ce 100644 --- a/regression/jbmc-strings/java_delete/test_delete.java +++ b/regression/jbmc-strings/java_delete/test_delete.java @@ -3,7 +3,7 @@ public class test_delete public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder("Abc"); - s.delete(1,2); + org.cprover.CProverString.delete(s,1,2); String str = s.toString(); assert(!str.equals("Ac")); } diff --git a/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class index ed3148e2f7e..130e3d10f6c 100644 Binary files a/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class and b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class differ diff --git a/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java index 5f2c995b56b..d43a2845f95 100644 --- a/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java +++ b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java @@ -4,7 +4,7 @@ public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder(); s.append("Abc"); - s.deleteCharAt(1); + org.cprover.CProverString.deleteCharAt(s, 1); String str = s.toString(); assert(!str.equals("Ac")); } diff --git a/regression/jbmc-strings/java_insert_char/test_insert_char.class b/regression/jbmc-strings/java_insert_char/test_insert_char.class index fbf4a82070b..ef129f739d9 100644 Binary files a/regression/jbmc-strings/java_insert_char/test_insert_char.class and b/regression/jbmc-strings/java_insert_char/test_insert_char.class differ diff --git a/regression/jbmc-strings/java_insert_char/test_insert_char.java b/regression/jbmc-strings/java_insert_char/test_insert_char.java index 3a83f03b332..12dcc8cdb90 100644 --- a/regression/jbmc-strings/java_insert_char/test_insert_char.java +++ b/regression/jbmc-strings/java_insert_char/test_insert_char.java @@ -3,7 +3,7 @@ public class test_insert_char public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 'b'); + org.cprover.CProverString.insert(sb, 1, 'b'); String s = sb.toString(); assert(!s.equals("abc")); } diff --git a/regression/jbmc-strings/java_insert_char_array/test.desc b/regression/jbmc-strings/java_insert_char_array/test.desc index 012a7e34e22..0fd3fc08bb0 100644 --- a/regression/jbmc-strings/java_insert_char_array/test.desc +++ b/regression/jbmc-strings/java_insert_char_array/test.desc @@ -3,6 +3,6 @@ test_insert_char_array.class --refine-strings --string-max-length 1000 --function test_insert_char_array.main ^EXIT=10$ ^SIGNAL=0$ -assertion.* line 28.* SUCCESS$ -assertion.* line 30.* FAILURE$ +assertion.* line 26.* SUCCESS$ +assertion.* line 28.* FAILURE$ -- diff --git a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class index 302260031f2..c19a742c0f4 100644 Binary files a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class and b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class differ diff --git a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java index 1f93e00b8da..f392655afc1 100644 --- a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java +++ b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java @@ -11,7 +11,7 @@ public static String stringOfCharArray(char arr[]) public static void insert(StringBuilder sb, int pos, char arr[]) { String s=stringOfCharArray(arr); - sb.insert(pos, s); + org.cprover.CProverString.insert(sb, pos, s); } public static void main(int i) { diff --git a/regression/jbmc-strings/java_insert_int/test_insert_int.class b/regression/jbmc-strings/java_insert_int/test_insert_int.class index cd355c86546..538a5890e2d 100644 Binary files a/regression/jbmc-strings/java_insert_int/test_insert_int.class and b/regression/jbmc-strings/java_insert_int/test_insert_int.class differ diff --git a/regression/jbmc-strings/java_insert_int/test_insert_int.java b/regression/jbmc-strings/java_insert_int/test_insert_int.java index 15a7a2d53f6..2765859866f 100644 --- a/regression/jbmc-strings/java_insert_int/test_insert_int.java +++ b/regression/jbmc-strings/java_insert_int/test_insert_int.java @@ -3,7 +3,7 @@ public class test_insert_int public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 42); + org.cprover.CProverString.insert(sb, 1, 42); String s = sb.toString(); assert(!s.equals("a42c")); } diff --git a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class index d6b470a1f72..9e6a87de460 100644 Binary files a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class and b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class differ diff --git a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java index c976ddd807f..60daceea887 100644 --- a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java +++ b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java @@ -3,8 +3,8 @@ public class test_insert_multiple public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, 'c'); - sb.insert(1, "b"); + org.cprover.CProverString.insert(sb, 1, 'c'); + org.cprover.CProverString.insert(sb, 1, "b"); String s = sb.toString(); assert(!s.equals("abcd")); } diff --git a/regression/jbmc-strings/java_insert_string/test_insert_string.class b/regression/jbmc-strings/java_insert_string/test_insert_string.class index be8f7ad0f79..e5990e07a15 100644 Binary files a/regression/jbmc-strings/java_insert_string/test_insert_string.class and b/regression/jbmc-strings/java_insert_string/test_insert_string.class differ diff --git a/regression/jbmc-strings/java_insert_string/test_insert_string.java b/regression/jbmc-strings/java_insert_string/test_insert_string.java index 028a348122b..50cd222f6ec 100644 --- a/regression/jbmc-strings/java_insert_string/test_insert_string.java +++ b/regression/jbmc-strings/java_insert_string/test_insert_string.java @@ -3,7 +3,7 @@ public class test_insert_string public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, "bc"); + org.cprover.CProverString.insert(sb, 1, "bc"); String s = sb.toString(); assert(!s.equals("abcd")); } diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class index c1cf5742e39..8eb78d4aaa4 100644 Binary files a/regression/strings-smoke-tests/cprover/CProverString.class and b/regression/strings-smoke-tests/cprover/CProverString.class differ diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java index 572056b2100..0603aac5dc6 100644 --- a/regression/strings-smoke-tests/cprover/CProverString.java +++ b/regression/strings-smoke-tests/cprover/CProverString.java @@ -8,6 +8,29 @@ public static char charAt(String s, int i) { return '\u0000'; } + public static int codePointAt(String s, int index) { + return s.codePointAt(index); + } + + public static int codePointBefore(String s, int index) { + return s.codePointBefore(index); + } + + public static int codePointCount( + String s, int beginIndex, int endIndex) { + return s.codePointCount(beginIndex, endIndex); + } + + public static int offsetByCodePoints( + String s, int index, int codePointOffset) { + return s.offsetByCodePoints(index, codePointOffset); + } + + public static CharSequence subSequence( + String s, int beginIndex, int endIndex) { + return s.subSequence(beginIndex, endIndex); + } + public static String substring(String s, int i) { if (i <= 0) return s; @@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) { return ""; return s.substring(i, j); } + + public static StringBuilder append( + StringBuilder sb, CharSequence cs, int i, int j) { + return sb.append(cs, i, j); + } + + public static StringBuilder delete(StringBuilder sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuilder deleteCharAt(StringBuilder sb, int index) { + return sb.deleteCharAt(index); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, long l) { + return sb.insert(offset, l); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, float f) { + return sb.insert(offset, f); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, double d) { + return sb.insert(offset, d); + } + + public static void setLength(StringBuffer sb, int newLength) { + sb.setLength(newLength); + } + + public static char charAt(StringBuffer sb, int index) { + return sb.charAt(index); + } + + public static void setCharAt(StringBuffer sb, int index, char c) { + sb.setCharAt(index, c); + } + + public static StringBuffer delete( + StringBuffer sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuffer deleteCharAt(StringBuffer sb, int index) { + return sb.deleteCharAt(index); + } + + public static String substring(StringBuffer sb, int start, int end) { + return sb.substring(start, end); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, long l) { + return sb.insert(offset, l); + } } diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.class b/regression/strings-smoke-tests/java_append_string/test_append_string.class index 3594e509e87..020199a6854 100644 Binary files a/regression/strings-smoke-tests/java_append_string/test_append_string.class and b/regression/strings-smoke-tests/java_append_string/test_append_string.class differ diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.java b/regression/strings-smoke-tests/java_append_string/test_append_string.java index 83a9ddf9b4c..d5665b01a88 100644 --- a/regression/strings-smoke-tests/java_append_string/test_append_string.java +++ b/regression/strings-smoke-tests/java_append_string/test_append_string.java @@ -17,7 +17,7 @@ public static void check(StringBuilder sb, String str) String init = sb.toString(); if(str.length() >= 4) { - sb.append(str, 2, 4); + org.cprover.CProverString.append(sb, str, 2, 4); String res = sb.toString(); assert(res.startsWith(init)); assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4))); diff --git a/regression/strings-smoke-tests/java_append_string/test_substring.desc b/regression/strings-smoke-tests/java_append_string/test_substring.desc index de4c8675ad1..dfddb22d72b 100644 --- a/regression/strings-smoke-tests/java_append_string/test_substring.desc +++ b/regression/strings-smoke-tests/java_append_string/test_substring.desc @@ -1,6 +1,6 @@ CORE test_append_string.class ---refine-strings --verbosity 10 --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null +--refine-strings --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.*\].* line 22.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.class b/regression/strings-smoke-tests/java_code_point/test_code_point.class index df523be365b..c07bae0ffb5 100644 Binary files a/regression/strings-smoke-tests/java_code_point/test_code_point.class and b/regression/strings-smoke-tests/java_code_point/test_code_point.class differ diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.java b/regression/strings-smoke-tests/java_code_point/test_code_point.java index afc21c44fed..ae782ecddfa 100644 --- a/regression/strings-smoke-tests/java_code_point/test_code_point.java +++ b/regression/strings-smoke-tests/java_code_point/test_code_point.java @@ -3,10 +3,10 @@ public class test_code_point public static void main(/*String[] argv*/) { String s = "!𐤇𐤄𐤋𐤋𐤅"; - assert(s.codePointAt(1) == 67847); - assert(s.codePointBefore(3) == 67847); - assert(s.codePointCount(1,5) >= 2); - assert(s.offsetByCodePoints(1,2) >= 3); + assert(org.cprover.CProverString.codePointAt(s, 1) == 67847); + assert(org.cprover.CProverString.codePointBefore(s, 3) == 67847); + assert(org.cprover.CProverString.codePointCount(s,1,5) >= 2); + assert(org.cprover.CProverString.offsetByCodePoints(s,1,2) >= 3); StringBuilder sb = new StringBuilder(); sb.appendCodePoint(0x10907); assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0)); diff --git a/regression/strings-smoke-tests/java_delete/test_delete.class b/regression/strings-smoke-tests/java_delete/test_delete.class index f18891851b1..44a8fdc10db 100644 Binary files a/regression/strings-smoke-tests/java_delete/test_delete.class and b/regression/strings-smoke-tests/java_delete/test_delete.class differ diff --git a/regression/strings-smoke-tests/java_delete/test_delete.java b/regression/strings-smoke-tests/java_delete/test_delete.java index 13bd09cd075..99298e536c3 100644 --- a/regression/strings-smoke-tests/java_delete/test_delete.java +++ b/regression/strings-smoke-tests/java_delete/test_delete.java @@ -3,7 +3,7 @@ public class test_delete public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder("Abc"); - s.delete(1,2); + org.cprover.CProverString.delete(s,1,2); String str = s.toString(); assert(str.equals("Ac")); } diff --git a/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class index cfd8561e596..d9148dfc211 100644 Binary files a/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class and b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class differ diff --git a/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java index 94787c5283d..2c56fb54b44 100644 --- a/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java +++ b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java @@ -4,7 +4,7 @@ public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder(); s.append("Abc"); - s.deleteCharAt(1); + org.cprover.CProverString.deleteCharAt(s, 1); String str = s.toString(); assert(str.equals("Ac")); } diff --git a/regression/strings-smoke-tests/java_insert_char/test_insert_char.class b/regression/strings-smoke-tests/java_insert_char/test_insert_char.class index 481304a9f6d..e06ee61b130 100644 Binary files a/regression/strings-smoke-tests/java_insert_char/test_insert_char.class and b/regression/strings-smoke-tests/java_insert_char/test_insert_char.class differ diff --git a/regression/strings-smoke-tests/java_insert_char/test_insert_char.java b/regression/strings-smoke-tests/java_insert_char/test_insert_char.java index ac6beb4ffcf..940292296f1 100644 --- a/regression/strings-smoke-tests/java_insert_char/test_insert_char.java +++ b/regression/strings-smoke-tests/java_insert_char/test_insert_char.java @@ -3,7 +3,7 @@ public class test_insert_char public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 'b'); + org.cprover.CProverString.insert(sb, 1, 'b'); String s = sb.toString(); assert(s.equals("abc")); } diff --git a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class index d0edb7e3e24..ceb34bf1896 100644 Binary files a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class and b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class differ diff --git a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java index ab28b86ffdc..543b9aa2024 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java +++ b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java @@ -4,7 +4,7 @@ public static void insert(StringBuilder sb, int offset, char[] arr) { assert(arr.length<5); for(int i=0; i