Skip to content

Commit 87bd027

Browse files
Use java-models-library instead of java_bycode/library
1 parent a485739 commit 87bd027

File tree

42 files changed

+42
-42
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+42
-42
lines changed

jbmc/regression/strings-smoke-tests/java_append_char/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_append_char.class
3-
--verbosity 10 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file test_append_char.java line 23 .* SUCCESS

jbmc/regression/strings-smoke-tests/java_append_string/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_append_string.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_case/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_case.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file test_case.java line 10 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_delete_char_at.class
3-
--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`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_equal/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_equal.class
3-
--verbosity 10 --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 8.* FAILURE$

jbmc/regression/strings-smoke-tests/java_format/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 6.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_format2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 6.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_format3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 7.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_if/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --max-nondet-string-length 100 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 11.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_insert_char/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_insert_char.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_insert_char_array.class
3-
--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`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file test_insert_char_array.java line 20 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_insert_multiple.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_insert_string/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_insert_string.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test2.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test3.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test4.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test5.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_binary1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_binary2.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_binary3.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_decimal.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex2.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex3.class
3-
--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal2.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal3.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test5.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_decimal.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex1.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex2.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_hex3.class
3-
--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal1.class
3-
--verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal2.class
3-
--verbosity 10 --max-nondet-string-length 100 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test_octal3.class
3-
--verbosity 10 --max-nondet-string-length 100 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 100 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_replace_char/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_replace_char.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_replace_char.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_replace_char.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test_set_char_at.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test_set_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test_set_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/strings-smoke-tests/java_string_printable/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test.class
3-
--verbosity 10 --function Test.check --max-nondet-string-length 100 --string-printable --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --function Test.check --max-nondet-string-length 100 --string-printable --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file Test.java line 6 .* SUCCESS

jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --function test.check --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --function test.check --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file test.java line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
test.class
3-
--verbosity 10 --max-nondet-string-length 1000 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--verbosity 10 --max-nondet-string-length 1000 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* file test.java line 9 .* SUCCESS$

0 commit comments

Comments
 (0)