Implement model for String.equals

codebyzeb · romainbrenguier · commit 0bf58a5203f8 · 2018-08-01T08:46:28.000+01:00
String.equals currently handled by CBMC, this removes support
within CBMC so that String.equals will be handled by a model instead.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check
+--function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 13 .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess
+--max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 23 .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringEquals/test.desc b/jbmc/regression/jbmc-strings/StringEquals/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 40 --function Test.check
+--max-nondet-string-length 40 --function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 9 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 20 --unwind 30 --function Test.verifyNonNull
+--max-nondet-string-length 20 --unwind 30 --function Test.verifyNonNull --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous04.class
---max-nondet-string-length 1000 --unwind 30
+--max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringSubstring/test.desc b/jbmc/regression/jbmc-strings/StringSubstring/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---unwind 10 --max-nondet-string-length 6  --function Test.testSuccess
+--unwind 10 --max-nondet-string-length 6  --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 21.*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/SubString01/test.desc b/jbmc/regression/jbmc-strings/SubString01/test.desc
@@ -1,6 +1,6 @@
 CORE
 SubString01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfLong.class
---max-nondet-string-length 1000 --function StringValueOfLong.main
+--max-nondet-string-length 1000 --function StringValueOfLong.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfBool.class
---max-nondet-string-length 1000 --function StringValueOfBool.main
+--max-nondet-string-length 1000 --function StringValueOfBool.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.test --cover location --trace --json-ui
+--function Test.test --cover location --trace --json-ui --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
-20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)
+64 of 92 covered \(69\.6%\)
diff --git a/jbmc/regression/jbmc-strings/cprover/CProverString.java b/jbmc/regression/jbmc-strings/cprover/CProverString.java
@@ -63,6 +63,14 @@ public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
         return sb.deleteCharAt(index);
     }
 
+    public static boolean equals(String a, String b)
+    {
+        if (a == null) {
+            return b == null;
+        }
+        return a.length() == b.length() && a.startsWith(b);
+    }
+
     public static StringBuilder insert(
             StringBuilder sb, int offset, String str) {
         return sb.insert(offset, str);
diff --git a/jbmc/regression/jbmc-strings/java_append_char/test.desc b/jbmc/regression/jbmc-strings/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---max-nondet-string-length 1000 --function test_append_char.main
+--max-nondet-string-length 1000 --function test_append_char.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/java_char_array_init/test.desc b/jbmc/regression/jbmc-strings/java_char_array_init/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_init.class
---max-nondet-string-length 1000 --function test_init.main
+--max-nondet-string-length 1000 --function test_init.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_init.java line 31 .* SUCCESS$
diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test.desc b/jbmc/regression/jbmc-strings/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---max-nondet-string-length 1000 --function test_insert_char.main
+--max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_append_char/test.desc b/jbmc/regression/strings-smoke-tests/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---verbosity 10 --max-nondet-string-length 1000
+--verbosity 10 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_append_char.java line 23 .* SUCCESS
diff --git a/jbmc/regression/strings-smoke-tests/java_append_string/test.desc b/jbmc/regression/strings-smoke-tests/java_append_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_case/test.desc b/jbmc/regression/strings-smoke-tests/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---verbosity 10 --max-nondet-string-length 1000 --function test_case.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_equal/test.desc b/jbmc/regression/strings-smoke-tests/java_equal/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_equal.class
---verbosity 10 --max-nondet-string-length 100
+--verbosity 10 --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_format/test.desc b/jbmc/regression/strings-smoke-tests/java_format/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format2/test.desc b/jbmc/regression/strings-smoke-tests/java_format2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format3/test.desc b/jbmc/regression/strings-smoke-tests/java_format3/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_if/test.desc b/jbmc/regression/strings-smoke-tests/java_if/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 100 --function test.main
+--verbosity 10 --max-nondet-string-length 100 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 11.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---verbosity 10  --max-nondet-string-length 1000 --function test_insert_char.main
+--verbosity 10  --max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---verbosity 10 --max-nondet-string-length 1000 --function Test4.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---verbosity 10 --max-nondet-string-length 1000 --function Test5.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main
+--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---verbosity 10 --max-nondet-string-length 1000 --function Test5.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main
+--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
