diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile new file mode 100644 index 00000000000..c41ab1c5be8 --- /dev/null +++ b/regression/strings-smoke-tests/Makefile @@ -0,0 +1,9 @@ + +test: + @../test.pl -c ../../../src/cbmc/cbmc + +testfuture: + @../test.pl -c ../../../src/cbmc/cbmc -CF + +testall: + @../test.pl -c ../../../src/cbmc/cbmc -CFTK diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc new file mode 100644 index 00000000000..0f1b3ae243f --- /dev/null +++ b/regression/strings-smoke-tests/java_append_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_char.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_append_char/test_append_char.class b/regression/strings-smoke-tests/java_append_char/test_append_char.class new file mode 100644 index 00000000000..00c40aef6f6 Binary files /dev/null and b/regression/strings-smoke-tests/java_append_char/test_append_char.class differ diff --git a/regression/strings-smoke-tests/java_append_char/test_append_char.java b/regression/strings-smoke-tests/java_append_char/test_append_char.java new file mode 100644 index 00000000000..3eec4f30abe --- /dev/null +++ b/regression/strings-smoke-tests/java_append_char/test_append_char.java @@ -0,0 +1,17 @@ +public class test_append_char +{ + public static void main(/*String[] args*/) + { + char[] diff = {'d', 'i', 'f', 'f'}; + char[] blue = {'b', 'l', 'u', 'e'}; + + StringBuilder buffer = new StringBuilder(); + + buffer.append(diff) + .append(blue); + + String tmp=buffer.toString(); + System.out.println(tmp); + assert tmp.equals("diffblue"); + } +} diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc new file mode 100644 index 00000000000..e1455859470 --- /dev/null +++ b/regression/strings-smoke-tests/java_append_int/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_int.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..16948397e03 Binary files /dev/null and b/regression/strings-smoke-tests/java_append_int/test_append_int.class 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 new file mode 100644 index 00000000000..963f3d7c063 --- /dev/null +++ b/regression/strings-smoke-tests/java_append_int/test_append_int.java @@ -0,0 +1,11 @@ +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 new file mode 100644 index 00000000000..5db2ac1db73 --- /dev/null +++ b/regression/strings-smoke-tests/java_append_object/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_object.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..ed6942a1fa6 Binary files /dev/null and b/regression/strings-smoke-tests/java_append_object/test_append_object.class 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 new file mode 100644 index 00000000000..121690451ca --- /dev/null +++ b/regression/strings-smoke-tests/java_append_object/test_append_object.java @@ -0,0 +1,17 @@ +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"); + } +} diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc new file mode 100644 index 00000000000..18035539d58 --- /dev/null +++ b/regression/strings-smoke-tests/java_append_string/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_string.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..622e08467f9 Binary files /dev/null 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 new file mode 100644 index 00000000000..e7f961172fa --- /dev/null +++ b/regression/strings-smoke-tests/java_append_string/test_append_string.java @@ -0,0 +1,14 @@ +public class test_append_string +{ + public static void main(/*String[] args*/) + { + String di = new String("di"); + StringBuilder diff = new StringBuilder(); + diff.append(di); + diff.append("ff"); + System.out.println(diff); + String s = diff.toString(); + System.out.println(s); + assert s.equals("diff"); + } +} diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc new file mode 100644 index 00000000000..e01a5054419 --- /dev/null +++ b/regression/strings-smoke-tests/java_case/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_case.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_case/test_case.class b/regression/strings-smoke-tests/java_case/test_case.class new file mode 100644 index 00000000000..9f7eaab446c Binary files /dev/null and b/regression/strings-smoke-tests/java_case/test_case.class differ diff --git a/regression/strings-smoke-tests/java_case/test_case.java b/regression/strings-smoke-tests/java_case/test_case.java new file mode 100644 index 00000000000..b3437a6f83e --- /dev/null +++ b/regression/strings-smoke-tests/java_case/test_case.java @@ -0,0 +1,12 @@ +public class test_case +{ + public static void main(/*String[] argv*/) + { + String s = new String("Ab"); + String l = s.toLowerCase(); + String u = s.toUpperCase(); + assert(l.equals("ab")); + assert(u.equals("AB")); + assert(s.equalsIgnoreCase("aB")); + } +} diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc new file mode 100644 index 00000000000..ecce56c1ab8 --- /dev/null +++ b/regression/strings-smoke-tests/java_char_array/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_char_array.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.class b/regression/strings-smoke-tests/java_char_array/test_char_array.class new file mode 100644 index 00000000000..0d2056042ca Binary files /dev/null and b/regression/strings-smoke-tests/java_char_array/test_char_array.class differ diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.java b/regression/strings-smoke-tests/java_char_array/test_char_array.java new file mode 100644 index 00000000000..017fe704124 --- /dev/null +++ b/regression/strings-smoke-tests/java_char_array/test_char_array.java @@ -0,0 +1,13 @@ +public class test_char_array +{ + public static void main(/*String[] argv*/) + { + String s = "abc"; + char [] str = s.toCharArray(); + char c = str[2]; + char a = s.charAt(0); + assert(str.length == 3); + assert(a == 'a'); + assert(c == 'c'); + } +} diff --git a/regression/strings-smoke-tests/java_char_array_init/test.desc b/regression/strings-smoke-tests/java_char_array_init/test.desc new file mode 100644 index 00000000000..fc1cde2392c --- /dev/null +++ b/regression/strings-smoke-tests/java_char_array_init/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_init.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_char_array_init/test_init.class b/regression/strings-smoke-tests/java_char_array_init/test_init.class new file mode 100644 index 00000000000..48075eb9187 Binary files /dev/null and b/regression/strings-smoke-tests/java_char_array_init/test_init.class differ diff --git a/regression/strings-smoke-tests/java_char_array_init/test_init.java b/regression/strings-smoke-tests/java_char_array_init/test_init.java new file mode 100644 index 00000000000..8e0f656e3e8 --- /dev/null +++ b/regression/strings-smoke-tests/java_char_array_init/test_init.java @@ -0,0 +1,21 @@ +public class test_init { + + public static void main(/*String[] argv*/) + { + char [] str = new char[10]; + str[0] = 'H'; + str[1] = 'e'; + str[2] = 'l'; + str[3] = 'l'; + str[4] = 'o'; + String s = new String(str); + String t = new String(str,1,2); + + System.out.println(s.length()); + assert(s.length() == 10); + System.out.println(s); + System.out.println(t); + assert(t.equals("el")); + assert(s.startsWith("Hello")); + } +} diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc new file mode 100644 index 00000000000..5bf29fc7a4d --- /dev/null +++ b/regression/strings-smoke-tests/java_char_at/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_char_at.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.class b/regression/strings-smoke-tests/java_char_at/test_char_at.class new file mode 100644 index 00000000000..de5fe888245 Binary files /dev/null and b/regression/strings-smoke-tests/java_char_at/test_char_at.class differ diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.java b/regression/strings-smoke-tests/java_char_at/test_char_at.java new file mode 100644 index 00000000000..3b8663d62ae --- /dev/null +++ b/regression/strings-smoke-tests/java_char_at/test_char_at.java @@ -0,0 +1,7 @@ +public class test_char_at { + + public static void main(/*String[] argv*/) { + String s = new String("abc"); + assert(s.charAt(2)=='c'); + } +} diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc new file mode 100644 index 00000000000..012c7c3501b --- /dev/null +++ b/regression/strings-smoke-tests/java_code_point/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_code_point.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..1d5d2269325 Binary files /dev/null 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 new file mode 100644 index 00000000000..faf9a2051d5 --- /dev/null +++ b/regression/strings-smoke-tests/java_code_point/test_code_point.java @@ -0,0 +1,14 @@ +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); + StringBuilder sb = new StringBuilder(); + sb.appendCodePoint(0x10907); + assert(s.charAt(1) == sb.charAt(0)); + } +} diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc new file mode 100644 index 00000000000..38aa025f416 --- /dev/null +++ b/regression/strings-smoke-tests/java_compare/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_compare.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_compare/test_compare.class b/regression/strings-smoke-tests/java_compare/test_compare.class new file mode 100644 index 00000000000..3a807f4d203 Binary files /dev/null and b/regression/strings-smoke-tests/java_compare/test_compare.class differ diff --git a/regression/strings-smoke-tests/java_compare/test_compare.java b/regression/strings-smoke-tests/java_compare/test_compare.java new file mode 100644 index 00000000000..c052ed429bd --- /dev/null +++ b/regression/strings-smoke-tests/java_compare/test_compare.java @@ -0,0 +1,9 @@ +public class test_compare +{ + public static void main(/*String[] argv*/) + { + String s1 = "ab"; + String s2 = "aa"; + assert(s1.compareTo(s2) == 1); + } +} diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc new file mode 100644 index 00000000000..fb784efd723 --- /dev/null +++ b/regression/strings-smoke-tests/java_concat/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_concat.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 10.* SUCCESS$ +^\[.*assertion.2\].* line 11.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_concat/test_concat.class b/regression/strings-smoke-tests/java_concat/test_concat.class new file mode 100644 index 00000000000..e4143c15773 Binary files /dev/null and b/regression/strings-smoke-tests/java_concat/test_concat.class differ diff --git a/regression/strings-smoke-tests/java_concat/test_concat.java b/regression/strings-smoke-tests/java_concat/test_concat.java new file mode 100644 index 00000000000..b9909c723d4 --- /dev/null +++ b/regression/strings-smoke-tests/java_concat/test_concat.java @@ -0,0 +1,13 @@ +public class test_concat +{ + public static void main(/*String[] argv*/) + { + String s = new String("pi"); + int i = s.length(); + String t = new String("ppo"); + String u = s.concat(t); + char c = u.charAt(i); + assert(c == 'p'); + assert(c == 'o'); + } +} diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc new file mode 100644 index 00000000000..2b96346d718 --- /dev/null +++ b/regression/strings-smoke-tests/java_contains/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_contains.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_contains/test_contains.class b/regression/strings-smoke-tests/java_contains/test_contains.class new file mode 100644 index 00000000000..adf0ece000a Binary files /dev/null and b/regression/strings-smoke-tests/java_contains/test_contains.class differ diff --git a/regression/strings-smoke-tests/java_contains/test_contains.java b/regression/strings-smoke-tests/java_contains/test_contains.java new file mode 100644 index 00000000000..5112c344c09 --- /dev/null +++ b/regression/strings-smoke-tests/java_contains/test_contains.java @@ -0,0 +1,11 @@ +public class test_contains +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abc"); + String u = "bc"; + String t = "ab"; + assert(s.contains(u)); + assert(s.contains(t)); + } +} diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc new file mode 100644 index 00000000000..27a1406cdb7 --- /dev/null +++ b/regression/strings-smoke-tests/java_delete/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_delete.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_delete/test_delete.class b/regression/strings-smoke-tests/java_delete/test_delete.class new file mode 100644 index 00000000000..f18891851b1 Binary files /dev/null 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 new file mode 100644 index 00000000000..13bd09cd075 --- /dev/null +++ b/regression/strings-smoke-tests/java_delete/test_delete.java @@ -0,0 +1,10 @@ +public class test_delete +{ + public static void main(/*String[] argv*/) + { + StringBuilder s = new StringBuilder("Abc"); + s.delete(1,2); + String str = s.toString(); + assert(str.equals("Ac")); + } +} diff --git a/regression/strings-smoke-tests/java_delete_char_at/test.desc b/regression/strings-smoke-tests/java_delete_char_at/test.desc new file mode 100644 index 00000000000..94ba56a2c54 --- /dev/null +++ b/regression/strings-smoke-tests/java_delete_char_at/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_delete_char_at.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..cfd8561e596 Binary files /dev/null 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 new file mode 100644 index 00000000000..94787c5283d --- /dev/null +++ b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java @@ -0,0 +1,11 @@ +public class test_delete_char_at +{ + public static void main(/*String[] argv*/) + { + StringBuilder s = new StringBuilder(); + s.append("Abc"); + s.deleteCharAt(1); + String str = s.toString(); + assert(str.equals("Ac")); + } +} diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc new file mode 100644 index 00000000000..9951c8a13ee --- /dev/null +++ b/regression/strings-smoke-tests/java_empty/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_empty.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_empty/test_empty.class b/regression/strings-smoke-tests/java_empty/test_empty.class new file mode 100644 index 00000000000..8e9a17d387e Binary files /dev/null and b/regression/strings-smoke-tests/java_empty/test_empty.class differ diff --git a/regression/strings-smoke-tests/java_empty/test_empty.java b/regression/strings-smoke-tests/java_empty/test_empty.java new file mode 100644 index 00000000000..47c335e16fa --- /dev/null +++ b/regression/strings-smoke-tests/java_empty/test_empty.java @@ -0,0 +1,8 @@ +public class test_empty +{ + public static void main(/*String[] argv*/) + { + String empty = ""; + assert(empty.isEmpty()); + } +} diff --git a/regression/strings-smoke-tests/java_endswith/test.desc b/regression/strings-smoke-tests/java_endswith/test.desc new file mode 100644 index 00000000000..0461a3e50e6 --- /dev/null +++ b/regression/strings-smoke-tests/java_endswith/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_endswith.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 9.* SUCCESS$ +^\[.*assertion.2\].* line 10.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_endswith/test_endswith.class b/regression/strings-smoke-tests/java_endswith/test_endswith.class new file mode 100644 index 00000000000..1f86e94431d Binary files /dev/null and b/regression/strings-smoke-tests/java_endswith/test_endswith.class differ diff --git a/regression/strings-smoke-tests/java_endswith/test_endswith.java b/regression/strings-smoke-tests/java_endswith/test_endswith.java new file mode 100644 index 00000000000..f7729ef6a40 --- /dev/null +++ b/regression/strings-smoke-tests/java_endswith/test_endswith.java @@ -0,0 +1,12 @@ +public class test_endswith +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abcd"); + String suff = "cd"; + String bad_suff = "bc"; + + assert(s.endsWith(suff)); + assert(s.endsWith(bad_suff)); + } +} diff --git a/regression/strings-smoke-tests/java_equal/test.desc b/regression/strings-smoke-tests/java_equal/test.desc new file mode 100644 index 00000000000..05f0f383230 --- /dev/null +++ b/regression/strings-smoke-tests/java_equal/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_equal.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* FAILURE$ +^\[.*assertion.2\].* line 9.* SUCCESS$ +-- diff --git a/regression/strings-smoke-tests/java_equal/test_equal.class b/regression/strings-smoke-tests/java_equal/test_equal.class new file mode 100644 index 00000000000..e0fc6db8aaf Binary files /dev/null and b/regression/strings-smoke-tests/java_equal/test_equal.class differ diff --git a/regression/strings-smoke-tests/java_equal/test_equal.java b/regression/strings-smoke-tests/java_equal/test_equal.java new file mode 100644 index 00000000000..a3acb0ebda5 --- /dev/null +++ b/regression/strings-smoke-tests/java_equal/test_equal.java @@ -0,0 +1,11 @@ +public class test_equal +{ + public static void main(String[] argv) + { + String s = new String("pi"); + String t = new String("po"); + String u = "po"; + assert(s.equals(t)); + assert(t.equals(u)); + } +} diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc new file mode 100644 index 00000000000..427d1fca836 --- /dev/null +++ b/regression/strings-smoke-tests/java_float/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_float.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_float/test_float.class b/regression/strings-smoke-tests/java_float/test_float.class new file mode 100644 index 00000000000..e4448d41558 Binary files /dev/null and b/regression/strings-smoke-tests/java_float/test_float.class differ diff --git a/regression/strings-smoke-tests/java_float/test_float.java b/regression/strings-smoke-tests/java_float/test_float.java new file mode 100644 index 00000000000..d2791d5c343 --- /dev/null +++ b/regression/strings-smoke-tests/java_float/test_float.java @@ -0,0 +1,15 @@ +public class test_float +{ + public static void main(/*String[] arg*/) + { + float inf = 100.0f / 0.0f; + float minus_inf = -100.0f / 0.0f; + float nan = 0.0f / 0.0f; + String inf_string = Float.toString(inf); + String mininf_string = Float.toString(minus_inf); + String nan_string = Float.toString(nan); + assert(nan_string.equals("NaN")); + assert(inf_string.equals("Infinity")); + assert(mininf_string.equals("-Infinity")); + } +} diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc new file mode 100644 index 00000000000..2db8d7116f9 --- /dev/null +++ b/regression/strings-smoke-tests/java_hash_code/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_hash_code.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_hash_code/test_hash_code.class b/regression/strings-smoke-tests/java_hash_code/test_hash_code.class new file mode 100644 index 00000000000..21bc5d96ca9 Binary files /dev/null and b/regression/strings-smoke-tests/java_hash_code/test_hash_code.class differ diff --git a/regression/strings-smoke-tests/java_hash_code/test_hash_code.java b/regression/strings-smoke-tests/java_hash_code/test_hash_code.java new file mode 100644 index 00000000000..d9f42b7ff9d --- /dev/null +++ b/regression/strings-smoke-tests/java_hash_code/test_hash_code.java @@ -0,0 +1,11 @@ +public class test_hash_code +{ + public static void main(/*String[] argv*/) + { + String s1 = "ab"; + String s2 = "ab"; + String s3 = "aa"; + assert(s1.hashCode() == s2.hashCode()); + assert(s1.hashCode() == s3.hashCode()); + } +} diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc new file mode 100644 index 00000000000..f2fa825597d --- /dev/null +++ b/regression/strings-smoke-tests/java_index_of/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_index_of.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.class b/regression/strings-smoke-tests/java_index_of/test_index_of.class new file mode 100644 index 00000000000..1acb3335d57 Binary files /dev/null and b/regression/strings-smoke-tests/java_index_of/test_index_of.class differ diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.java b/regression/strings-smoke-tests/java_index_of/test_index_of.java new file mode 100644 index 00000000000..270267196c5 --- /dev/null +++ b/regression/strings-smoke-tests/java_index_of/test_index_of.java @@ -0,0 +1,10 @@ +public class test_index_of +{ + public static void main(/*String[] argv*/) + { + String s = "Abc"; + String bc = "bc"; + int i = s.indexOf(bc); + assert(i == 1); + } +} diff --git a/regression/strings-smoke-tests/java_index_of_char/test.desc b/regression/strings-smoke-tests/java_index_of_char/test.desc new file mode 100644 index 00000000000..63382a455f3 --- /dev/null +++ b/regression/strings-smoke-tests/java_index_of_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_index_of_char.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.class b/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.class new file mode 100644 index 00000000000..f87a1026683 Binary files /dev/null and b/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.class differ diff --git a/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java b/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java new file mode 100644 index 00000000000..6a5d3d60bd6 --- /dev/null +++ b/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java @@ -0,0 +1,10 @@ +public class test_index_of_char +{ + public static void main(/*String[] argv*/) + { + String s = "Abc"; + char c = 'c'; + int i = s.indexOf(c); + assert(i == 2); + } +} diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc new file mode 100644 index 00000000000..77d3ce2ebd9 --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_char.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..481304a9f6d Binary files /dev/null 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 new file mode 100644 index 00000000000..ac6beb4ffcf --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_char/test_insert_char.java @@ -0,0 +1,10 @@ +public class test_insert_char +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ac"); + sb.insert(1, 'b'); + String s = sb.toString(); + assert(s.equals("abc")); + } +} diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc new file mode 100644 index 00000000000..d48c601b61b --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_char_array.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- 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 new file mode 100644 index 00000000000..3c0b5329230 Binary files /dev/null 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 new file mode 100644 index 00000000000..2c2840df672 --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java @@ -0,0 +1,14 @@ +public class test_insert_char_array +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + char[] array = new char[2]; + array[0] = 'b'; + array[1] = 'c'; + sb.insert(1, array); + String s = sb.toString(); + System.out.println(s); + assert(s.equals("abcd")); + } +} diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc new file mode 100644 index 00000000000..dc039fedbea --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_int/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_int.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_insert_int/test_insert_int.class b/regression/strings-smoke-tests/java_insert_int/test_insert_int.class new file mode 100644 index 00000000000..8b0121ec681 Binary files /dev/null and b/regression/strings-smoke-tests/java_insert_int/test_insert_int.class differ diff --git a/regression/strings-smoke-tests/java_insert_int/test_insert_int.java b/regression/strings-smoke-tests/java_insert_int/test_insert_int.java new file mode 100644 index 00000000000..b787141e51a --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_int/test_insert_int.java @@ -0,0 +1,10 @@ +public class test_insert_int +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ac"); + sb.insert(1, 42); + String s = sb.toString(); + assert(s.equals("a42c")); + } +} diff --git a/regression/strings-smoke-tests/java_insert_multiple/.test_insert.java.swp b/regression/strings-smoke-tests/java_insert_multiple/.test_insert.java.swp new file mode 100644 index 00000000000..5596a2c906d Binary files /dev/null and b/regression/strings-smoke-tests/java_insert_multiple/.test_insert.java.swp differ diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc new file mode 100644 index 00000000000..983d416dd3b --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_multiple/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_multiple.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class new file mode 100644 index 00000000000..17ced6ec67c Binary files /dev/null and b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class differ diff --git a/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java new file mode 100644 index 00000000000..cce6881ca7d --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java @@ -0,0 +1,11 @@ +public class test_insert_multiple +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + sb.insert(1, 'c'); + sb.insert(1, "b"); + String s = sb.toString(); + assert(s.equals("abcd")); + } +} diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc new file mode 100644 index 00000000000..b438d32d6d9 --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_string/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_string.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_insert_string/test_insert_string.class b/regression/strings-smoke-tests/java_insert_string/test_insert_string.class new file mode 100644 index 00000000000..39cc969a902 Binary files /dev/null and b/regression/strings-smoke-tests/java_insert_string/test_insert_string.class differ diff --git a/regression/strings-smoke-tests/java_insert_string/test_insert_string.java b/regression/strings-smoke-tests/java_insert_string/test_insert_string.java new file mode 100644 index 00000000000..7c161205131 --- /dev/null +++ b/regression/strings-smoke-tests/java_insert_string/test_insert_string.java @@ -0,0 +1,10 @@ +public class test_insert_string +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + sb.insert(1, "bc"); + String s = sb.toString(); + assert(s.equals("abcd")); + } +} diff --git a/regression/strings-smoke-tests/java_int_to_string/test.desc b/regression/strings-smoke-tests/java_int_to_string/test.desc new file mode 100644 index 00000000000..a615a10f538 --- /dev/null +++ b/regression/strings-smoke-tests/java_int_to_string/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_int.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.class b/regression/strings-smoke-tests/java_int_to_string/test_int.class new file mode 100644 index 00000000000..eff0e5a422e Binary files /dev/null and b/regression/strings-smoke-tests/java_int_to_string/test_int.class differ diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.java b/regression/strings-smoke-tests/java_int_to_string/test_int.java new file mode 100644 index 00000000000..f46411ed166 --- /dev/null +++ b/regression/strings-smoke-tests/java_int_to_string/test_int.java @@ -0,0 +1,11 @@ +public class test_int +{ + public static void main(/*String[] argv*/) + { + String s = Integer.toString(12); + assert(s.equals("12")); + String t = Integer.toString(-23); + System.out.println(t); + assert(t.equals("-23")); + } +} diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc new file mode 100644 index 00000000000..645e267029c --- /dev/null +++ b/regression/strings-smoke-tests/java_intern/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_intern.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 9.* SUCCESS$ +-- diff --git a/regression/strings-smoke-tests/java_intern/test_intern.class b/regression/strings-smoke-tests/java_intern/test_intern.class new file mode 100644 index 00000000000..894615c0a9a Binary files /dev/null and b/regression/strings-smoke-tests/java_intern/test_intern.class differ diff --git a/regression/strings-smoke-tests/java_intern/test_intern.java b/regression/strings-smoke-tests/java_intern/test_intern.java new file mode 100644 index 00000000000..7f9d5283597 --- /dev/null +++ b/regression/strings-smoke-tests/java_intern/test_intern.java @@ -0,0 +1,11 @@ +public class test_intern +{ + public static void main(/*String[] argv*/) + { + String s1 = "abc"; + String s3 = "abc"; + String x = s1.intern(); + String y = s3.intern(); + assert(x == y); + } +} diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc new file mode 100644 index 00000000000..77bc5b7f18f --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_last_index_of.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class new file mode 100644 index 00000000000..4455da4d179 Binary files /dev/null and b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class differ diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java new file mode 100644 index 00000000000..8b3a0904d5b --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java @@ -0,0 +1,10 @@ +public class test_last_index_of +{ + public static void main(/*String[] argv*/) + { + String s = "abcab"; + String ab = "ab"; + int i = s.lastIndexOf(ab); + assert(i == 3); + } +} diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/regression/strings-smoke-tests/java_last_index_of_char/test.desc new file mode 100644 index 00000000000..3e9a3d4b547 --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_last_index_of_char.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.class b/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.class new file mode 100644 index 00000000000..388717f4261 Binary files /dev/null and b/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.class differ diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java b/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java new file mode 100644 index 00000000000..029d59c9d68 --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java @@ -0,0 +1,9 @@ +public class test_last_index_of_char +{ + public static void main(/*String[] argv*/) + { + String s = "abcab"; + int n = s.lastIndexOf('a'); + assert(n == 3); + } +} diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc new file mode 100644 index 00000000000..913afbf13c7 --- /dev/null +++ b/regression/strings-smoke-tests/java_length/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_length.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_length/test_length.class b/regression/strings-smoke-tests/java_length/test_length.class new file mode 100644 index 00000000000..9273d09869b Binary files /dev/null and b/regression/strings-smoke-tests/java_length/test_length.class differ diff --git a/regression/strings-smoke-tests/java_length/test_length.java b/regression/strings-smoke-tests/java_length/test_length.java new file mode 100644 index 00000000000..4222414fa80 --- /dev/null +++ b/regression/strings-smoke-tests/java_length/test_length.java @@ -0,0 +1,9 @@ +public class test_length +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abc"); + int l = s.length(); + assert(l == 3); + } +} diff --git a/regression/strings-smoke-tests/java_parseint/test.desc b/regression/strings-smoke-tests/java_parseint/test.desc new file mode 100644 index 00000000000..9cb70f5a957 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_parseint.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 7.* SUCCESS$ +^\[.*assertion.2\].* line 8.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.class b/regression/strings-smoke-tests/java_parseint/test_parseint.class new file mode 100644 index 00000000000..e1ffe0c7210 Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint/test_parseint.class differ diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.java b/regression/strings-smoke-tests/java_parseint/test_parseint.java new file mode 100644 index 00000000000..f278f273675 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint/test_parseint.java @@ -0,0 +1,10 @@ +public class test_parseint +{ + public static void main(String[] argv) + { + String twelve = new String("12"); + int parsed = Integer.parseInt(twelve); + assert(parsed == 12); + assert(parsed != 12); + } +} diff --git a/regression/strings-smoke-tests/java_replace/test.desc b/regression/strings-smoke-tests/java_replace/test.desc new file mode 100644 index 00000000000..59c7d326a0b --- /dev/null +++ b/regression/strings-smoke-tests/java_replace/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_replace.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_replace/test_replace.class b/regression/strings-smoke-tests/java_replace/test_replace.class new file mode 100644 index 00000000000..d15509ee8ac Binary files /dev/null and b/regression/strings-smoke-tests/java_replace/test_replace.class differ diff --git a/regression/strings-smoke-tests/java_replace/test_replace.java b/regression/strings-smoke-tests/java_replace/test_replace.java new file mode 100644 index 00000000000..07e7ac036b9 --- /dev/null +++ b/regression/strings-smoke-tests/java_replace/test_replace.java @@ -0,0 +1,13 @@ +public class test_replace +{ + public static void main(/*String[] argv*/) + { + String s = new String("abcabd"); + String u = s.replace("d","z"); + System.out.println(u); + assert(u.equals("abcabz")); + String v = u.replace("ab","w"); + System.out.println(v); + assert(v.equals("wcwz")); + } +} diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc new file mode 100644 index 00000000000..528d4eead6c --- /dev/null +++ b/regression/strings-smoke-tests/java_replace_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_replace_char.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_replace_char/test_replace_char.class b/regression/strings-smoke-tests/java_replace_char/test_replace_char.class new file mode 100644 index 00000000000..64626b3b09d Binary files /dev/null and b/regression/strings-smoke-tests/java_replace_char/test_replace_char.class differ diff --git a/regression/strings-smoke-tests/java_replace_char/test_replace_char.java b/regression/strings-smoke-tests/java_replace_char/test_replace_char.java new file mode 100644 index 00000000000..82a023924e2 --- /dev/null +++ b/regression/strings-smoke-tests/java_replace_char/test_replace_char.java @@ -0,0 +1,9 @@ +public class test_replace_char +{ + public static void main(/*String[] argv*/) + { + String s = new String("abcabd"); + String t = s.replace('b','m'); + assert(t.equals("amcamd")); + } +} diff --git a/regression/strings-smoke-tests/java_set_char_at/test.desc b/regression/strings-smoke-tests/java_set_char_at/test.desc new file mode 100644 index 00000000000..650e7712278 --- /dev/null +++ b/regression/strings-smoke-tests/java_set_char_at/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_set_char_at.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class new file mode 100644 index 00000000000..6e843afbe2a Binary files /dev/null and b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class differ diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java new file mode 100644 index 00000000000..fd1d1fbf9e2 --- /dev/null +++ b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java @@ -0,0 +1,13 @@ +public class test_set_char_at +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abc"); + char c = s.charAt(1); + StringBuilder sb = new StringBuilder(s); + sb.setCharAt(1,'w'); + s = sb.toString(); + assert(s.equals("Awc")); + assert(s.charAt(2)=='c'); + } +} diff --git a/regression/strings-smoke-tests/java_set_length/test.desc b/regression/strings-smoke-tests/java_set_length/test.desc new file mode 100644 index 00000000000..ab59e459eb1 --- /dev/null +++ b/regression/strings-smoke-tests/java_set_length/test.desc @@ -0,0 +1,9 @@ +FUTURE +test_set_length.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* SUCCESS$ +^\[.*assertion.3\].* line 10.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_set_length/test_set_length.class b/regression/strings-smoke-tests/java_set_length/test_set_length.class new file mode 100644 index 00000000000..8cb9e416191 Binary files /dev/null and b/regression/strings-smoke-tests/java_set_length/test_set_length.class differ diff --git a/regression/strings-smoke-tests/java_set_length/test_set_length.java b/regression/strings-smoke-tests/java_set_length/test_set_length.java new file mode 100644 index 00000000000..5894b27beeb --- /dev/null +++ b/regression/strings-smoke-tests/java_set_length/test_set_length.java @@ -0,0 +1,12 @@ +public class test_set_length +{ + public static void main(/*String[] argv*/) + { + StringBuilder s = new StringBuilder("abc"); + s.setLength(10); + String t = s.toString(); + assert(t.startsWith("abc")); + assert(t.length() == 10); + assert(t.length() == 3); + } +} diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc new file mode 100644 index 00000000000..5c5d85565c2 --- /dev/null +++ b/regression/strings-smoke-tests/java_starts_with/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_starts_with.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_starts_with/test_starts_with.class b/regression/strings-smoke-tests/java_starts_with/test_starts_with.class new file mode 100644 index 00000000000..da1decd8d35 Binary files /dev/null and b/regression/strings-smoke-tests/java_starts_with/test_starts_with.class differ diff --git a/regression/strings-smoke-tests/java_starts_with/test_starts_with.java b/regression/strings-smoke-tests/java_starts_with/test_starts_with.java new file mode 100644 index 00000000000..aba79d846c0 --- /dev/null +++ b/regression/strings-smoke-tests/java_starts_with/test_starts_with.java @@ -0,0 +1,11 @@ +public class test_starts_with +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abcd"); + String pref = "Ab"; + String bad_pref = "bc"; + assert(s.startsWith(pref)); + assert(s.startsWith(bad_pref)); + } +} diff --git a/regression/strings-smoke-tests/java_string_builder_length/test.desc b/regression/strings-smoke-tests/java_string_builder_length/test.desc new file mode 100644 index 00000000000..ba9187109ed --- /dev/null +++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_sb_length.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.class b/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.class new file mode 100644 index 00000000000..cfc35874d26 Binary files /dev/null and b/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.class differ diff --git a/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java b/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java new file mode 100644 index 00000000000..b616749ffb4 --- /dev/null +++ b/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java @@ -0,0 +1,9 @@ +public class test_sb_length +{ + public static void main(/*String[] argv*/) + { + StringBuilder x = new StringBuilder("abc"); + x.append("de"); + assert(x.length() == 5); + } +} diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc new file mode 100644 index 00000000000..34585a7900d --- /dev/null +++ b/regression/strings-smoke-tests/java_subsequence/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_subsequence.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_subsequence/test_subsequence.class b/regression/strings-smoke-tests/java_subsequence/test_subsequence.class new file mode 100644 index 00000000000..0f8410939e1 Binary files /dev/null and b/regression/strings-smoke-tests/java_subsequence/test_subsequence.class differ diff --git a/regression/strings-smoke-tests/java_subsequence/test_subsequence.java b/regression/strings-smoke-tests/java_subsequence/test_subsequence.java new file mode 100644 index 00000000000..4d8d79cb381 --- /dev/null +++ b/regression/strings-smoke-tests/java_subsequence/test_subsequence.java @@ -0,0 +1,14 @@ +public class test_subsequence +{ + public static void main(/*String[] argv*/) + { + String abcdef = "AbcDef"; + CharSequence cde = abcdef.subSequence(2,5); + char c = cde.charAt(0); + char d = cde.charAt(1); + char e = cde.charAt(2); + assert(c == 'c'); + assert(d == 'D'); + assert(e == 'e'); + } +} diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc new file mode 100644 index 00000000000..8a29460f529 --- /dev/null +++ b/regression/strings-smoke-tests/java_substring/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_substring.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_substring/test_substring.class b/regression/strings-smoke-tests/java_substring/test_substring.class new file mode 100644 index 00000000000..3ba0b60e7f2 Binary files /dev/null and b/regression/strings-smoke-tests/java_substring/test_substring.class differ diff --git a/regression/strings-smoke-tests/java_substring/test_substring.java b/regression/strings-smoke-tests/java_substring/test_substring.java new file mode 100644 index 00000000000..03a33fdbebd --- /dev/null +++ b/regression/strings-smoke-tests/java_substring/test_substring.java @@ -0,0 +1,14 @@ +public class test_substring +{ + public static void main(/*String[] argv*/) + { + String abcdef = "AbcDef"; + String cde = abcdef.substring(2,5); + char c = cde.charAt(0); + char d = cde.charAt(1); + char e = cde.charAt(2); + assert(c == 'c'); + assert(d == 'D'); + assert(e == 'e'); + } +} diff --git a/regression/strings-smoke-tests/java_trim/test.desc b/regression/strings-smoke-tests/java_trim/test.desc new file mode 100644 index 00000000000..c7a307c37ed --- /dev/null +++ b/regression/strings-smoke-tests/java_trim/test.desc @@ -0,0 +1,8 @@ +FUTURE +test_trim.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 6.* SUCCESS$ +^\[.*assertion.2\].* line 7.* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_trim/test_trim.class b/regression/strings-smoke-tests/java_trim/test_trim.class new file mode 100644 index 00000000000..33b34714ae2 Binary files /dev/null and b/regression/strings-smoke-tests/java_trim/test_trim.class differ diff --git a/regression/strings-smoke-tests/java_trim/test_trim.java b/regression/strings-smoke-tests/java_trim/test_trim.java new file mode 100644 index 00000000000..20dd7ba2796 --- /dev/null +++ b/regression/strings-smoke-tests/java_trim/test_trim.java @@ -0,0 +1,9 @@ +public class test_trim +{ + public static void main(/*String[] argv*/) + { + String empty = " "; + assert(empty.trim().isEmpty()); + assert(empty.isEmpty()); + } +} diff --git a/regression/strings/RegexMatches01/test.desc b/regression/strings/RegexMatches01/test.desc index 45cc542b352..e4259466e6b 100644 --- a/regression/strings/RegexMatches01/test.desc +++ b/regression/strings/RegexMatches01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches01.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/RegexMatches02/test.desc b/regression/strings/RegexMatches02/test.desc index 86353d9a54c..006922c3d6a 100644 --- a/regression/strings/RegexMatches02/test.desc +++ b/regression/strings/RegexMatches02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches02.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/RegexSubstitution01/test.desc b/regression/strings/RegexSubstitution01/test.desc index bc7ed3648f3..ccf24b2e8fa 100644 --- a/regression/strings/RegexSubstitution01/test.desc +++ b/regression/strings/RegexSubstitution01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/RegexSubstitution02/test.desc b/regression/strings/RegexSubstitution02/test.desc index 0645c3ac9b8..7064bcc0333 100644 --- a/regression/strings/RegexSubstitution02/test.desc +++ b/regression/strings/RegexSubstitution02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/RegexSubstitution03/test.desc b/regression/strings/RegexSubstitution03/test.desc index 20da1478b1a..4b0d5739c42 100644 --- a/regression/strings/RegexSubstitution03/test.desc +++ b/regression/strings/RegexSubstitution03/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution03.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StaticCharMethods01/test.desc b/regression/strings/StaticCharMethods01/test.desc index 4b633e92bcf..a40f4534120 100644 --- a/regression/strings/StaticCharMethods01/test.desc +++ b/regression/strings/StaticCharMethods01/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StaticCharMethods02/test.desc b/regression/strings/StaticCharMethods02/test.desc index 00aaaba8964..9366df6fa57 100644 --- a/regression/strings/StaticCharMethods02/test.desc +++ b/regression/strings/StaticCharMethods02/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods03/test.desc b/regression/strings/StaticCharMethods03/test.desc index 6f3d3bc5607..caba8503984 100644 --- a/regression/strings/StaticCharMethods03/test.desc +++ b/regression/strings/StaticCharMethods03/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods04/test.desc b/regression/strings/StaticCharMethods04/test.desc index 0c9484ef337..1f686c041c2 100644 --- a/regression/strings/StaticCharMethods04/test.desc +++ b/regression/strings/StaticCharMethods04/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/strings/StaticCharMethods05/test.desc index 5b4a6b4b622..b21901ac84a 100644 --- a/regression/strings/StaticCharMethods05/test.desc +++ b/regression/strings/StaticCharMethods05/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods05.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods06/test.desc b/regression/strings/StaticCharMethods06/test.desc index 6f351b2c7cf..3caa6a7b878 100644 --- a/regression/strings/StaticCharMethods06/test.desc +++ b/regression/strings/StaticCharMethods06/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods06.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderAppend01/test.desc b/regression/strings/StringBuilderAppend01/test.desc index f1f89b629be..d0207fc9ea7 100644 --- a/regression/strings/StringBuilderAppend01/test.desc +++ b/regression/strings/StringBuilderAppend01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderAppend02/test.desc b/regression/strings/StringBuilderAppend02/test.desc index 1336c45c3d2..70357b670d8 100644 --- a/regression/strings/StringBuilderAppend02/test.desc +++ b/regression/strings/StringBuilderAppend02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen01/test.desc b/regression/strings/StringBuilderCapLen01/test.desc index 05516f08da2..4186f2534ac 100644 --- a/regression/strings/StringBuilderCapLen01/test.desc +++ b/regression/strings/StringBuilderCapLen01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderCapLen02/test.desc b/regression/strings/StringBuilderCapLen02/test.desc index 72a0bbd72c2..f9db006ed0b 100644 --- a/regression/strings/StringBuilderCapLen02/test.desc +++ b/regression/strings/StringBuilderCapLen02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen03/test.desc b/regression/strings/StringBuilderCapLen03/test.desc index 474bdc661ab..c35dfb33871 100644 --- a/regression/strings/StringBuilderCapLen03/test.desc +++ b/regression/strings/StringBuilderCapLen03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen04/test.desc b/regression/strings/StringBuilderCapLen04/test.desc index fa342b79518..78930851e45 100644 --- a/regression/strings/StringBuilderCapLen04/test.desc +++ b/regression/strings/StringBuilderCapLen04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars01/test.desc b/regression/strings/StringBuilderChars01/test.desc index 41dfe54abeb..48acfb25a5d 100644 --- a/regression/strings/StringBuilderChars01/test.desc +++ b/regression/strings/StringBuilderChars01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars01.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderChars02/test.desc b/regression/strings/StringBuilderChars02/test.desc index 50e49d474bc..d9006ab74ba 100644 --- a/regression/strings/StringBuilderChars02/test.desc +++ b/regression/strings/StringBuilderChars02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars02.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars03/test.desc b/regression/strings/StringBuilderChars03/test.desc index 23dda39df4e..d6f1cb4155c 100644 --- a/regression/strings/StringBuilderChars03/test.desc +++ b/regression/strings/StringBuilderChars03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars03.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars04/test.desc b/regression/strings/StringBuilderChars04/test.desc index a68edd89395..37009795a48 100644 --- a/regression/strings/StringBuilderChars04/test.desc +++ b/regression/strings/StringBuilderChars04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars04.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars05/test.desc b/regression/strings/StringBuilderChars05/test.desc index eeac328e02b..49aed9d48fd 100644 --- a/regression/strings/StringBuilderChars05/test.desc +++ b/regression/strings/StringBuilderChars05/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars05.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars06/test.desc b/regression/strings/StringBuilderChars06/test.desc index a3dc3712a5a..5ccf470590e 100644 --- a/regression/strings/StringBuilderChars06/test.desc +++ b/regression/strings/StringBuilderChars06/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars06.class ---string-refine --unwind 100 +--refine-strings --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderConstructors01/test.desc b/regression/strings/StringBuilderConstructors01/test.desc index 2c60f9bbbda..3e27d46c329 100644 --- a/regression/strings/StringBuilderConstructors01/test.desc +++ b/regression/strings/StringBuilderConstructors01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderConstructors02/test.desc b/regression/strings/StringBuilderConstructors02/test.desc index 5e951bc8079..f6c0cded34e 100644 --- a/regression/strings/StringBuilderConstructors02/test.desc +++ b/regression/strings/StringBuilderConstructors02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderInsertDelete01/test.desc b/regression/strings/StringBuilderInsertDelete01/test.desc index 4c3000d6a97..b2f927ad3b7 100644 --- a/regression/strings/StringBuilderInsertDelete01/test.desc +++ b/regression/strings/StringBuilderInsertDelete01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderInsertDelete02/test.desc b/regression/strings/StringBuilderInsertDelete02/test.desc index ae4d0ca5b81..1e67f7eb3c0 100644 --- a/regression/strings/StringBuilderInsertDelete02/test.desc +++ b/regression/strings/StringBuilderInsertDelete02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderInsertDelete03/test.desc b/regression/strings/StringBuilderInsertDelete03/test.desc index 3dfa92f0338..084038f4465 100644 --- a/regression/strings/StringBuilderInsertDelete03/test.desc +++ b/regression/strings/StringBuilderInsertDelete03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare01/test.desc b/regression/strings/StringCompare01/test.desc index 52b1d6d084c..007a6f798a7 100644 --- a/regression/strings/StringCompare01/test.desc +++ b/regression/strings/StringCompare01/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringCompare02/test.desc b/regression/strings/StringCompare02/test.desc index eb52d1f1a58..971e6a98c81 100644 --- a/regression/strings/StringCompare02/test.desc +++ b/regression/strings/StringCompare02/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare03/test.desc b/regression/strings/StringCompare03/test.desc index bd0f3177acf..acc89c80c4a 100644 --- a/regression/strings/StringCompare03/test.desc +++ b/regression/strings/StringCompare03/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare04/test.desc b/regression/strings/StringCompare04/test.desc index 88ecddbfcf6..3ea3cbd7592 100644 --- a/regression/strings/StringCompare04/test.desc +++ b/regression/strings/StringCompare04/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare05/test.desc b/regression/strings/StringCompare05/test.desc index 1358a05a36b..ef6aac2b72e 100644 --- a/regression/strings/StringCompare05/test.desc +++ b/regression/strings/StringCompare05/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare05.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation01/test.desc b/regression/strings/StringConcatenation01/test.desc index a229b504571..6465f209faa 100644 --- a/regression/strings/StringConcatenation01/test.desc +++ b/regression/strings/StringConcatenation01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringConcatenation01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringConcatenation02/test.desc b/regression/strings/StringConcatenation02/test.desc index 0e1faf53d5e..e6ea2349af8 100644 --- a/regression/strings/StringConcatenation02/test.desc +++ b/regression/strings/StringConcatenation02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringConcatenation02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation03/test.desc b/regression/strings/StringConcatenation03/test.desc index 3c01a4ee0a9..ecb497de375 100644 --- a/regression/strings/StringConcatenation03/test.desc +++ b/regression/strings/StringConcatenation03/test.desc @@ -1,6 +1,6 @@ FUTURE StringConcatenation03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation04/test.desc b/regression/strings/StringConcatenation04/test.desc index 3dbecf065ba..1425e609a3a 100644 --- a/regression/strings/StringConcatenation04/test.desc +++ b/regression/strings/StringConcatenation04/test.desc @@ -1,6 +1,6 @@ FUTURE StringConcatenation04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors01/test.desc b/regression/strings/StringConstructors01/test.desc index ed57bdfdde5..b1465868c19 100644 --- a/regression/strings/StringConstructors01/test.desc +++ b/regression/strings/StringConstructors01/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringConstructors02/test.desc b/regression/strings/StringConstructors02/test.desc index e3904d1d557..37838aafbc9 100644 --- a/regression/strings/StringConstructors02/test.desc +++ b/regression/strings/StringConstructors02/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors03/test.desc b/regression/strings/StringConstructors03/test.desc index 0caf75f41ea..10193fc66c2 100644 --- a/regression/strings/StringConstructors03/test.desc +++ b/regression/strings/StringConstructors03/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors04/test.desc b/regression/strings/StringConstructors04/test.desc index 75364dcde22..2e6e88fa862 100644 --- a/regression/strings/StringConstructors04/test.desc +++ b/regression/strings/StringConstructors04/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors05/test.desc b/regression/strings/StringConstructors05/test.desc index e74dfc73f6c..a3c6a6c0437 100644 --- a/regression/strings/StringConstructors05/test.desc +++ b/regression/strings/StringConstructors05/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors05.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringIndexMethods01/test.desc b/regression/strings/StringIndexMethods01/test.desc index 005d4459f12..dc4c6f14324 100644 --- a/regression/strings/StringIndexMethods01/test.desc +++ b/regression/strings/StringIndexMethods01/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringIndexMethods02/test.desc b/regression/strings/StringIndexMethods02/test.desc index 28df14f0145..1114e980758 100644 --- a/regression/strings/StringIndexMethods02/test.desc +++ b/regression/strings/StringIndexMethods02/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringIndexMethods03/test.desc b/regression/strings/StringIndexMethods03/test.desc index 02f9934726b..69d7e5d5745 100644 --- a/regression/strings/StringIndexMethods03/test.desc +++ b/regression/strings/StringIndexMethods03/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringIndexMethods04/test.desc b/regression/strings/StringIndexMethods04/test.desc index cb94fecb6a6..0707dbe9105 100644 --- a/regression/strings/StringIndexMethods04/test.desc +++ b/regression/strings/StringIndexMethods04/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringIndexMethods05/test.desc b/regression/strings/StringIndexMethods05/test.desc index cb43b009246..bfe98a03e7c 100644 --- a/regression/strings/StringIndexMethods05/test.desc +++ b/regression/strings/StringIndexMethods05/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods05.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringMiscellaneous01/test.desc b/regression/strings/StringMiscellaneous01/test.desc index 050c3e99e90..624c8028cb3 100644 --- a/regression/strings/StringMiscellaneous01/test.desc +++ b/regression/strings/StringMiscellaneous01/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous01.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringMiscellaneous02/test.desc b/regression/strings/StringMiscellaneous02/test.desc index 8f1a1d9475f..3fde950e418 100644 --- a/regression/strings/StringMiscellaneous02/test.desc +++ b/regression/strings/StringMiscellaneous02/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous02.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringMiscellaneous03/test.desc b/regression/strings/StringMiscellaneous03/test.desc index 341867d536f..2a1a3f02739 100644 --- a/regression/strings/StringMiscellaneous03/test.desc +++ b/regression/strings/StringMiscellaneous03/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous03.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringMiscellaneous04/test.desc b/regression/strings/StringMiscellaneous04/test.desc index 737ab3b0f8c..4c2c0491e5f 100644 --- a/regression/strings/StringMiscellaneous04/test.desc +++ b/regression/strings/StringMiscellaneous04/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous04.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringStartEnd01/test.desc b/regression/strings/StringStartEnd01/test.desc index a5463d5b5ea..eba4f6eb2b0 100644 --- a/regression/strings/StringStartEnd01/test.desc +++ b/regression/strings/StringStartEnd01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringStartEnd01.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringStartEnd02/test.desc b/regression/strings/StringStartEnd02/test.desc index 8e623622f72..ff91ad0ce4d 100644 --- a/regression/strings/StringStartEnd02/test.desc +++ b/regression/strings/StringStartEnd02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringStartEnd02.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringStartEnd03/test.desc b/regression/strings/StringStartEnd03/test.desc index 2903ec98e3e..6b1695384ca 100644 --- a/regression/strings/StringStartEnd03/test.desc +++ b/regression/strings/StringStartEnd03/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringStartEnd03.class ---string-refine --unwind 15 +--refine-strings --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf01/test.desc b/regression/strings/StringValueOf01/test.desc index 341f5e98975..c6098401ba0 100644 --- a/regression/strings/StringValueOf01/test.desc +++ b/regression/strings/StringValueOf01/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringValueOf02/test.desc b/regression/strings/StringValueOf02/test.desc index a10b398bf41..aa3fb97ba7c 100644 --- a/regression/strings/StringValueOf02/test.desc +++ b/regression/strings/StringValueOf02/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf03/test.desc b/regression/strings/StringValueOf03/test.desc index 4ed709a2404..4c7357c2278 100644 --- a/regression/strings/StringValueOf03/test.desc +++ b/regression/strings/StringValueOf03/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf04/test.desc b/regression/strings/StringValueOf04/test.desc index 0d8442e9de1..5cd66829b02 100644 --- a/regression/strings/StringValueOf04/test.desc +++ b/regression/strings/StringValueOf04/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringValueOf04.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf05/test.desc b/regression/strings/StringValueOf05/test.desc index f77cdef0b8e..3f5b25f9ce3 100644 --- a/regression/strings/StringValueOf05/test.desc +++ b/regression/strings/StringValueOf05/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringValueOf05.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf06/test.desc b/regression/strings/StringValueOf06/test.desc index 56551c4a14b..bf1c4048390 100644 --- a/regression/strings/StringValueOf06/test.desc +++ b/regression/strings/StringValueOf06/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringValueOf06.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf07/test.desc b/regression/strings/StringValueOf07/test.desc index 6dde9de229d..7ba53c21fb6 100644 --- a/regression/strings/StringValueOf07/test.desc +++ b/regression/strings/StringValueOf07/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringValueOf07.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf08/test.desc b/regression/strings/StringValueOf08/test.desc index 21d64075aaf..474c02ef13f 100644 --- a/regression/strings/StringValueOf08/test.desc +++ b/regression/strings/StringValueOf08/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf08.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf09/test.desc b/regression/strings/StringValueOf09/test.desc index 4ff97a7caef..a63f7bc3e0c 100644 --- a/regression/strings/StringValueOf09/test.desc +++ b/regression/strings/StringValueOf09/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf09.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringValueOf10/test.desc b/regression/strings/StringValueOf10/test.desc index 10e7f184189..3f8c5d6d60f 100644 --- a/regression/strings/StringValueOf10/test.desc +++ b/regression/strings/StringValueOf10/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf10.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/SubString01/test.desc b/regression/strings/SubString01/test.desc index 8eea70cf458..975e4d2e0a7 100644 --- a/regression/strings/SubString01/test.desc +++ b/regression/strings/SubString01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG SubString01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/SubString02/test.desc b/regression/strings/SubString02/test.desc index 063ce88f0f2..bdafa21bc63 100644 --- a/regression/strings/SubString02/test.desc +++ b/regression/strings/SubString02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG SubString02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/SubString03/test.desc b/regression/strings/SubString03/test.desc index f985329ce2d..961f1a92ce8 100644 --- a/regression/strings/SubString03/test.desc +++ b/regression/strings/SubString03/test.desc @@ -1,6 +1,6 @@ KNOWNBUG SubString03.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/TokenTest01/test.desc b/regression/strings/TokenTest01/test.desc index 02a11e8e392..122e6a8830a 100644 --- a/regression/strings/TokenTest01/test.desc +++ b/regression/strings/TokenTest01/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest01.class ---string-refine --unwind 30 +--refine-strings --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/TokenTest02/test.desc b/regression/strings/TokenTest02/test.desc index 48e6b0c1ab6..6d1dabed602 100644 --- a/regression/strings/TokenTest02/test.desc +++ b/regression/strings/TokenTest02/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest02.class ---string-refine --unwind 15 +--refine-strings --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/Validate01/test.desc b/regression/strings/Validate01/test.desc index e797b2735aa..649136a2956 100644 --- a/regression/strings/Validate01/test.desc +++ b/regression/strings/Validate01/test.desc @@ -1,6 +1,6 @@ FUTURE Validate01.class ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/Validate02/test.desc b/regression/strings/Validate02/test.desc index a5a3a6f1d20..22251c38a95 100644 --- a/regression/strings/Validate02/test.desc +++ b/regression/strings/Validate02/test.desc @@ -1,6 +1,6 @@ FUTURE Validate02.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/bug-test-gen-095/test.class b/regression/strings/bug-test-gen-095/test.class new file mode 100644 index 00000000000..3895d218c3d Binary files /dev/null and b/regression/strings/bug-test-gen-095/test.class differ diff --git a/regression/strings/bug-test-gen-095/test.desc b/regression/strings/bug-test-gen-095/test.desc new file mode 100644 index 00000000000..a40f9e43402 --- /dev/null +++ b/regression/strings/bug-test-gen-095/test.desc @@ -0,0 +1,7 @@ +KNOWNBUG +test.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings/bug-test-gen-095/test.java b/regression/strings/bug-test-gen-095/test.java new file mode 100644 index 00000000000..a6910527551 --- /dev/null +++ b/regression/strings/bug-test-gen-095/test.java @@ -0,0 +1,10 @@ +public class test +{ + public static void main(String[] args) + { + StringBuilder sb = new StringBuilder(args[0]); + sb.append("Z"); + String s = sb.toString(); + assert(s.equals("fg")); + } +} diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h index 1ec17bca535..86af21533f8 100644 --- a/regression/strings/cprover-string-hack.h +++ b/regression/strings/cprover-string-hack.h @@ -1,18 +1,32 @@ -typedef struct __CPROVER_string { char *s; } __CPROVER_string; -//typedef struct __CPROVER_char { char c; } __CPROVER_char; -typedef unsigned char __CPROVER_char; +/*******************************************************************\ + +Module: Hack for C string tests + +Author: Romain Brenguier + +\*******************************************************************/ + +#ifndef CPROVER_ESSION_STRINGS_CPROVER_STRING_HACK_H +#define CPROVER_ESSION_STRINGS_CPROVER_STRING_HACK_H + +typedef struct __attribute__((__packed__)) __CPROVER_refined_string_type // NOLINT + { int length; char content[]; } __CPROVER_refined_string_type; +typedef __CPROVER_refined_string_type __CPROVER_string; //NOLINT /****************************************************************************** * CPROVER string functions ******************************************************************************/ /* returns s[p] */ -#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p) +#define __CPROVER_char_at(s, p) \ + __CPROVER_uninterpreted_string_char_at_func(s, p) /* string equality */ -#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2) +#define __CPROVER_string_equal(s1, s2) \ + __CPROVER_uninterpreted_string_equal_func(s1, s2) /* defines a string literal, e.g. __CPROVER_string_literal("foo") */ -#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s) +#define __CPROVER_string_literal(s) \ + __CPROVER_uninterpreted_string_literal_func(s) /* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you * *must* use a C string literal as argument (i.e. double quotes "c", not @@ -20,30 +34,39 @@ typedef unsigned char __CPROVER_char; #define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c) /* produces the concatenation of s1 and s2 */ -#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2) +#define __CPROVER_string_concat(s1, s2) \ + __CPROVER_uninterpreted_string_concat_func(s1, s2) /* return the length of s */ -#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s) +#define __CPROVER_string_length(s) \ + __CPROVER_uninterpreted_string_length_func(s) /* extracts the substring between positions i and j (j not included) */ -#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j) +#define __CPROVER_string_substring(s, i, j) \ + __CPROVER_uninterpreted_string_substring_func(s, i, j) /* test whether p is a prefix of s */ -#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s) +#define __CPROVER_string_isprefix(p, s) \ + __CPROVER_uninterpreted_string_is_prefix_func(p, s) /* test whether p is a suffix of s */ -#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s) +#define __CPROVER_string_issuffix(p, s) \ + __CPROVER_uninterpreted_string_is_suffix_func(p, s) /* test whether p contains s */ -#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s) +#define __CPROVER_string_contains(p, s) \ + __CPROVER_uninterpreted_string_contains_func(p, s) /* first index where character c appears, -1 if not found */ -#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c) +#define __CPROVER_string_index_of(s, c) \ + __CPROVER_uninterpreted_string_index_of_func(s, c) /* last index where character c appears */ -#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c) +#define __CPROVER_string_last_index_of(s, c) \ + __CPROVER_uninterpreted_string_last_index_of_func(s, c) /* returns a new string obtained from s by setting s[p] = c */ -#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c) +#define __CPROVER_char_set(s, p, c) \ + __CPROVER_uninterpreted_string_char_set_func(s, p, c) #define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s) @@ -54,19 +77,32 @@ typedef unsigned char __CPROVER_char; /****************************************************************************** * don't use these directly ******************************************************************************/ -extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos); -extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2); +extern char __CPROVER_uninterpreted_string_char_at_func( + __CPROVER_string str, int pos); +extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func( + __CPROVER_string str1, __CPROVER_string str2); extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(char * str); -extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func(); -extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2); +extern char __CPROVER_uninterpreted_char_literal_func(); +extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func( + __CPROVER_string str1, __CPROVER_string str2); extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str); -extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j); -extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str); -extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str); -extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2); -extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c); -extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c); -extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c); -extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str); +extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func( + __CPROVER_string str, int i, int j); +extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func( + __CPROVER_string pref, __CPROVER_string str); +extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func( + __CPROVER_string suff, __CPROVER_string str); +extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func( + __CPROVER_string str1, __CPROVER_string str2); +extern int __CPROVER_uninterpreted_string_index_of_func( + __CPROVER_string str, char c); +extern int __CPROVER_uninterpreted_string_last_index_of_func( + __CPROVER_string str, char c); +extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func( + __CPROVER_string str, int pos, char c); +extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func( + __CPROVER_string str); extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str); extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i); + +#endif diff --git a/regression/strings/java_append_char/test.desc b/regression/strings/java_append_char/test.desc new file mode 100644 index 00000000000..f38fb748736 --- /dev/null +++ b/regression/strings/java_append_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_char.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 15.* FAILURE$ +-- diff --git a/regression/strings/java_append_char/test_append_char.class b/regression/strings/java_append_char/test_append_char.class new file mode 100644 index 00000000000..c0b1491423b Binary files /dev/null and b/regression/strings/java_append_char/test_append_char.class differ diff --git a/regression/strings/java_append_char/test_append_char.java b/regression/strings/java_append_char/test_append_char.java new file mode 100644 index 00000000000..90e9ab089a2 --- /dev/null +++ b/regression/strings/java_append_char/test_append_char.java @@ -0,0 +1,17 @@ +public class test_append_char +{ + public static void main(/*String[] args*/) + { + char[] diff = {'d', 'i', 'f', 'f'}; + char[] blue = {'b', 'l', 'u', 'e'}; + + StringBuilder buffer = new StringBuilder(); + + buffer.append(diff) + .append(blue); + + String tmp=buffer.toString(); + System.out.println(tmp); + assert(!tmp.equals("diffblue")); + } +} diff --git a/regression/strings/java_append_int/test.desc b/regression/strings/java_append_int/test.desc new file mode 100644 index 00000000000..d65eecf13f5 --- /dev/null +++ b/regression/strings/java_append_int/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_int.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 9.* FAILURE$ +-- diff --git a/regression/strings/java_append_int/test_append_int.class b/regression/strings/java_append_int/test_append_int.class new file mode 100644 index 00000000000..d9ee5046e7d Binary files /dev/null and b/regression/strings/java_append_int/test_append_int.class differ diff --git a/regression/strings/java_append_int/test_append_int.java b/regression/strings/java_append_int/test_append_int.java new file mode 100644 index 00000000000..cf550211ad7 --- /dev/null +++ b/regression/strings/java_append_int/test_append_int.java @@ -0,0 +1,11 @@ +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/java_append_object/test.desc b/regression/strings/java_append_object/test.desc new file mode 100644 index 00000000000..f15910bca93 --- /dev/null +++ b/regression/strings/java_append_object/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_object.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 15.* FAILURE$ +-- diff --git a/regression/strings/java_append_object/test_append_object.class b/regression/strings/java_append_object/test_append_object.class new file mode 100644 index 00000000000..fbfec51a3f5 Binary files /dev/null and b/regression/strings/java_append_object/test_append_object.class differ diff --git a/regression/strings/java_append_object/test_append_object.java b/regression/strings/java_append_object/test_append_object.java new file mode 100644 index 00000000000..e139a01679a --- /dev/null +++ b/regression/strings/java_append_object/test_append_object.java @@ -0,0 +1,17 @@ +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")); + } +} diff --git a/regression/strings/java_append_string/test.desc b/regression/strings/java_append_string/test.desc new file mode 100644 index 00000000000..7b6ea8ccae7 --- /dev/null +++ b/regression/strings/java_append_string/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_append_string.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 12.* FAILURE$ +-- diff --git a/regression/strings/java_append_string/test_append_string.class b/regression/strings/java_append_string/test_append_string.class new file mode 100644 index 00000000000..f2cb5cf8bea Binary files /dev/null and b/regression/strings/java_append_string/test_append_string.class differ diff --git a/regression/strings/java_append_string/test_append_string.java b/regression/strings/java_append_string/test_append_string.java new file mode 100644 index 00000000000..54665da29cc --- /dev/null +++ b/regression/strings/java_append_string/test_append_string.java @@ -0,0 +1,14 @@ +public class test_append_string +{ + public static void main(/*String[] args*/) + { + String di = new String("di"); + StringBuilder diff = new StringBuilder(); + diff.append(di); + diff.append("ff"); + System.out.println(diff); + String s = diff.toString(); + System.out.println(s); + assert (!s.equals("diff")); + } +} diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc index 9f48288c694..47db60a36d9 100644 --- a/regression/strings/java_case/test.desc +++ b/regression/strings/java_case/test.desc @@ -1,10 +1,7 @@ FUTURE test_case.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$ -^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$ -^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$ -^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$ +^\[.*assertion.1\].* line 8.* FAILURE$ -- diff --git a/regression/strings/java_case/test_case.class b/regression/strings/java_case/test_case.class index 8579881de17..5887b496986 100644 Binary files a/regression/strings/java_case/test_case.class and b/regression/strings/java_case/test_case.class differ diff --git a/regression/strings/java_case/test_case.java b/regression/strings/java_case/test_case.java index ce3a51814c8..309abfc07b9 100644 --- a/regression/strings/java_case/test_case.java +++ b/regression/strings/java_case/test_case.java @@ -1,16 +1,12 @@ -public class test_case { - - public static void main(String[] argv) { - - String s = new String("AbcCdE"); - String l = s.toLowerCase(); - System.out.println(l); - - String u = s.toUpperCase(); - System.out.println(u); - assert(l.equals("abccde")); - assert(u.equals("ABCCDE")); - assert(s.equalsIgnoreCase("ABccDe")); - assert(!l.equals("abccde") || !u.equals("ABCCDE")); - } +public class test_case +{ + public static void main(/*String[] argv*/) + { + String s = new String("Ab"); + String l = s.toLowerCase(); + String u = s.toUpperCase(); + assert(!l.equals("ab") || + !u.equals("AB") || + !s.equalsIgnoreCase("aB")); + } } diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc index 8282b808b84..62cc45997ba 100644 --- a/regression/strings/java_char_array/test.desc +++ b/regression/strings/java_char_array/test.desc @@ -1,9 +1,7 @@ FUTURE test_char_array.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$ -^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$ -^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$ +^\[.*assertion.1\].* line 9.* FAILURE$ -- diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/strings/java_char_array/test_char_array.class index 836942da134..38a7ecf41ed 100644 Binary files a/regression/strings/java_char_array/test_char_array.class and b/regression/strings/java_char_array/test_char_array.class differ diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/strings/java_char_array/test_char_array.java index 3cfd4000d3a..96e250fb030 100644 --- a/regression/strings/java_char_array/test_char_array.java +++ b/regression/strings/java_char_array/test_char_array.java @@ -1,15 +1,13 @@ -public class test_char_array { - - public static void main(String[] argv) - { - String s = "abc"; - char [] str = s.toCharArray(); - int[] test = new int[312]; - char c = str[2]; - String t = argv[0]; - char d = t.charAt(0); - assert(str.length == 3); - assert(c == 'c'); - assert(c == d || d < 'a' || d > 'z' ); - } +public class test_char_array +{ + public static void main(/*String[] argv*/) + { + String s = "abc"; + char [] str = s.toCharArray(); + char c = str[2]; + char a = s.charAt(0); + assert(str.length != 3 || + a != 'a' || + c != 'c'); + } } diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc index fe5ffae7238..24437881467 100644 --- a/regression/strings/java_char_array_init/test.desc +++ b/regression/strings/java_char_array_init/test.desc @@ -1,11 +1,7 @@ FUTURE test_init.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$ -^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$ -^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$ -^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$ -^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$ +^\[.*assertion.1\].* line 14.* FAILURE$ -- diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/strings/java_char_array_init/test_init.class index be3baee56bd..ff9c64510da 100644 Binary files a/regression/strings/java_char_array_init/test_init.class and b/regression/strings/java_char_array_init/test_init.class differ diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/strings/java_char_array_init/test_init.java index 5f4e220844c..b27030b1306 100644 --- a/regression/strings/java_char_array_init/test_init.java +++ b/regression/strings/java_char_array_init/test_init.java @@ -1,23 +1,18 @@ public class test_init { - public static void main(String[] argv) - { - char [] str = new char[10]; - str[0] = 'H'; - str[1] = 'e'; - str[2] = 'l'; - str[3] = 'l'; - str[4] = 'o'; - String s = new String(str); - String t = new String(str,1,2); + public static void main(/*String[] argv*/) + { + char [] str = new char[10]; + str[0] = 'H'; + str[1] = 'e'; + str[2] = 'l'; + str[3] = 'l'; + str[4] = 'o'; + String s = new String(str); + String t = new String(str,1,2); - System.out.println(s); - System.out.println(s.length()); - assert(s.startsWith("Hello")); - assert(s.length() == 10); - assert(t.equals("el")); - String u = String.valueOf(str,3,2); - assert(u.equals("lo")); - assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo")); - } + assert(s.length() != 10 || + !t.equals("el") || + !s.startsWith("Hello")); + } } diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc index 6f206a0f22f..0226b19529e 100644 --- a/regression/strings/java_char_at/test.desc +++ b/regression/strings/java_char_at/test.desc @@ -1,9 +1,7 @@ FUTURE test_char_at.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$ -^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$ -^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$ +^\[.*assertion.1\].* line 5.* FAILURE$ -- diff --git a/regression/strings/java_char_at/test_char_at.class b/regression/strings/java_char_at/test_char_at.class index 7d1f07fad7d..dc9ed32f19f 100644 Binary files a/regression/strings/java_char_at/test_char_at.class and b/regression/strings/java_char_at/test_char_at.class differ diff --git a/regression/strings/java_char_at/test_char_at.java b/regression/strings/java_char_at/test_char_at.java index 337c6524099..9ae02733fb8 100644 --- a/regression/strings/java_char_at/test_char_at.java +++ b/regression/strings/java_char_at/test_char_at.java @@ -1,17 +1,7 @@ public class test_char_at { - public static void main(String[] argv) { - String s = new String("Hello World!"); - char c = s.charAt(4); - StringBuilder sb = new StringBuilder(s); - sb.setCharAt(5,'-'); - s = sb.toString(); - - if(argv.length==1) - assert(c == 'o'); - else if(argv.length==2) - assert(c == 'p'); - else - assert(s.equals("Hello-World!")); - } + public static void main(/*String[] argv*/) { + String s = new String("abc"); + assert(s.charAt(2)!='c'); + } } diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc index 35ca0cd6f4b..2b94f1fa0c0 100644 --- a/regression/strings/java_code_point/test.desc +++ b/regression/strings/java_code_point/test.desc @@ -1,11 +1,7 @@ FUTURE test_code_point.class ---string-refine -^EXIT=0$ +--refine-strings +^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$ -^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$ -^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$ -^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$ -^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$ +^\[.*assertion.1\].* line 8.* FAILURE$ -- diff --git a/regression/strings/java_code_point/test_code_point.class b/regression/strings/java_code_point/test_code_point.class index c257f0633ec..f2f5fbad63a 100644 Binary files a/regression/strings/java_code_point/test_code_point.class and b/regression/strings/java_code_point/test_code_point.class differ diff --git a/regression/strings/java_code_point/test_code_point.java b/regression/strings/java_code_point/test_code_point.java index c27a56f575c..345dc1fa08b 100644 --- a/regression/strings/java_code_point/test_code_point.java +++ b/regression/strings/java_code_point/test_code_point.java @@ -1,13 +1,14 @@ -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); - StringBuilder sb = new StringBuilder(); - sb.appendCodePoint(0x10907); - assert(s.charAt(1) == sb.charAt(0)); - } +public class test_code_point +{ + public static void main(/*String[] argv*/) + { + String s = "!𐤇𐤄𐤋𐤋𐤅"; + StringBuilder sb = new StringBuilder(); + sb.appendCodePoint(0x10907); + assert(s.codePointAt(1) != 67847 || + s.codePointBefore(3) != 67847 || + s.codePointCount(1,5) < 2 || + s.offsetByCodePoints(1,2) < 3 || + s.charAt(1) != sb.charAt(0)); + } } diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc index 517b208c3e4..e7444831e77 100644 --- a/regression/strings/java_compare/test.desc +++ b/regression/strings/java_compare/test.desc @@ -1,10 +1,7 @@ FUTURE test_compare.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$ -^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$ -^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$ -^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$ +^\[.*assertion.1\].* line 7.* FAILURE$ -- diff --git a/regression/strings/java_compare/test_compare.class b/regression/strings/java_compare/test_compare.class index 5616013c523..67f18914ea6 100644 Binary files a/regression/strings/java_compare/test_compare.class and b/regression/strings/java_compare/test_compare.class differ diff --git a/regression/strings/java_compare/test_compare.java b/regression/strings/java_compare/test_compare.java index 8c1d4b71a0c..0a535fd0bf3 100644 --- a/regression/strings/java_compare/test_compare.java +++ b/regression/strings/java_compare/test_compare.java @@ -1,18 +1,9 @@ -public class test_compare { - - public static void main(String[] argv) { - String s1 = "abc"; - String s2 = "aac"; - assert(s1.compareTo(s2) == 1); - - assert(s2.compareTo(argv[0]) != -1); - - String s3 = "abc"; - assert(s3.hashCode() == s1.hashCode()); - assert(s3.hashCode() == s2.hashCode()); - - /*String x = s1.intern(); - String y = s3.intern(); - assert(x == y);*/ - } +public class test_compare +{ + public static void main(/*String[] argv*/) + { + String s1 = "ab"; + String s2 = "aa"; + assert(s1.compareTo(s2) != 1); + } } diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc index 8ef2898e0d7..fb784efd723 100644 --- a/regression/strings/java_concat/test.desc +++ b/regression/strings/java_concat/test.desc @@ -1,8 +1,8 @@ FUTURE test_concat.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$ -^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$ +^\[.*assertion.1\].* line 10.* SUCCESS$ +^\[.*assertion.2\].* line 11.* FAILURE$ -- diff --git a/regression/strings/java_concat/test_concat.class b/regression/strings/java_concat/test_concat.class index a6d4008aa26..a69c05921f6 100644 Binary files a/regression/strings/java_concat/test_concat.class and b/regression/strings/java_concat/test_concat.class differ diff --git a/regression/strings/java_concat/test_concat.java b/regression/strings/java_concat/test_concat.java index d714ea89538..6bbe753b2e4 100644 --- a/regression/strings/java_concat/test_concat.java +++ b/regression/strings/java_concat/test_concat.java @@ -1,12 +1,13 @@ -public class test_concat { - - public static void main(String[] argv) { - String s = new String("pi"); - int i = s.length(); - String t = new String("ppo"); - String u = s.concat(t); - char c = u.charAt(i); - assert(c == 'p'); - assert(c == 'o'); - } +public class test_concat +{ + public static void main(/*String[] argv*/) + { + String s = new String("pi"); + int i = s.length(); + String t = new String("ppo"); + String u = s.concat(t); + char c = u.charAt(i); + assert(c == 'p'); + assert(c != 'p'); + } } diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc index 4e7a3bd4f7d..bb4fadba9d3 100644 --- a/regression/strings/java_contains/test.desc +++ b/regression/strings/java_contains/test.desc @@ -1,8 +1,7 @@ FUTURE test_contains.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$ -^\[assertion.2\] assertion at file test_contains.java line 8: FAILURE$ +^\[.*assertion.1\].* line 7.* FAILURE$ -- diff --git a/regression/strings/java_contains/test_contains.class b/regression/strings/java_contains/test_contains.class index 855ab828393..9bbccb03775 100644 Binary files a/regression/strings/java_contains/test_contains.class and b/regression/strings/java_contains/test_contains.class differ diff --git a/regression/strings/java_contains/test_contains.java b/regression/strings/java_contains/test_contains.java index fce2ee63047..6f4c60a1a2e 100644 --- a/regression/strings/java_contains/test_contains.java +++ b/regression/strings/java_contains/test_contains.java @@ -1,10 +1,9 @@ -public class test_contains { - - public static void main(String[] argv) { - String s = new String("Hello World!"); - String u = "o W"; - String t = "W o"; - assert(s.contains(u)); - assert(s.contains(t)); - } +public class test_contains +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abc"); + String u = "bc"; + assert(!s.contains(u)); + } } diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc index c6c608c0955..ff41e78b3df 100644 --- a/regression/strings/java_delete/test.desc +++ b/regression/strings/java_delete/test.desc @@ -1,8 +1,7 @@ FUTURE test_delete.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$ -^\[assertion.2\] assertion at file test_delete.java line 12: FAILURE$ +^\[.*assertion.1\].* line 8.* FAILURE$ -- diff --git a/regression/strings/java_delete/test_delete.class b/regression/strings/java_delete/test_delete.class index 6d30024f108..7036ce13c90 100644 Binary files a/regression/strings/java_delete/test_delete.class and b/regression/strings/java_delete/test_delete.class differ diff --git a/regression/strings/java_delete/test_delete.java b/regression/strings/java_delete/test_delete.java index c91b16c5b89..ea846cd215a 100644 --- a/regression/strings/java_delete/test_delete.java +++ b/regression/strings/java_delete/test_delete.java @@ -1,15 +1,10 @@ -public class test_delete { - - public static void main(String[] argv) { - StringBuilder s = new StringBuilder(); - s.append("Hello World!"); - s.delete(4,6); - s.deleteCharAt(1); - - String str = s.toString(); - System.out.println(str); - assert(str.equals("HllWorld!")); - assert(!str.equals("HllWorld!")); - - } +public class test_delete +{ + public static void main(/*String[] argv*/) + { + StringBuilder s = new StringBuilder("Abc"); + s.delete(1,2); + String str = s.toString(); + assert(!str.equals("Ac")); + } } diff --git a/regression/strings/java_delete_char_at/test.desc b/regression/strings/java_delete_char_at/test.desc new file mode 100644 index 00000000000..0314c606e56 --- /dev/null +++ b/regression/strings/java_delete_char_at/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_delete_char_at.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 9.* FAILURE$ +-- diff --git a/regression/strings/java_delete_char_at/test_delete_char_at.class b/regression/strings/java_delete_char_at/test_delete_char_at.class new file mode 100644 index 00000000000..ed3148e2f7e Binary files /dev/null and b/regression/strings/java_delete_char_at/test_delete_char_at.class differ diff --git a/regression/strings/java_delete_char_at/test_delete_char_at.java b/regression/strings/java_delete_char_at/test_delete_char_at.java new file mode 100644 index 00000000000..5f2c995b56b --- /dev/null +++ b/regression/strings/java_delete_char_at/test_delete_char_at.java @@ -0,0 +1,11 @@ +public class test_delete_char_at +{ + public static void main(/*String[] argv*/) + { + StringBuilder s = new StringBuilder(); + s.append("Abc"); + s.deleteCharAt(1); + String str = s.toString(); + assert(!str.equals("Ac")); + } +} diff --git a/regression/strings/java_easychair/easychair.class b/regression/strings/java_easychair/easychair.class index e47900cc0b2..e6c5f66c42d 100644 Binary files a/regression/strings/java_easychair/easychair.class and b/regression/strings/java_easychair/easychair.class differ diff --git a/regression/strings/java_easychair/easychair.java b/regression/strings/java_easychair/easychair.java index 55ca2a31bb3..caed962fb46 100644 --- a/regression/strings/java_easychair/easychair.java +++ b/regression/strings/java_easychair/easychair.java @@ -1,34 +1,34 @@ -public class easychair { +public class easychair +{ + public static void main(String[] argv) + { + if(argv.length > 1) + { + String str = new String(argv[1]); + if(str.length() < 40) + { + // containing "/" and containing "EasyChair" + int lastSlash = str.lastIndexOf('/'); + if(lastSlash < 0) return ; - public static void main(String[] argv) { - if(argv.length > 1){ - String str = new String(argv[1]); - if(str.length() < 40){ - - // containing "/" and containing "EasyChair" - int lastSlash = str.lastIndexOf('/'); - if(lastSlash < 0) return ; - - String rest = str.substring(lastSlash + 1); - // warning: removed this because contains is not efficient at the moment - if(! rest.contains("EasyChair")) return ; - // (2) Check that str starts with "http://" - if(! str.startsWith("http://")) return ; - // (3) Take the string between "http://" and the last "/". - // if it starts with "www." strip the "www." off - String t = str.substring("http://".length(),lastSlash - "http://".length()); - if(t.startsWith("www.")) - t = t.substring("www.".length()); - - // - //(4) Check that after stripping we have either "live.com" - // or "google.com" - if(!t.equals("live.com") && !t.equals("google.com")) - return ; - // s survived all checks - assert(false); //return true; - } - } - } + String rest = str.substring(lastSlash + 1); + // warning: removed this because contains is not efficient at the moment + if(! rest.contains("EasyChair")) return ; + // (2) Check that str starts with "http://" + if(! str.startsWith("http://")) return ; + // (3) Take the string between "http://" and the last "/". + // if it starts with "www." strip the "www." off + String t = str.substring("http://".length(),lastSlash - "http://".length()); + if(t.startsWith("www.")) + t = t.substring("www.".length()); + //(4) Check that after stripping we have either "live.com" + // or "google.com" + if(!t.equals("live.com") && !t.equals("google.com")) + return ; + // s survived all checks + assert(false); //return true; + } + } + } } diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc index 8680af72c5a..14418a7798e 100644 --- a/regression/strings/java_easychair/test.desc +++ b/regression/strings/java_easychair/test.desc @@ -1,7 +1,7 @@ -FUTURE +THOROUGH easychair.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$ +^\[.*assertion.1\].* line 30.* FAILURE$ -- diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc index cab514b80b5..44e8e1346a9 100644 --- a/regression/strings/java_empty/test.desc +++ b/regression/strings/java_empty/test.desc @@ -1,8 +1,7 @@ FUTURE test_empty.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$ -^\[assertion.2\] assertion at file test_empty.java line 5: FAILURE$ +^\[.*assertion.1\].* line 6.* FAILURE$ -- diff --git a/regression/strings/java_empty/test_empty.class b/regression/strings/java_empty/test_empty.class index f0ced290ee3..147a2b628fe 100644 Binary files a/regression/strings/java_empty/test_empty.class and b/regression/strings/java_empty/test_empty.class differ diff --git a/regression/strings/java_empty/test_empty.java b/regression/strings/java_empty/test_empty.java index 2465fb16e41..18fde4a115e 100644 --- a/regression/strings/java_empty/test_empty.java +++ b/regression/strings/java_empty/test_empty.java @@ -1,7 +1,8 @@ -public class test_empty { - public static void main(String[] argv) { - String empty = " "; - assert(empty.trim().isEmpty()); - assert(empty.isEmpty()); - } +public class test_empty +{ + public static void main(/*String[] argv*/) + { + String empty = ""; + assert(!empty.isEmpty()); + } } diff --git a/regression/strings/java_endswith/test.desc b/regression/strings/java_endswith/test.desc new file mode 100644 index 00000000000..285e6ee103c --- /dev/null +++ b/regression/strings/java_endswith/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_endswith.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 7.* FAILURE$ +-- diff --git a/regression/strings/java_endswith/test_endswith.class b/regression/strings/java_endswith/test_endswith.class new file mode 100644 index 00000000000..e3d453c444f Binary files /dev/null and b/regression/strings/java_endswith/test_endswith.class differ diff --git a/regression/strings/java_endswith/test_endswith.java b/regression/strings/java_endswith/test_endswith.java new file mode 100644 index 00000000000..fabf6f8dde0 --- /dev/null +++ b/regression/strings/java_endswith/test_endswith.java @@ -0,0 +1,9 @@ +public class test_endswith +{ + public static void main(/*String[] argv*/) + { + String s = new String("Abcd"); + String suff = "cd"; + assert(!s.endsWith(suff)); + } +} diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc index d66c30b26fe..bb61dcea8ed 100644 --- a/regression/strings/java_equal/test.desc +++ b/regression/strings/java_equal/test.desc @@ -1,8 +1,7 @@ FUTURE test_equal.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$ -^\[assertion.2\] assertion at file test_equal.java line 8: SUCCESS$ +^\[.*assertion.1\].* line 8.* FAILURE$ -- diff --git a/regression/strings/java_equal/test_equal.class b/regression/strings/java_equal/test_equal.class index 26ee19e6cb1..e0fc6db8aaf 100644 Binary files a/regression/strings/java_equal/test_equal.class and b/regression/strings/java_equal/test_equal.class differ diff --git a/regression/strings/java_equal/test_equal.java b/regression/strings/java_equal/test_equal.java index 151162a106d..e8c9ac7cb1a 100644 --- a/regression/strings/java_equal/test_equal.java +++ b/regression/strings/java_equal/test_equal.java @@ -1,10 +1,9 @@ -public class test_equal { - - public static void main(String[] argv) { - String s = new String("pi"); - String t = new String("po"); - String u = "po"; - assert(s.equals(t)); - assert(t.equals(u)); - } +public class test_equal +{ + public static void main(String[] argv) + { + String s = new String("pi"); + String t = new String("po"); + assert(!s.equals(t)); + } } diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc index 955f0358eab..31404ae5e08 100644 --- a/regression/strings/java_float/test.desc +++ b/regression/strings/java_float/test.desc @@ -1,10 +1,7 @@ FUTURE test_float.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$ -^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$ -^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$ -^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$ +^\[.*assertion.1\].* line 15.* FAILURE$ -- diff --git a/regression/strings/java_float/test_float.class b/regression/strings/java_float/test_float.class index 356d0e17871..00e8622e2ac 100644 Binary files a/regression/strings/java_float/test_float.class and b/regression/strings/java_float/test_float.class differ diff --git a/regression/strings/java_float/test_float.java b/regression/strings/java_float/test_float.java index e59c631d91e..312f1aeaf10 100644 --- a/regression/strings/java_float/test_float.java +++ b/regression/strings/java_float/test_float.java @@ -1,20 +1,17 @@ -public class test_float { - - public static void main(String[] arg) { - float inf = 100.0f / 0.0f; - float minus_inf = -100.0f / 0.0f; - float nan = 0.0f / 0.0f; - String inf_string = Float.toString(inf); - String mininf_string = Float.toString(minus_inf); - String nan_string = Float.toString(nan); - //String arg1 = arg[0]; - System.out.println(nan_string); - System.out.println(inf_string); - System.out.println(mininf_string); - assert(nan_string.equals("NaN")); - assert(inf_string.equals("Infinity")); - assert(mininf_string.equals("-Infinity")); - assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity") - || !mininf_string.equals("-Infinity")); - } +public class test_float +{ + public static void main(/*String[] arg*/) + { + float inf = 100.0f / 0.0f; + float minus_inf = -100.0f / 0.0f; + float nan = 0.0f / 0.0f; + String inf_string = Float.toString(inf); + String mininf_string = Float.toString(minus_inf); + String nan_string = Float.toString(nan); + System.out.println(nan_string); + System.out.println(inf_string); + System.out.println(mininf_string); + assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity") + || !mininf_string.equals("-Infinity")); + } } diff --git a/regression/strings/java_hash_code/test.desc b/regression/strings/java_hash_code/test.desc new file mode 100644 index 00000000000..4f786d42f80 --- /dev/null +++ b/regression/strings/java_hash_code/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_hash_code.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 7.* FAILURE$ +-- diff --git a/regression/strings/java_hash_code/test_hash_code.class b/regression/strings/java_hash_code/test_hash_code.class new file mode 100644 index 00000000000..d9b3e2b2f3d Binary files /dev/null and b/regression/strings/java_hash_code/test_hash_code.class differ diff --git a/regression/strings/java_hash_code/test_hash_code.java b/regression/strings/java_hash_code/test_hash_code.java new file mode 100644 index 00000000000..fbc15f0b4c2 --- /dev/null +++ b/regression/strings/java_hash_code/test_hash_code.java @@ -0,0 +1,9 @@ +public class test_hash_code +{ + public static void main(/*String[] argv*/) + { + String s1 = "ab"; + String s2 = "ab"; + assert(s1.hashCode() != s2.hashCode()); + } +} diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc index daa6c32493b..28a0809f441 100644 --- a/regression/strings/java_index_of/test.desc +++ b/regression/strings/java_index_of/test.desc @@ -1,16 +1,7 @@ FUTURE test_index_of.class ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$ -^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$ -^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$ -^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$ -^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$ -^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$ -^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$ -^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$ -^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$ -^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$ +^\[.*assertion.1\].* line 8.* FAILURE$ -- diff --git a/regression/strings/java_index_of/test_index_of.class b/regression/strings/java_index_of/test_index_of.class index 8b3b7525f1a..cae397a79fb 100644 Binary files a/regression/strings/java_index_of/test_index_of.class and b/regression/strings/java_index_of/test_index_of.class differ diff --git a/regression/strings/java_index_of/test_index_of.java b/regression/strings/java_index_of/test_index_of.java index bbe06d279ec..b607ba79570 100644 --- a/regression/strings/java_index_of/test_index_of.java +++ b/regression/strings/java_index_of/test_index_of.java @@ -1,32 +1,10 @@ -public class test_index_of { - - public static void main(String[] argv) { - String s = "Hello World!"; - char c = 'o'; - int i = s.indexOf(c); - int j = s.lastIndexOf('o'); - int k = s.indexOf(c,5); - int l = s.lastIndexOf(c,5); - int m = s.indexOf("lo"); - int n = s.lastIndexOf("lo"); - if(argv.length == 1){ - assert(i == 4); - assert(i != 4); - } - else if(argv.length == 2){ - assert(j == 7); - assert(j != 7); - } - else if(argv.length == 3){ - assert(k == 7); - assert(k != 7); - } - else if(argv.length == 4){ - assert(l == 4); - assert(l != 4); - } else { - assert(m != 2); - assert(n != 2); - } - } +public class test_index_of +{ + public static void main(/*String[] argv*/) + { + String s = "Abc"; + String bc = "bc"; + int i = s.indexOf(bc); + assert(i != 1); + } } diff --git a/regression/strings/java_index_of_char/test.desc b/regression/strings/java_index_of_char/test.desc new file mode 100644 index 00000000000..30d179cbaaa --- /dev/null +++ b/regression/strings/java_index_of_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_index_of_char.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* FAILURE$ +-- diff --git a/regression/strings/java_index_of_char/test_index_of_char.class b/regression/strings/java_index_of_char/test_index_of_char.class new file mode 100644 index 00000000000..bf4fa6e946e Binary files /dev/null and b/regression/strings/java_index_of_char/test_index_of_char.class differ diff --git a/regression/strings/java_index_of_char/test_index_of_char.java b/regression/strings/java_index_of_char/test_index_of_char.java new file mode 100644 index 00000000000..92d75b3b07d --- /dev/null +++ b/regression/strings/java_index_of_char/test_index_of_char.java @@ -0,0 +1,10 @@ +public class test_index_of_char +{ + public static void main(/*String[] argv*/) + { + String s = "Abc"; + char c = 'c'; + int i = s.indexOf(c); + assert(i != 2); + } +} diff --git a/regression/strings/java_insert/test_insert.class b/regression/strings/java_insert/test_insert.class deleted file mode 100644 index 5fa0f425061..00000000000 Binary files a/regression/strings/java_insert/test_insert.class and /dev/null differ diff --git a/regression/strings/java_insert/test_insert.java b/regression/strings/java_insert/test_insert.java deleted file mode 100644 index 6871a51716c..00000000000 --- a/regression/strings/java_insert/test_insert.java +++ /dev/null @@ -1,19 +0,0 @@ -public class test_insert { - - public static void main(String[] argv) { - int i = 123; - long j = 123; - char c = '/'; - boolean b = true; - StringBuilder sb = new StringBuilder("hello"); - sb.insert(2,i); - sb.insert(2,c); - sb.insert(2,j); - sb.insert(2,b); - sb.insert(2,"abc"); - String s = sb.toString(); - System.out.println(s); - assert(s.equals("heabctrue123/123llo")); - assert(!s.equals("heabctrue123/123llo")); - } -} diff --git a/regression/strings/java_insert/test_insert1.class b/regression/strings/java_insert/test_insert1.class deleted file mode 100644 index 80091936cea..00000000000 Binary files a/regression/strings/java_insert/test_insert1.class and /dev/null differ diff --git a/regression/strings/java_insert/test_insert1.java b/regression/strings/java_insert/test_insert1.java deleted file mode 100644 index 54e754302c5..00000000000 --- a/regression/strings/java_insert/test_insert1.java +++ /dev/null @@ -1,23 +0,0 @@ -public class test_insert1 { - - public static void main(String[] argv) { - int i = 123; - long j = 123; - char c = '/'; - boolean b = true; - StringBuilder sb = new StringBuilder("hello"); - sb.insert(2,i); - - /* - sb.insert(2,c); - sb.insert(2,j); - sb.insert(2,b); - sb.insert(2,"abc"); - */ - String s = sb.toString(); - System.out.println(s); - assert(s.equals("he123llo")); - //assert(s.equals("heabctrue123/123llo")); - //assert(!s.equals("heabctrue123/123llo")); - } -} diff --git a/regression/strings/java_insert_char/test.desc b/regression/strings/java_insert_char/test.desc new file mode 100644 index 00000000000..f5727a3a4ab --- /dev/null +++ b/regression/strings/java_insert_char/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_char.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* FAILURE$ +-- diff --git a/regression/strings/java_insert_char/test_insert_char.class b/regression/strings/java_insert_char/test_insert_char.class new file mode 100644 index 00000000000..fbf4a82070b Binary files /dev/null and b/regression/strings/java_insert_char/test_insert_char.class differ diff --git a/regression/strings/java_insert_char/test_insert_char.java b/regression/strings/java_insert_char/test_insert_char.java new file mode 100644 index 00000000000..3a83f03b332 --- /dev/null +++ b/regression/strings/java_insert_char/test_insert_char.java @@ -0,0 +1,10 @@ +public class test_insert_char +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ac"); + sb.insert(1, 'b'); + String s = sb.toString(); + assert(!s.equals("abc")); + } +} diff --git a/regression/strings/java_insert_char_array/test.desc b/regression/strings/java_insert_char_array/test.desc new file mode 100644 index 00000000000..2432502ce3b --- /dev/null +++ b/regression/strings/java_insert_char_array/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_char_array.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 12.* FAILURE$ +-- diff --git a/regression/strings/java_insert_char_array/test_insert_char_array.class b/regression/strings/java_insert_char_array/test_insert_char_array.class new file mode 100644 index 00000000000..bc1a23a7496 Binary files /dev/null and b/regression/strings/java_insert_char_array/test_insert_char_array.class differ diff --git a/regression/strings/java_insert_char_array/test_insert_char_array.java b/regression/strings/java_insert_char_array/test_insert_char_array.java new file mode 100644 index 00000000000..079dbd2fee6 --- /dev/null +++ b/regression/strings/java_insert_char_array/test_insert_char_array.java @@ -0,0 +1,14 @@ +public class test_insert_char_array +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + char[] array = new char[2]; + array[0] = 'b'; + array[1] = 'c'; + sb.insert(1, array); + String s = sb.toString(); + System.out.println(s); + assert(!s.equals("abcd")); + } +} diff --git a/regression/strings/java_insert_int/test.desc b/regression/strings/java_insert_int/test.desc new file mode 100644 index 00000000000..2229d33b491 --- /dev/null +++ b/regression/strings/java_insert_int/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_int.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* FAILURE$ +-- diff --git a/regression/strings/java_insert_int/test_insert_int.class b/regression/strings/java_insert_int/test_insert_int.class new file mode 100644 index 00000000000..cd355c86546 Binary files /dev/null and b/regression/strings/java_insert_int/test_insert_int.class differ diff --git a/regression/strings/java_insert_int/test_insert_int.java b/regression/strings/java_insert_int/test_insert_int.java new file mode 100644 index 00000000000..15a7a2d53f6 --- /dev/null +++ b/regression/strings/java_insert_int/test_insert_int.java @@ -0,0 +1,10 @@ +public class test_insert_int +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ac"); + sb.insert(1, 42); + String s = sb.toString(); + assert(!s.equals("a42c")); + } +} diff --git a/regression/strings/java_insert_multiple/test.desc b/regression/strings/java_insert_multiple/test.desc new file mode 100644 index 00000000000..497793cd650 --- /dev/null +++ b/regression/strings/java_insert_multiple/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_multiple.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 9.* FAILURE$ +-- diff --git a/regression/strings/java_insert_multiple/test_insert_multiple.class b/regression/strings/java_insert_multiple/test_insert_multiple.class new file mode 100644 index 00000000000..d6b470a1f72 Binary files /dev/null and b/regression/strings/java_insert_multiple/test_insert_multiple.class differ diff --git a/regression/strings/java_insert_multiple/test_insert_multiple.java b/regression/strings/java_insert_multiple/test_insert_multiple.java new file mode 100644 index 00000000000..c976ddd807f --- /dev/null +++ b/regression/strings/java_insert_multiple/test_insert_multiple.java @@ -0,0 +1,11 @@ +public class test_insert_multiple +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + sb.insert(1, 'c'); + sb.insert(1, "b"); + String s = sb.toString(); + assert(!s.equals("abcd")); + } +} diff --git a/regression/strings/java_insert_string/test.desc b/regression/strings/java_insert_string/test.desc new file mode 100644 index 00000000000..91e13cefab1 --- /dev/null +++ b/regression/strings/java_insert_string/test.desc @@ -0,0 +1,7 @@ +FUTURE +test_insert_string.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* FAILURE$ +-- diff --git a/regression/strings/java_insert_string/test_insert_string.class b/regression/strings/java_insert_string/test_insert_string.class new file mode 100644 index 00000000000..be8f7ad0f79 Binary files /dev/null and b/regression/strings/java_insert_string/test_insert_string.class differ diff --git a/regression/strings/java_insert_string/test_insert_string.java b/regression/strings/java_insert_string/test_insert_string.java new file mode 100644 index 00000000000..028a348122b --- /dev/null +++ b/regression/strings/java_insert_string/test_insert_string.java @@ -0,0 +1,10 @@ +public class test_insert_string +{ + public static void main(/*String[] argv*/) + { + StringBuilder sb = new StringBuilder("ad"); + sb.insert(1, "bc"); + String s = sb.toString(); + assert(!s.equals("abcd")); + } +} diff --git a/regression/strings/java_int/test.desc b/regression/strings/java_int/test.desc deleted file mode 100644 index ae60dd78af0..00000000000 --- a/regression/strings/java_int/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -FUTURE -test_int.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$ -^\[assertion.2\] assertion at file test_int.java line 9: SUCCESS$ -^\[assertion.3\] assertion at file test_int.java line 12: SUCCESS$ -^\[assertion.4\] assertion at file test_int.java line 15: SUCCESS$ -^\[assertion.5\] assertion at file test_int.java line 18: SUCCESS$ -^\[assertion.6\] assertion at file test_int.java line 21: SUCCESS$ -^\[assertion.7\] assertion at file test_int.java line 23: FAILURE$ --- diff --git a/regression/strings/java_int/test_int.class b/regression/strings/java_int/test_int.class deleted file mode 100644 index 643d7eca09c..00000000000 Binary files a/regression/strings/java_int/test_int.class and /dev/null differ diff --git a/regression/strings/java_int/test_int.java b/regression/strings/java_int/test_int.java deleted file mode 100644 index 620ae638dce..00000000000 --- a/regression/strings/java_int/test_int.java +++ /dev/null @@ -1,25 +0,0 @@ -public class test_int { - - public static void main(String[] argv) { - String s = Integer.toString(2345); - char c = s.charAt(1); - char d = s.charAt(2); - char e = s.charAt(3); - assert(c == '3'); - assert(d == '4'); - - int i = Integer.parseInt("1234"); - assert(i == 1234); - - String t = Integer.toString(-2345); - assert(t.charAt(0) == '-'); - - int j = Integer.parseInt("-4231"); - assert(j == -4231); - - String u = Integer.toHexString(43981); - assert(u.equals("abcd")); - - assert(e == '2' || i < 1234 || t.charAt(0) != '-' || j != -4231 || !u.equals("abcd")); - } -} diff --git a/regression/strings/java_prefix/test.desc b/regression/strings/java_prefix/test.desc deleted file mode 100644 index 175f934ca1d..00000000000 --- a/regression/strings/java_prefix/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -FUTURE -test_prefix.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$ -^\[assertion.2\] assertion at file test_prefix.java line 16: FAILURE$ -^\[assertion.3\] assertion at file test_prefix.java line 18: SUCCESS$ -^\[assertion.4\] assertion at file test_prefix.java line 20: FAILURE$ --- diff --git a/regression/strings/java_prefix/test_prefix.class b/regression/strings/java_prefix/test_prefix.class deleted file mode 100644 index 6f5f4025932..00000000000 Binary files a/regression/strings/java_prefix/test_prefix.class and /dev/null differ diff --git a/regression/strings/java_prefix/test_prefix.java b/regression/strings/java_prefix/test_prefix.java deleted file mode 100644 index c9b5fa72fcf..00000000000 --- a/regression/strings/java_prefix/test_prefix.java +++ /dev/null @@ -1,23 +0,0 @@ -public class test_prefix { - - public static void main(String[] argv) { - String s = new String("Hello World!"); - //String t = new String("Hello"); - //String u = new String("Wello"); - String u = "Wello"; - boolean b = s.startsWith("Hello"); - //boolean c = s.startsWith("Wello"); - //boolean b = s.startsWith(t); - boolean c = s.startsWith(u); - boolean d = s.startsWith("lo",3); - if(argv.length == 1){ - assert(b); - } else if(argv.length == 2){ - assert(c); - } else if(argv.length == 3){ - assert(d); - } else if(argv.length == 4){ - assert(!d); - } - } -} diff --git a/regression/strings/java_replace/test.desc b/regression/strings/java_replace/test.desc deleted file mode 100644 index 1e89ebe37b4..00000000000 --- a/regression/strings/java_replace/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_replace.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$ -^\[assertion.2\] assertion at file test_replace.java line 8: FAILURE$ --- diff --git a/regression/strings/java_replace/test_replace.class b/regression/strings/java_replace/test_replace.class deleted file mode 100644 index c795826dc15..00000000000 Binary files a/regression/strings/java_replace/test_replace.class and /dev/null differ diff --git a/regression/strings/java_replace/test_replace.java b/regression/strings/java_replace/test_replace.java deleted file mode 100644 index 342bf9afddc..00000000000 --- a/regression/strings/java_replace/test_replace.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_replace { - - public static void main(String[] argv) { - String s = new String("Hello World!"); - String t = s.replace('o','u'); - assert(t.equals("Hellu Wurld!")); - System.out.println(t); - assert(!t.equals("Hellu Wurld!")); - } -} diff --git a/regression/strings/java_set_length/test.desc b/regression/strings/java_set_length/test.desc deleted file mode 100644 index 43f82a648fd..00000000000 --- a/regression/strings/java_set_length/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -FUTURE -test_set_length.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$ -^\[assertion.2\] assertion at file test_set_length.java line 9: SUCCESS$ -^\[assertion.3\] assertion at file test_set_length.java line 10: FAILURE$ --- diff --git a/regression/strings/java_set_length/test_set_length.class b/regression/strings/java_set_length/test_set_length.class deleted file mode 100644 index 8836640967a..00000000000 Binary files a/regression/strings/java_set_length/test_set_length.class and /dev/null differ diff --git a/regression/strings/java_set_length/test_set_length.java b/regression/strings/java_set_length/test_set_length.java deleted file mode 100644 index 97b20f2332d..00000000000 --- a/regression/strings/java_set_length/test_set_length.java +++ /dev/null @@ -1,12 +0,0 @@ -public class test_set_length { - - public static void main(String[] argv) { - - StringBuilder s = new StringBuilder("abc"); - s.setLength(10); - String t = s.toString(); - assert(t.startsWith("abc")); - assert(t.length() == 10); - assert(t.length() == 3); - } -} diff --git a/regression/strings/java_string_builder/test.desc b/regression/strings/java_string_builder/test.desc deleted file mode 100644 index 9712205b104..00000000000 --- a/regression/strings/java_string_builder/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -FUTURE -test_string_builder.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$ -^\[assertion.2\] assertion at file test_string_builder.java line 12: SUCCESS$ -^\[assertion.3\] assertion at file test_string_builder.java line 13: FAILURE$ --- diff --git a/regression/strings/java_string_builder/test_string_builder.class b/regression/strings/java_string_builder/test_string_builder.class deleted file mode 100644 index 7a61d1f02be..00000000000 Binary files a/regression/strings/java_string_builder/test_string_builder.class and /dev/null differ diff --git a/regression/strings/java_string_builder/test_string_builder.java b/regression/strings/java_string_builder/test_string_builder.java deleted file mode 100644 index 1d76b34e9f8..00000000000 --- a/regression/strings/java_string_builder/test_string_builder.java +++ /dev/null @@ -1,16 +0,0 @@ -public class test_string_builder { - public static void main(String[] argv) { - if(argv.length > 2) { - StringBuilder tmp = new StringBuilder(); - tmp.append("prefix "); - tmp.append(argv[1]); - tmp.append(" middle ").append(argv[2]).append(" end"); - //StringBuilder tmp1 = tmp.append(argv[2]); - //tmp1.append(" end"); - String r = tmp.toString(); - assert(r.startsWith("pref")); - assert(r.endsWith("end")); - assert(r.startsWith("pr3f")); - } - } -} diff --git a/regression/strings/java_string_builder_insert/test.desc b/regression/strings/java_string_builder_insert/test.desc deleted file mode 100644 index 2655f846da1..00000000000 --- a/regression/strings/java_string_builder_insert/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_insert.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$ -^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$ --- diff --git a/regression/strings/java_string_builder_insert/test_insert.class b/regression/strings/java_string_builder_insert/test_insert.class deleted file mode 100644 index 69a32d7f93f..00000000000 Binary files a/regression/strings/java_string_builder_insert/test_insert.class and /dev/null differ diff --git a/regression/strings/java_string_builder_insert/test_insert.java b/regression/strings/java_string_builder_insert/test_insert.java deleted file mode 100644 index 1fac897c5ed..00000000000 --- a/regression/strings/java_string_builder_insert/test_insert.java +++ /dev/null @@ -1,20 +0,0 @@ -public class test_insert { - - public static void main(String[] argv) - { - char [] str = new char[5]; - str[0] = 'H'; - str[1] = 'e'; - str[2] = 'l'; - str[3] = 'l'; - str[4] = 'o'; - - - StringBuilder sb = new StringBuilder(" world"); - sb.insert(0,str); - String s = sb.toString(); - System.out.println(s); - assert(s.equals("Hello world")); - assert(!s.equals("Hello world")); - } -} diff --git a/regression/strings/java_string_builder_length/test.desc b/regression/strings/java_string_builder_length/test.desc deleted file mode 100644 index c4720992571..00000000000 --- a/regression/strings/java_string_builder_length/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_sb_length.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -\[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$ -\[assertion.2\] assertion at file test_sb_length.java line 8: FAILURE$ --- diff --git a/regression/strings/java_string_builder_length/test_sb_length.class b/regression/strings/java_string_builder_length/test_sb_length.class deleted file mode 100644 index 586e8f71935..00000000000 Binary files a/regression/strings/java_string_builder_length/test_sb_length.class and /dev/null differ diff --git a/regression/strings/java_string_builder_length/test_sb_length.java b/regression/strings/java_string_builder_length/test_sb_length.java deleted file mode 100644 index 652b72cdc90..00000000000 --- a/regression/strings/java_string_builder_length/test_sb_length.java +++ /dev/null @@ -1,11 +0,0 @@ -public class test_sb_length { - public static void main(String[] argv) { - StringBuilder tmp = new StringBuilder("prefix"); - //tmp.append("prefix"); - tmp.append("end"); - assert(tmp.length() == 9); - if(argv.length > 1) { - assert(tmp.length() == 12); - } - } -} diff --git a/regression/strings/java_strlen/test.desc b/regression/strings/java_strlen/test.desc deleted file mode 100644 index b98e6f76f0a..00000000000 --- a/regression/strings/java_strlen/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_length.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$ -^\[assertion.2\] assertion at file test_length.java line 11: FAILURE$ --- diff --git a/regression/strings/java_strlen/test_length.class b/regression/strings/java_strlen/test_length.class deleted file mode 100644 index 7f1c10c02ca..00000000000 Binary files a/regression/strings/java_strlen/test_length.class and /dev/null differ diff --git a/regression/strings/java_strlen/test_length.java b/regression/strings/java_strlen/test_length.java deleted file mode 100644 index 9410315db38..00000000000 --- a/regression/strings/java_strlen/test_length.java +++ /dev/null @@ -1,14 +0,0 @@ -public class test_length { - - public static void main(String[] argv) { - String s = new String("hello"); - if(argv.length > 1) { - String t = argv[1]; - int i = t.length(); - String u = t.concat(s); - char c = u.charAt(i); - assert(c == 'h'); - assert(c == 'o'); - } - } -} diff --git a/regression/strings/java_substring/test.desc b/regression/strings/java_substring/test.desc deleted file mode 100644 index bd54a8204fe..00000000000 --- a/regression/strings/java_substring/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -FUTURE -test_substring.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$ -^\[assertion.2\] assertion at file test_substring.java line 13: FAILURE$ -^\[assertion.3\] assertion at file test_substring.java line 20: SUCCESS$ -^\[assertion.4\] assertion at file test_substring.java line 21: FAILURE$ --- diff --git a/regression/strings/java_substring/test_substring.class b/regression/strings/java_substring/test_substring.class deleted file mode 100644 index e6532aca43e..00000000000 Binary files a/regression/strings/java_substring/test_substring.class and /dev/null differ diff --git a/regression/strings/java_substring/test_substring.java b/regression/strings/java_substring/test_substring.java deleted file mode 100644 index 8a2ac883cca..00000000000 --- a/regression/strings/java_substring/test_substring.java +++ /dev/null @@ -1,27 +0,0 @@ -public class test_substring { - - public static void main(String[] argv) { - if(argv.length > 1) { - String t = argv[1]; - - if(t.length() == 6) { - String u = t.substring(2,4); - char c = u.charAt(1); - char d = t.charAt(3); - char e = t.charAt(4); - assert(c == d); - assert(c == e); - } - else if(t.length() == 5){ - CharSequence u = t.subSequence(2,4); - char c = u.charAt(1); - char d = t.charAt(3); - char e = t.charAt(4); - assert(c == d); - assert(c == e); - } - - - } - } -} diff --git a/regression/strings/java_suffix/test.desc b/regression/strings/java_suffix/test.desc deleted file mode 100644 index 2740e87d6e4..00000000000 --- a/regression/strings/java_suffix/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_suffix.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$ -^\[assertion.2\] assertion at file test_suffix.java line 13: FAILURE$ --- diff --git a/regression/strings/java_suffix/test_suffix.class b/regression/strings/java_suffix/test_suffix.class deleted file mode 100644 index 557acd02653..00000000000 Binary files a/regression/strings/java_suffix/test_suffix.class and /dev/null differ diff --git a/regression/strings/java_suffix/test_suffix.java b/regression/strings/java_suffix/test_suffix.java deleted file mode 100644 index f61b0b8ba36..00000000000 --- a/regression/strings/java_suffix/test_suffix.java +++ /dev/null @@ -1,15 +0,0 @@ -public class test_suffix { - - public static void main(String[] argv) { - String s = new String("Hello World!"); - //String t = new String("Hello"); - //String u = new String("Wello"); - String u = "Wello!"; - boolean b = s.endsWith("World!"); - //boolean c = s.startsWith("Wello"); - //boolean b = s.startsWith(t); - boolean c = s.startsWith(u); - assert(b); - assert(c); - } -} diff --git a/regression/strings/java_trim/test.desc b/regression/strings/java_trim/test.desc deleted file mode 100644 index 7c0f1a87978..00000000000 --- a/regression/strings/java_trim/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_trim.class ---string-refine -^EXIT=10$ -^SIGNAL=0$ -^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$ -^\[assertion.2\] assertion at file test_trim.java line 6: FAILURE$ --- diff --git a/regression/strings/java_trim/test_trim.class b/regression/strings/java_trim/test_trim.class deleted file mode 100644 index 8e6a923dcbc..00000000000 Binary files a/regression/strings/java_trim/test_trim.class and /dev/null differ diff --git a/regression/strings/java_trim/test_trim.java b/regression/strings/java_trim/test_trim.java deleted file mode 100644 index 8d8d41cb29a..00000000000 --- a/regression/strings/java_trim/test_trim.java +++ /dev/null @@ -1,8 +0,0 @@ -public class test_trim { - public static void main(String[] argv) { - String t = " a b c "; - String x = t.trim(); - assert(x.equals("a b c")); - assert(x.equals("abc ")); - } -} diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc index b86ded86c18..2e0b38c3ae3 100644 --- a/regression/strings/test1/test.desc +++ b/regression/strings/test1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$ diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc index b322a1d0d33..809cbcdaa29 100644 --- a/regression/strings/test2/test.desc +++ b/regression/strings/test2/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion n == 5: SUCCESS$ diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc index c88a62b6704..6fddff4c129 100644 --- a/regression/strings/test3.1/test.desc +++ b/regression/strings/test3.1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc index c88a62b6704..6fddff4c129 100644 --- a/regression/strings/test3.2/test.desc +++ b/regression/strings/test3.2/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc index c88a62b6704..6fddff4c129 100644 --- a/regression/strings/test3.3/test.desc +++ b/regression/strings/test3.3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc index d88e1c83744..fc1cde2392c 100644 --- a/regression/strings/test3.4/test.desc +++ b/regression/strings/test3.4/test.desc @@ -1,7 +1,7 @@ FUTURE -test.c ---string-refine -^EXIT=10$ +test_init.class +--refine-strings +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ +^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc index 24ed719acc2..f6f9a63520a 100644 --- a/regression/strings/test3/test.desc +++ b/regression/strings/test3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_length\(s\) == i \+ 5: SUCCESS$ diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc index c88a62b6704..6fddff4c129 100644 --- a/regression/strings/test4/test.desc +++ b/regression/strings/test4/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc index d88e1c83744..303defd9de4 100644 --- a/regression/strings/test5/test.desc +++ b/regression/strings/test5/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc index 99f3cfd81de..360759faf98 100644 --- a/regression/strings/test_char_set/test.desc +++ b/regression/strings/test_char_set/test.desc @@ -1,8 +1,8 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("apc"\)): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("abc"\)): FAILURE$ +^\[.*assertion.1\].* SUCCESS$ +^\[.*assertion.2\].* FAILURE$ -- diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc index 8df68c18bc3..317a4d1b4dd 100644 --- a/regression/strings/test_concat/test.desc +++ b/regression/strings/test_concat/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion c == .p.: SUCCESS$ diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc index f2414880794..b0e33ce2b43 100644 --- a/regression/strings/test_contains/test.desc +++ b/regression/strings/test_contains/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"3\"\)): SUCCESS$ diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc index 5fbe05f8fdd..34297ec50f5 100644 --- a/regression/strings/test_equal/test.desc +++ b/regression/strings/test_equal/test.desc @@ -1,8 +1,8 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("pippo"\)): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("mippo"\)): FAILURE$ +^\[.*.assertion.1\].* SUCCESS$ +^\[.*.assertion.2\].* FAILURE$ -- diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc index edc8e09c4ed..a2c12c3d259 100644 --- a/regression/strings/test_index_of/test.desc +++ b/regression/strings/test_index_of/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$ diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc index 8d78e11e71b..fcce43ca76c 100644 --- a/regression/strings/test_int/test.desc +++ b/regression/strings/test_int/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$ diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc index 9bb75eda5b6..f2f54e69921 100644 --- a/regression/strings/test_pass1/test.desc +++ b/regression/strings/test_pass1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc index 3edb9f68f7a..f1f3d1618c8 100644 --- a/regression/strings/test_pass_pc3/test.desc +++ b/regression/strings/test_pass_pc3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_length\(s3\) == 0: FAILURE$ diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc index 6c62a2fa466..be0ed5dc69e 100644 --- a/regression/strings/test_prefix/test.desc +++ b/regression/strings/test_prefix/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion b: SUCCESS$ diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc index 30c3f4066ed..28ed1b7e698 100644 --- a/regression/strings/test_strlen/test.desc +++ b/regression/strings/test_strlen/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$ diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc index a32376aca23..f0e4b5832b2 100644 --- a/regression/strings/test_substring/test.desc +++ b/regression/strings/test_substring/test.desc @@ -1,10 +1,10 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cc"\)): FAILURE$ -^\[main.assertion.3\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("bc"\)): SUCCESS$ -^\[main.assertion.4\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): FAILURE$ +^\[.*assertion.1\].* SUCCESS$ +^\[.*assertion.2\].* FAILURE$ +^\[.*assertion.3\].* SUCCESS$ +^\[.*assertion.4\].* FAILURE$ -- diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc index 9f425595434..e7e8c1e36be 100644 --- a/regression/strings/test_suffix/test.desc +++ b/regression/strings/test_suffix/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---string-refine +--refine-strings ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("po"\),s\): SUCCESS$