diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index c86885cfd2e..c9d9226d346 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit c86885cfd2e8cf98947132de15bcfa3835ae3ebc +Subproject commit c9d9226d34649c21f30bb99f92e0a3d6e5fb8977 diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc index c085d3c6925..6548c5cfd69 100644 --- 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 . ../../../lib/java-models-library/target/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 index 09c05d89840..652cb83a258 100644 --- 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 . ../../../lib/java-models-library/target/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 index 3b16b6472cc..b7ff1d977cd 100644 --- 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 . ../../../lib/java-models-library/target/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 index 2a4995cc7b0..658e20f4a42 100644 --- 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 . ../../../lib/java-models-library/target/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 index 5a6493cc9dd..a5ba422b1fc 100644 --- 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 . ../../../lib/java-models-library/target/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 index 77004d943d0..6e2c644b6e8 100644 --- 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 . ../../../lib/java-models-library/target/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 index 7d212539658..5157c1be281 100644 --- 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 . ../../../lib/java-models-library/target/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 index 8f6e86bcba9..20ed7a4c860 100644 --- 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 . ../../../lib/java-models-library/target/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 index 2a4950dbf45..e52e6d77905 100644 --- 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 . ../../../lib/java-models-library/target/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 index 2631500be00..b3c3e06f78f 100644 --- 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 . ../../../lib/java-models-library/target/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 index d25b7391444..421bcd60cc3 100644 --- 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 --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 diff --git a/jbmc/regression/jbmc-strings/java_append_char/test.desc b/jbmc/regression/jbmc-strings/java_append_char/test.desc index 71043e73f19..0feb7314782 100644 --- 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 . ../../../lib/java-models-library/target/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 index d73e3c7dbac..76e0fabf8f5 100644 --- 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 . ../../../lib/java-models-library/target/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 index 9a83cbda83c..72c885f35ee 100644 --- 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 . ../../../lib/java-models-library/target/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 index ac1c9428a67..cf8f2e31ecb 100644 --- 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 . ../../../lib/java-models-library/target/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 index 6f95d07fc09..66470659f76 100644 --- 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 . ../../../lib/java-models-library/target/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 index 1d6ecc944c3..da0703b2a91 100644 --- 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 . ../../../lib/java-models-library/target/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 index 778e65ea7c3..da76a225dd7 100644 --- 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 . ../../../lib/java-models-library/target/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 index 116034ea133..1ffde552029 100644 --- 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 . ../../../lib/java-models-library/target/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 index 596c113a269..3e95de2da58 100644 --- 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 . ../../../lib/java-models-library/target/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 index f8e74ee54e1..331f4c619b2 100644 --- 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 . ../../../lib/java-models-library/target/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 index 47a451b32d1..e067816ba2d 100644 --- 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 . ../../../lib/java-models-library/target/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 index 13181d89185..8ec0ccd7115 100644 --- 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 . ../../../lib/java-models-library/target/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 index a9502c6fcca..57fb092553a 100644 --- 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 . ../../../lib/java-models-library/target/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 index 1d763c7bc2f..6bd6ccb525c 100644 --- 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 . ../../../lib/java-models-library/target/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 index af69a7a96b3..79353940068 100644 --- 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 . ../../../lib/java-models-library/target/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 index 5e399123ae3..57be32d5863 100644 --- 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 . ../../../lib/java-models-library/target/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 index 2836a8e301a..152582bb0cc 100644 --- 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 . ../../../lib/java-models-library/target/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 index 89d011bd40b..b20b4b8d28b 100644 --- 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 . ../../../lib/java-models-library/target/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 index 24fa815010f..a9754298dae 100644 --- 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 . ../../../lib/java-models-library/target/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 index 38bd06e75c4..cec7e75f38b 100644 --- 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 . ../../../lib/java-models-library/target/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 index af9f367a40a..416de68ef04 100644 --- 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 . ../../../lib/java-models-library/target/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 index bea25418b87..ea585467d6d 100644 --- 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 . ../../../lib/java-models-library/target/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 index ffe64c3c60a..3ecbd196acd 100644 --- 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 . ../../../lib/java-models-library/target/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 index 101333b4532..839901b1767 100644 --- 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 . ../../../lib/java-models-library/target/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 index ca902955ffd..65350100490 100644 --- 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 . ../../../lib/java-models-library/target/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 index ee6a2476f08..0c37cd057f6 100644 --- 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 . ../../../lib/java-models-library/target/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 index b4cdac17a5f..e9c03f7d20d 100644 --- 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 . ../../../lib/java-models-library/target/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 index e8f2161cd07..446432b16a0 100644 --- 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 . ../../../lib/java-models-library/target/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 index 56d6b4e18d1..5533dcc9727 100644 --- 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 . ../../../lib/java-models-library/target/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 index 7905d63513f..f75efa020ec 100644 --- 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 . ../../../lib/java-models-library/target/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 index afbf33b8565..3825202eb48 100644 --- 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 . ../../../lib/java-models-library/target/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 index 2836a8e301a..152582bb0cc 100644 --- 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 . ../../../lib/java-models-library/target/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 index af9f367a40a..416de68ef04 100644 --- 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 . ../../../lib/java-models-library/target/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 index ca902955ffd..65350100490 100644 --- 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 . ../../../lib/java-models-library/target/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 index ee6a2476f08..0c37cd057f6 100644 --- 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 . ../../../lib/java-models-library/target/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 index b4cdac17a5f..e9c03f7d20d 100644 --- 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 . ../../../lib/java-models-library/target/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 index e8f2161cd07..446432b16a0 100644 --- 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 . ../../../lib/java-models-library/target/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 index 98a4ff52518..78fc88f64df 100644 --- 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 @@ -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$ 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 index 5111865d119..bcfafdfeba1 100644 --- 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 @@ -1,6 +1,6 @@ CORE Test_octal2.class ---verbosity 10 --max-nondet-string-length 100 --function Test_octal2.main +--verbosity 10 --max-nondet-string-length 100 --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$ 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 index 612a31faed9..73df760e443 100644 --- 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 @@ -1,6 +1,6 @@ CORE Test_octal3.class ---verbosity 10 --max-nondet-string-length 100 --function Test_octal3.main +--verbosity 10 --max-nondet-string-length 100 --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$ diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc index 2df369dfaea..754bda5048d 100644 --- a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc @@ -1,6 +1,6 @@ CORE test_replace_char.class ---verbosity 10 --max-nondet-string-length 1000 --function test_replace_char.main +--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` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 index b394b585a0e..43ef5163a91 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_set_char_at.class ---verbosity 10 --max-nondet-string-length 1000 --function test_set_char_at.main +--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` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc index 6884c820757..37cc7923bbb 100644 --- a/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---verbosity 10 --function Test.check --max-nondet-string-length 100 --string-printable --java-assume-inputs-non-null +--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` ^EXIT=10$ ^SIGNAL=0$ assertion.* file Test.java line 6 .* SUCCESS 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 index 567d75e441e..7250e66f0ea 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc @@ -1,6 +1,6 @@ CORE test.class ---verbosity 10 --function test.check --max-nondet-string-length 100 +--verbosity 10 --function test.check --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 7 .* SUCCESS$ 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 index a2bb2d0d696..5e816958c53 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -1,6 +1,6 @@ CORE test.class ---verbosity 10 --max-nondet-string-length 1000 --function test.main +--verbosity 10 --max-nondet-string-length 1000 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 9 .* SUCCESS$ diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 7c39fde5d55..ebf92963563 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -942,72 +942,6 @@ java_string_library_preprocesst::string_literal_to_string_expr( ID_cprover_string_literal_func, {expr}, loc, symbol_table, code); } -/// Used to provide code for the Java String.equals(Object) function. -/// \param type: type of the function call -/// \param loc: location in the program_invocation_name -/// \param symbol_table: symbol table -/// \param function_id: unused -/// \return Code corresponding to: -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// IF arg->@class_identifier == "java.lang.String" -/// THEN -/// string_expr1 = {this->length; *this->data} -/// string_expr2 = {arg->length; *arg->data} -/// bool string_equals_tmp = cprover_string_equal(string_expr1, string_expr2) -/// return string_equals_tmp -/// ELSE -/// return false -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -codet java_string_library_preprocesst::make_equals_function_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table) -{ - const typet &return_type = type.return_type(); - exprt::operandst ops; - for(const auto &p : type.parameters()) - { - symbol_exprt sym(p.get_identifier(), p.type()); - ops.push_back(sym); - } - - code_ifthenelset code; - code.cond() = [&] { - const member_exprt class_identifier( - checked_dereference(ops[1], ops[1].type().subtype()), - "@class_identifier", - string_typet()); - return equal_exprt( - class_identifier, - constant_exprt("java::java.lang.String", string_typet())); - }(); - - code.then_case() = [&] { - code_blockt instance_case; - // Check content equality - const symbolt string_equals_sym = get_fresh_aux_symbol( - return_type, - id2string(function_id), - "str_eq", - loc, - ID_java, - symbol_table); - const symbol_exprt string_equals = string_equals_sym.symbol_expr(); - instance_case.add(code_declt(string_equals), loc); - const exprt::operandst args = - process_equals_function_operands(ops, loc, symbol_table, instance_case); - const auto fun_app = make_function_application( - ID_cprover_string_equal_func, args, return_type, symbol_table); - instance_case.add(code_assignt(string_equals, fun_app), loc); - instance_case.add(code_returnt(string_equals), loc); - return instance_case; - }(); - - code.else_case() = code_returnt(from_integer(false, return_type)); - return code; -} - /// Provide code for the String.valueOf(F) function. /// \param type: type of the function call /// \param loc: location in the program_invocation_name @@ -2031,15 +1965,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]= ID_cprover_string_endswith_func; - - conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"] = - std::bind( - &java_string_library_preprocesst::make_equals_function_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3, - std::placeholders::_4); cprover_equivalent_to_java_function ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]= ID_cprover_string_equals_ignore_case_func; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h index 78c3ae4667f..dca4e97d2cd 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.h +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h @@ -145,12 +145,6 @@ class java_string_library_preprocesst:public messaget // A set tells us what java types should be considered as string objects std::unordered_set string_types; - codet make_equals_function_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table); - codet make_float_to_string_code( const java_method_typet &type, const source_locationt &loc, diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp index 9bfd8c125a4..1297d5ccc6c 100644 --- a/src/solvers/flattening/boolbv_array.cpp +++ b/src/solvers/flattening/boolbv_array.cpp @@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_array(const exprt &expr) { - std::size_t width=boolbv_width(expr.type()); + const std::size_t width = boolbv_width(expr.type()); + const exprt::operandst &operands = expr.operands(); - if(width==0) - return conversion_failed(expr); + if(operands.empty() && width == 0) + return bvt(); if(expr.type().id()==ID_array) { @@ -24,7 +25,7 @@ bvt boolbvt::convert_array(const exprt &expr) "the bit width being nonzero implies that the array has a nonzero size " "in which case the array shall have operands"); const exprt::operandst &operands=expr.operands(); - std::size_t op_width=width/operands.size(); + const std::size_t op_width = width / operands.size(); bvt bv; bv.reserve(width); diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index d9262493cfb..a10a24097d8 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -105,7 +105,6 @@ static void update_index_set( /// \param val: an index expression /// \return `axiom` with substitued `qvar` static exprt instantiate( - messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val); @@ -229,7 +228,6 @@ static void display_index_set( /// (See `instantiate(const string_not_contains_constraintt&,const index_set_pairt&,const string_constraint_generatort&,const std::map&)` /// for details) static std::vector generate_instantiations( - messaget::mstreamt &stream, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms, @@ -242,7 +240,7 @@ static std::vector generate_instantiations( for(const auto &univ_axiom : axioms.universal) { for(const auto &j : i.second) - lemmas.push_back(instantiate(stream, univ_axiom, i.first, j)); + lemmas.push_back(instantiate(univ_axiom, i.first, j)); } } for(const auto &nc_axiom : axioms.not_contains) @@ -762,8 +760,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() initial_index_set(index_sets, ns, axioms); update_index_set(index_sets, ns, current_constraints); current_constraints.clear(); - for(const auto &instance : generate_instantiations( - debug(), generator, index_sets, axioms, not_contain_witnesses)) + const auto instances = generate_instantiations( + generator, index_sets, axioms, not_contain_witnesses); + for(const auto &instance : instances) add_lemma(instance); while((loop_bound_--)>0) @@ -819,8 +818,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() } } current_constraints.clear(); - for(const auto &instance : generate_instantiations( - debug(), generator, index_sets, axioms, not_contain_witnesses)) + const auto instances = generate_instantiations( + generator, index_sets, axioms, not_contain_witnesses); + for(const auto &instance : instances) add_lemma(instance); } else @@ -1519,7 +1519,6 @@ exprt simplify_sum(const exprt &f) /// $q + x$, `compute_inverse_function(q,v,f)` returns an expression /// for $v - x$. static exprt compute_inverse_function( - messaget::mstreamt &stream, const exprt &qvar, const exprt &val, const exprt &f) @@ -1550,8 +1549,6 @@ static exprt compute_inverse_function( "a proper function must have exactly one " "occurrences after reduction, or it cancelled out, and it does not" " have one")); - stream << "in string_refinementt::compute_inverse_function:" - << " warning: occurrences of qvar cancelled out " << messaget::eom; } elems.erase(it); @@ -1824,32 +1821,30 @@ find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar) } /// Instantiates a string constraint by substituting the quantifiers. -/// For a string constraint of the form \f$\forall q. P(x)\f$, -/// substitute `qvar` the universally quantified variable of `axiom`, by -/// an index `val`, in `axiom`, so that the index used for `str` equals `val`. -/// For instance, if `axiom` corresponds to \f$\forall q. s[q+x]={\tt 'a'} \land -/// t[q]={\tt 'b'} \f$, `instantiate(axiom,s,v)` would return an expression for -/// \f$s[v]={\tt 'a'} \land t[v-x]={\tt 'b'}\f$. -/// \param stream: a message stream -/// \param axiom: a universally quantified formula `axiom` +/// For a string constraint of the form `forall q. P(x)`, +/// substitute `q` the universally quantified variable of `axiom`, by +/// an `index`, in `axiom`, so that the index used for `str` equals `val`. +/// For instance, if `axiom` is `forall q. s[q+x] = 'a' && t[q] = 'b'`, +/// `instantiate(axiom,s,v)` would return the expression +/// `s[v] = 'a' && t[v-x] = 'b'`. +/// If there are several such indexes, the conjunction of the instantiations is +/// returned, for instance for a formula: +/// `forall q. s[q+x]='a' && s[q]=c` we would get +/// `s[v] = 'a' && s[v-x] = c && s[v+x] = 'a' && s[v] = c`. +/// \param axiom: a universally quantified formula /// \param str: an array of characters /// \param val: an index expression /// \return instantiated formula static exprt instantiate( - messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val) { - const auto indexes = find_indexes(axiom.body, str, axiom.univ_var); - INVARIANT( - str.id() == ID_array || indexes.size() <= 1, - "non constant array should always be accessed at the same index"); exprt::operandst conjuncts; - for(const auto &index : indexes) + for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var)) { const exprt univ_var_value = - compute_inverse_function(stream, axiom.univ_var, val, index); + compute_inverse_function(axiom.univ_var, val, index); implies_exprt instance( and_exprt( binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),