diff --git a/regression/jbmc-strings/java_append_object/test.desc b/regression/jbmc-strings/java_append_object/test.desc index 2af06f2686a..ce08e3e17ad 100644 --- a/regression/jbmc-strings/java_append_object/test.desc +++ b/regression/jbmc-strings/java_append_object/test.desc @@ -5,3 +5,5 @@ test_append_object.class ^SIGNAL=0$ ^\[.*assertion\.1\].* line 15.* FAILURE$ -- +-- +Issue: diffblue/test-gen#82 diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class deleted file mode 100644 index 8eb78d4aaa4..00000000000 Binary files a/regression/strings-smoke-tests/cprover/CProverString.class and /dev/null differ diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java deleted file mode 100644 index 0603aac5dc6..00000000000 --- a/regression/strings-smoke-tests/cprover/CProverString.java +++ /dev/null @@ -1,150 +0,0 @@ -package org.cprover; - -public final class CProverString { - public static char charAt(String s, int i) { - if (0 <= i && i < s.length()) - return s.charAt(i); - else - 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; - else if (i >= s.length()) - return ""; - else - return s.substring(i); - } - - public static String substring(String s, int i, int j) { - if (i < 0) - return substring(s, 0, j); - if (j >= s.length()) - return substring(s, 0, s.length() - 1); - if (i >= 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_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc deleted file mode 100644 index 71e874d2486..00000000000 --- a/regression/strings-smoke-tests/java_append_int/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_append_int.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/regression/strings-smoke-tests/java_append_int/test_append_int.class b/regression/strings-smoke-tests/java_append_int/test_append_int.class deleted file mode 100644 index 16948397e03..00000000000 Binary files a/regression/strings-smoke-tests/java_append_int/test_append_int.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_append_int/test_append_int.java b/regression/strings-smoke-tests/java_append_int/test_append_int.java deleted file mode 100644 index 963f3d7c063..00000000000 --- a/regression/strings-smoke-tests/java_append_int/test_append_int.java +++ /dev/null @@ -1,11 +0,0 @@ -public class test_append_int -{ - public static void main(/*String[] args*/) - { - StringBuilder diffblue = new StringBuilder(); - diffblue.append("d"); - diffblue.append(4); - String s = diffblue.toString(); - assert s.equals("d4"); - } -} diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc deleted file mode 100644 index c905a3990f6..00000000000 --- a/regression/strings-smoke-tests/java_append_object/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -FUTURE -test_append_object.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types --- -Issue: diffblue/test-gen#82 diff --git a/regression/strings-smoke-tests/java_append_object/test_append_object.class b/regression/strings-smoke-tests/java_append_object/test_append_object.class deleted file mode 100644 index ed6942a1fa6..00000000000 Binary files a/regression/strings-smoke-tests/java_append_object/test_append_object.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_append_object/test_append_object.java b/regression/strings-smoke-tests/java_append_object/test_append_object.java deleted file mode 100644 index 121690451ca..00000000000 --- a/regression/strings-smoke-tests/java_append_object/test_append_object.java +++ /dev/null @@ -1,17 +0,0 @@ -public class test_append_object -{ - public static void main(/*String[] args*/) - { - Object diff = "diff"; - Object blue = "blue"; - - StringBuilder buffer = new StringBuilder(); - - buffer.append(diff) - .append(blue); - - String tmp=buffer.toString(); - System.out.println(tmp); - assert tmp.equals("diffblue"); - } -}