Skip to content

Implement model for String.equals #2588

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Oct 1, 2018
Merged

Implement model for String.equals #2588

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
1b349ed
Update java-models-library submodule
codebyzeb Jul 20, 2018
77131c0
Allow empty arrays in convert_array
romainbrenguier Aug 8, 2018
968c239
Use java models in String tests
romainbrenguier Aug 6, 2018
7e53e6e
Stop preprocessing String.equals
codebyzeb Jul 20, 2018
6d153a2
Stop output of useless warning
romainbrenguier Sep 10, 2018
ff740ef
Relax condition in instantiate
romainbrenguier Sep 10, 2018
a485739
Improve documentation of instantiate
romainbrenguier Sep 28, 2018
87bd027
Use java-models-library instead of java_bycode/library
romainbrenguier Oct 1, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion jbmc/lib/java-models-library
Open in desktop
Submodule java-models-library updated 1 files
+26 −4 src/main/java/java/lang/String.java
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test.class
--function Test.check
--function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does this work on windows ?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think format_classpath.sh is made specifically to work on linux, mac and windows (unlike using : as a separator)

^SIGNAL=0$
assertion at file Test.java line 13 .*: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 23 .*: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringConcatenation01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
StringConcatenation01.class
--max-nondet-string-length 1000
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringEquals/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion at file Test.java line 9 .* SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 48 .* SUCCESS
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/StringSubstring/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 21.*: SUCCESS
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/SubString01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
SubString01.class
--max-nondet-string-length 1000
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/char_escape/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test.class
--function Test.test --trace --json-ui
--function Test.test --trace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --json-ui
^EXIT=10$
^SIGNAL=0$
"reason": "assertion at file Test.java line 14
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/java_append_char/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/java_char_array_init/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* file test_init.java line 31 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-strings/java_insert_char/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion\.1\].* line 8.* FAILURE$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_append_char/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* file test_append_char.java line 23 .* SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_append_string/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_case/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* file test_case.java line 10 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_equal/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* FAILURE$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_format/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 6.* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_format2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 6.* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_format3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 7.* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_if/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 11.* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_octal1.class
--verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main
--verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
assertion.* line 7 .* SUCCESS$
Expand Down
Loading