From 7ef8a0edbb5325b7c0772ed68dee8488a777c060 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 15 Jul 2018 12:00:45 +0100 Subject: [PATCH] Remove obsolete string-max-length option --- .../jbmc-strings/CharacterGetNumericValue/test.desc | 2 +- jbmc/regression/jbmc-strings/RegexMatches01/test.desc | 2 +- jbmc/regression/jbmc-strings/RegexMatches02/test.desc | 2 +- .../jbmc-strings/RegexSubstitution01/test.desc | 2 +- .../jbmc-strings/RegexSubstitution02/test.desc | 2 +- .../jbmc-strings/RegexSubstitution03/test.desc | 2 +- jbmc/regression/jbmc-strings/StartsWith/test.desc | 2 +- jbmc/regression/jbmc-strings/StartsWith/test_det.desc | 2 +- .../jbmc-strings/StartsWith/test_nondet.desc | 2 +- .../jbmc-strings/StaticCharMethods01/test.desc | 2 +- .../jbmc-strings/StaticCharMethods02/test.desc | 2 +- .../jbmc-strings/StaticCharMethods03/test.desc | 2 +- .../jbmc-strings/StaticCharMethods04/test.desc | 2 +- .../jbmc-strings/StaticCharMethods05/test.desc | 2 +- .../jbmc-strings/StaticCharMethods06/test.desc | 2 +- jbmc/regression/jbmc-strings/StringArray/test.desc | 2 +- .../jbmc-strings/StringBuilderAppend01/test.desc | 2 +- .../jbmc-strings/StringBuilderAppend02/test.desc | 2 +- .../jbmc-strings/StringBuilderCapLen01/test.desc | 2 +- .../jbmc-strings/StringBuilderCapLen02/test.desc | 2 +- .../jbmc-strings/StringBuilderCapLen03/test.desc | 2 +- .../jbmc-strings/StringBuilderCapLen04/test.desc | 2 +- .../jbmc-strings/StringBuilderChars01/test.desc | 2 +- .../jbmc-strings/StringBuilderChars02/test.desc | 2 +- .../jbmc-strings/StringBuilderChars03/test.desc | 2 +- .../jbmc-strings/StringBuilderChars04/test.desc | 2 +- .../jbmc-strings/StringBuilderChars05/test.desc | 2 +- .../jbmc-strings/StringBuilderChars06/test.desc | 2 +- .../jbmc-strings/StringBuilderConstructors01/test.desc | 2 +- .../jbmc-strings/StringBuilderConstructors02/test.desc | 2 +- .../jbmc-strings/StringBuilderInsertDelete01/test.desc | 2 +- .../jbmc-strings/StringBuilderInsertDelete02/test.desc | 2 +- .../jbmc-strings/StringBuilderInsertDelete03/test.desc | 2 +- jbmc/regression/jbmc-strings/StringCompare01/test.desc | 2 +- jbmc/regression/jbmc-strings/StringCompare02/test.desc | 2 +- jbmc/regression/jbmc-strings/StringCompare03/test.desc | 2 +- jbmc/regression/jbmc-strings/StringCompare04/test.desc | 2 +- jbmc/regression/jbmc-strings/StringCompare05/test.desc | 2 +- .../jbmc-strings/StringConcat/test_buffer_det.desc | 2 +- .../StringConcat/test_buffer_nondet_loop.desc | 2 +- .../StringConcat/test_buffer_nondet_loop2.desc | 2 +- .../StringConcat/test_buffer_nondet_loop3.desc | 2 +- .../StringConcat/test_buffer_nondet_loop4.desc | 2 +- .../StringConcat/test_buffer_nondet_loop5.desc | 2 +- .../StringConcat/test_char_buffer_det.desc | 2 +- .../StringConcat/test_char_buffer_det_loop.desc | 2 +- .../StringConcat/test_char_buffer_det_loop2.desc | 2 +- .../jbmc-strings/StringConcat/test_string_det.desc | 2 +- .../jbmc-strings/StringConcat/test_string_nondet.desc | 2 +- .../jbmc-strings/StringConcat_StringII/test.desc | 2 +- .../jbmc-strings/StringConcat_StringII/test_fail.desc | 2 +- .../jbmc-strings/StringConcatenation01/test.desc | 2 +- .../jbmc-strings/StringConcatenation02/test.desc | 2 +- .../jbmc-strings/StringConcatenation03/test.desc | 2 +- .../jbmc-strings/StringConcatenation04/test.desc | 2 +- .../jbmc-strings/StringConstructors01/test.desc | 2 +- .../jbmc-strings/StringConstructors02/test.desc | 2 +- .../jbmc-strings/StringConstructors03/test.desc | 2 +- .../jbmc-strings/StringConstructors04/test.desc | 2 +- .../jbmc-strings/StringConstructors05/test.desc | 2 +- .../regression/jbmc-strings/StringContains01/test.desc | 2 +- .../regression/jbmc-strings/StringContains02/test.desc | 2 +- .../regression/jbmc-strings/StringContains03/test.desc | 2 +- .../jbmc-strings/StringDependencies/test.desc | 2 +- jbmc/regression/jbmc-strings/StringEquals/test.desc | 2 +- .../jbmc-strings/StringEquals/test_verify.desc | 2 +- .../StringEquals/test_verify_non_null.desc | 2 +- .../jbmc-strings/StringIndexMethods01/test.desc | 2 +- .../jbmc-strings/StringIndexMethods02/test.desc | 2 +- .../jbmc-strings/StringIndexMethods03/test.desc | 2 +- .../jbmc-strings/StringIndexMethods04/test.desc | 2 +- .../jbmc-strings/StringIndexMethods04/test_bug.desc | 2 +- .../jbmc-strings/StringIndexMethods05/test.desc | 2 +- jbmc/regression/jbmc-strings/StringIndexOf/test.desc | 2 +- jbmc/regression/jbmc-strings/StringIndexOf/test2.desc | 2 +- .../jbmc-strings/StringIndexOf/test_thorough.desc | 2 +- .../jbmc-strings/StringLastIndexOf/test.desc | 2 +- .../jbmc-strings/StringMiscellaneous01/test.desc | 2 +- .../jbmc-strings/StringMiscellaneous02/test.desc | 2 +- .../jbmc-strings/StringMiscellaneous03/test.desc | 2 +- .../jbmc-strings/StringMiscellaneous04/test.desc | 2 +- .../regression/jbmc-strings/StringStartEnd01/test.desc | 2 +- .../regression/jbmc-strings/StringStartEnd02/test.desc | 2 +- .../regression/jbmc-strings/StringStartEnd03/test.desc | 2 +- jbmc/regression/jbmc-strings/StringSubstring/test.desc | 2 +- .../jbmc-strings/StringSubstring/test_fail.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf01/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf02/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf03/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf04/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf05/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf06/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf07/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf08/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf09/test.desc | 2 +- jbmc/regression/jbmc-strings/StringValueOf10/test.desc | 2 +- jbmc/regression/jbmc-strings/SubString01/test.desc | 2 +- jbmc/regression/jbmc-strings/SubString02/test.desc | 2 +- jbmc/regression/jbmc-strings/SubString03/test.desc | 2 +- jbmc/regression/jbmc-strings/TokenTest01/test.desc | 2 +- jbmc/regression/jbmc-strings/TokenTest02/test.desc | 2 +- jbmc/regression/jbmc-strings/Validate01/test.desc | 2 +- jbmc/regression/jbmc-strings/Validate02/test.desc | 2 +- .../jbmc-strings/VerifStringLastIndexOf/test.desc | 2 +- .../regression/jbmc-strings/bug-test-gen-095/test.desc | 2 +- .../jbmc-strings/bug-test-gen-119-2/test.desc | 2 +- .../regression/jbmc-strings/bug-test-gen-119/test.desc | 2 +- jbmc/regression/jbmc-strings/instanceof/test.desc | 2 +- .../regression/jbmc-strings/java_append_char/test.desc | 2 +- jbmc/regression/jbmc-strings/java_append_int/test.desc | 2 +- .../jbmc-strings/java_append_object/test.desc | 2 +- .../jbmc-strings/java_char_array_init/test.desc | 2 +- jbmc/regression/jbmc-strings/java_char_at/test.desc | 2 +- jbmc/regression/jbmc-strings/java_compare/test.desc | 2 +- jbmc/regression/jbmc-strings/java_concat/test.desc | 2 +- jbmc/regression/jbmc-strings/java_delete/test.desc | 2 +- jbmc/regression/jbmc-strings/java_easychair/test.desc | 2 +- jbmc/regression/jbmc-strings/java_empty/test.desc | 2 +- .../regression/jbmc-strings/java_insert_char/test.desc | 2 +- jbmc/regression/jbmc-strings/java_insert_int/test.desc | 2 +- jbmc/regression/jbmc-strings/long_string/test.desc | 2 +- .../jbmc-strings/max-length-generic-array/test.desc | 2 +- .../max-length-generic-array/test_gen.desc | 2 +- jbmc/regression/jbmc-strings/max-length/test1.desc | 2 +- jbmc/regression/jbmc-strings/max-length/test2.desc | 2 +- jbmc/regression/jbmc-strings/max-length/test3.desc | 2 +- jbmc/regression/jbmc-strings/max-length/test4.desc | 4 ++-- .../strings-smoke-tests/java_append_char/test.desc | 2 +- .../strings-smoke-tests/java_append_int/test.desc | 2 +- .../strings-smoke-tests/java_append_string/test.desc | 2 +- .../java_append_string/test_substring.desc | 2 +- .../regression/strings-smoke-tests/java_case/test.desc | 2 +- .../strings-smoke-tests/java_char_array/test.desc | 2 +- .../strings-smoke-tests/java_char_at/test.desc | 2 +- .../strings-smoke-tests/java_code_point/test.desc | 2 +- .../strings-smoke-tests/java_contains/test.desc | 2 +- .../java_contains/test_string_printable.desc | 2 +- .../strings-smoke-tests/java_delete_char_at/test.desc | 2 +- .../strings-smoke-tests/java_endswith/test.desc | 2 +- .../strings-smoke-tests/java_equal/test.desc | 2 +- .../strings-smoke-tests/java_equal/test_2.desc | 2 +- .../strings-smoke-tests/java_float/test.desc | 2 +- .../strings-smoke-tests/java_format/test.desc | 2 +- .../strings-smoke-tests/java_format2/test.desc | 2 +- .../strings-smoke-tests/java_format3/test.desc | 2 +- .../strings-smoke-tests/java_format4/test.desc | 2 +- .../strings-smoke-tests/java_format5/test.desc | 2 +- .../strings-smoke-tests/java_hash_code/test.desc | 2 +- jbmc/regression/strings-smoke-tests/java_if/test.desc | 2 +- .../strings-smoke-tests/java_index_of/test.desc | 2 +- .../strings-smoke-tests/java_index_of2/test.desc | 2 +- .../strings-smoke-tests/java_index_of_char/test.desc | 2 +- .../strings-smoke-tests/java_insert_char/test.desc | 2 +- .../java_insert_char_array/test.desc | 2 +- .../strings-smoke-tests/java_insert_multiple/test.desc | 2 +- .../strings-smoke-tests/java_insert_string/test.desc | 2 +- .../strings-smoke-tests/java_int_to_string/test1.desc | 2 +- .../strings-smoke-tests/java_int_to_string/test2.desc | 2 +- .../java_int_to_string/test2_bug.desc | 2 +- .../strings-smoke-tests/java_int_to_string/test3.desc | 2 +- .../strings-smoke-tests/java_int_to_string/test4.desc | 2 +- .../strings-smoke-tests/java_int_to_string/test5.desc | 2 +- .../java_int_to_string_knownbug/test.desc | 2 +- .../java_int_to_string_with_radix/test_binary1.desc | 2 +- .../java_int_to_string_with_radix/test_binary2.desc | 2 +- .../java_int_to_string_with_radix/test_binary3.desc | 2 +- .../java_int_to_string_with_radix/test_decimal.desc | 2 +- .../java_int_to_string_with_radix/test_hex1.desc | 2 +- .../java_int_to_string_with_radix/test_hex2.desc | 2 +- .../java_int_to_string_with_radix/test_hex3.desc | 2 +- .../java_int_to_string_with_radix/test_octal1.desc | 2 +- .../java_int_to_string_with_radix/test_octal2.desc | 2 +- .../java_int_to_string_with_radix/test_octal3.desc | 2 +- .../test_binary.desc | 2 +- .../test_hex.desc | 2 +- .../test_octal.desc | 2 +- .../strings-smoke-tests/java_intern/test.desc | 2 +- .../strings-smoke-tests/java_last_index_of/test.desc | 2 +- .../strings-smoke-tests/java_last_index_of2/test.desc | 2 +- .../java_last_index_of_char/test.desc | 2 +- .../strings-smoke-tests/java_length/test.desc | 2 +- .../strings-smoke-tests/java_length2/test.desc | 2 +- .../strings-smoke-tests/java_long_to_string/test1.desc | 2 +- .../strings-smoke-tests/java_long_to_string/test2.desc | 2 +- .../strings-smoke-tests/java_long_to_string/test3.desc | 2 +- .../strings-smoke-tests/java_long_to_string/test4.desc | 2 +- .../strings-smoke-tests/java_long_to_string/test5.desc | 2 +- .../java_long_to_string_with_radix/test_binary1.desc | 2 +- .../java_long_to_string_with_radix/test_binary2.desc | 2 +- .../java_long_to_string_with_radix/test_binary3.desc | 2 +- .../java_long_to_string_with_radix/test_decimal.desc | 2 +- .../java_long_to_string_with_radix/test_hex1.desc | 2 +- .../java_long_to_string_with_radix/test_hex2.desc | 2 +- .../java_long_to_string_with_radix/test_hex3.desc | 2 +- .../java_long_to_string_with_radix/test_octal1.desc | 2 +- .../java_long_to_string_with_radix/test_octal2.desc | 2 +- .../java_long_to_string_with_radix/test_octal3.desc | 2 +- .../strings-smoke-tests/java_parseint/test1.desc | 2 +- .../strings-smoke-tests/java_parseint/test2.desc | 2 +- .../strings-smoke-tests/java_parseint/test3.desc | 2 +- .../java_parseint_knownbug/test.desc | 2 +- .../java_parseint_with_radix/test1.desc | 2 +- .../java_parseint_with_radix/test2.desc | 2 +- .../java_parseint_with_radix/test3.desc | 2 +- .../java_parseint_with_radix/test4.desc | 2 +- .../java_parseint_with_radix/test5.desc | 2 +- .../java_parseint_with_radix/test6.desc | 2 +- .../java_parseint_with_radix_knownbug/test.desc | 2 +- .../java_parselong/test_binary_min.desc | 2 +- .../java_parselong/test_decimal_max.desc | 2 +- .../java_parselong/test_decimal_min.desc | 2 +- .../strings-smoke-tests/java_parselong/test_hex.desc | 2 +- .../strings-smoke-tests/java_parselong/test_octal.desc | 2 +- .../strings-smoke-tests/java_replace/test.desc | 2 +- .../strings-smoke-tests/java_replace_char/test.desc | 2 +- .../strings-smoke-tests/java_set_char_at/test.desc | 2 +- .../strings-smoke-tests/java_set_length/test.desc | 2 +- .../strings-smoke-tests/java_starts_with/test.desc | 2 +- .../java_string_builder_length/test.desc | 2 +- .../java_string_printable/test.desc | 2 +- .../java_string_printable/test_char.desc | 2 +- .../strings-smoke-tests/java_subsequence/test.desc | 2 +- .../strings-smoke-tests/java_substring/test.desc | 2 +- .../regression/strings-smoke-tests/java_trim/test.desc | 2 +- .../strings-smoke-tests/java_value_of_float/test.desc | 2 +- .../java_value_of_float_2/test.desc | 2 +- .../java_value_of_float_3/test.desc | 2 +- .../java_value_of_float_4/test.desc | 2 +- .../java_value_of_float_5/test.desc | 2 +- .../strings-smoke-tests/java_value_of_long/test.desc | 2 +- .../max_input_length/MemberTest.desc | 8 -------- .../max_input_length/MemberTest2.desc | 8 -------- .../strings-smoke-tests/max_input_length/test1.desc | 2 +- .../strings-smoke-tests/max_input_length/test2.desc | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 10 +++------- jbmc/src/jbmc/jbmc_parse_options.h | 1 - 236 files changed, 236 insertions(+), 257 deletions(-) delete mode 100644 jbmc/regression/strings-smoke-tests/max_input_length/MemberTest.desc delete mode 100644 jbmc/regression/strings-smoke-tests/max_input_length/MemberTest2.desc diff --git a/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc b/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc index 30ce2644914..c121b97aa19 100644 --- a/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc +++ b/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion at file test.java line 8 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/RegexMatches01/test.desc b/jbmc/regression/jbmc-strings/RegexMatches01/test.desc index 4a95eb71ab0..893f7683604 100644 --- a/jbmc/regression/jbmc-strings/RegexMatches01/test.desc +++ b/jbmc/regression/jbmc-strings/RegexMatches01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches01.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/RegexMatches02/test.desc b/jbmc/regression/jbmc-strings/RegexMatches02/test.desc index 9b754d1a449..519e130da29 100644 --- a/jbmc/regression/jbmc-strings/RegexMatches02/test.desc +++ b/jbmc/regression/jbmc-strings/RegexMatches02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches02.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc b/jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc index 2d24db23d16..8921222791a 100644 --- a/jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc +++ b/jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc b/jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc index 2caa11a3221..66a3783f61f 100644 --- a/jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc +++ b/jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/RegexSubstitution03/test.desc b/jbmc/regression/jbmc-strings/RegexSubstitution03/test.desc index 9f141b34217..f1c9f84ac34 100644 --- a/jbmc/regression/jbmc-strings/RegexSubstitution03/test.desc +++ b/jbmc/regression/jbmc-strings/RegexSubstitution03/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StartsWith/test.desc b/jbmc/regression/jbmc-strings/StartsWith/test.desc index 13bacc2677a..c6eb33fee3a 100644 --- a/jbmc/regression/jbmc-strings/StartsWith/test.desc +++ b/jbmc/regression/jbmc-strings/StartsWith/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-input-length 10 --unwind 10 --function Test.check +--refine-strings --max-nondet-string-length 10 --unwind 10 --function Test.check ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 31 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StartsWith/test_det.desc b/jbmc/regression/jbmc-strings/StartsWith/test_det.desc index bb9017ada0d..e326403b0dd 100644 --- a/jbmc/regression/jbmc-strings/StartsWith/test_det.desc +++ b/jbmc/regression/jbmc-strings/StartsWith/test_det.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkDet +--refine-strings --max-nondet-string-length 100 --unwind 10 --function Test.checkDet ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 41 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc index b02b55f1509..8dde2ad0501 100644 --- a/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc +++ b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkNonDet +--refine-strings --max-nondet-string-length 100 --unwind 10 --function Test.checkNonDet ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 66 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods01/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods01/test.desc index 35c0f3a7f1e..6971683a810 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods01/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods01/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods02/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods02/test.desc index 70e90e4115a..432054fa5d3 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods02/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods02/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods03/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods03/test.desc index 712044431a5..f3e90dc8412 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods03/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods03/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods04/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods04/test.desc index ee66116b0fa..4bc890602f2 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods04/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods04/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods05/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods05/test.desc index 41218e79141..7e721f661d2 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods05/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods05/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods05.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 12 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StaticCharMethods06/test.desc b/jbmc/regression/jbmc-strings/StaticCharMethods06/test.desc index b0047376ea1..623f468e7ca 100644 --- a/jbmc/regression/jbmc-strings/StaticCharMethods06/test.desc +++ b/jbmc/regression/jbmc-strings/StaticCharMethods06/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods06.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringArray/test.desc b/jbmc/regression/jbmc-strings/StringArray/test.desc index 84195a84d46..b5486ffc5ca 100644 --- a/jbmc/regression/jbmc-strings/StringArray/test.desc +++ b/jbmc/regression/jbmc-strings/StringArray/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check --string-max-input-length 1000 +--refine-strings --function Test.check --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 20.* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend01/test.desc index 925b862d11e..f5aa2ba8a9a 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderAppend01/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderAppend01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend02/test.desc index d0ef683f373..1d6669f8c64 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderAppend02/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderAppend02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc index 12d6f321534..15678d7ba2a 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderCapLen02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderCapLen02/test.desc index 68183ab0c8b..15404d4345b 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderCapLen02/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderCapLen02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderCapLen03/test.desc b/jbmc/regression/jbmc-strings/StringBuilderCapLen03/test.desc index 98f5aa74306..089beb330f3 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderCapLen03/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderCapLen03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderCapLen04/test.desc b/jbmc/regression/jbmc-strings/StringBuilderCapLen04/test.desc index 2bf31910709..10886f1aee8 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderCapLen04/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderCapLen04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc index df8aa84cc74..f83ae816756 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars01.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars02/test.desc index 991d4cca0eb..050ef1d6783 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars02/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars02.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars03/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars03/test.desc index 6ec91ba3f69..f6a7b2f9996 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars03/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars03.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc index 802a60269ec..89c4e5cc692 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars04.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc index fdb12721623..e64e863a9e1 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars05.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars06/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars06/test.desc index fbb6f1bb87d..bdd0542b78b 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars06/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars06/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars06.class ---refine-strings --string-max-length 1000 --unwind 100 +--refine-strings --max-nondet-string-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc index 39bcec0b205..4d1a4b718e6 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc index 889460297ea..c69c5c09e4a 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc index 5c347f7792a..279438386e2 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc index 576410049d8..12bcf3efcfc 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc index 934b4de8579..c4f6cd393ef 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringCompare01/test.desc b/jbmc/regression/jbmc-strings/StringCompare01/test.desc index 5e60d31b865..a406a47f364 100644 --- a/jbmc/regression/jbmc-strings/StringCompare01/test.desc +++ b/jbmc/regression/jbmc-strings/StringCompare01/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringCompare02/test.desc b/jbmc/regression/jbmc-strings/StringCompare02/test.desc index 2970a511914..601f109346f 100644 --- a/jbmc/regression/jbmc-strings/StringCompare02/test.desc +++ b/jbmc/regression/jbmc-strings/StringCompare02/test.desc @@ -1,6 +1,6 @@ CORE StringCompare02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 12 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringCompare03/test.desc b/jbmc/regression/jbmc-strings/StringCompare03/test.desc index 15b7f91b1fe..f6e564d55be 100644 --- a/jbmc/regression/jbmc-strings/StringCompare03/test.desc +++ b/jbmc/regression/jbmc-strings/StringCompare03/test.desc @@ -1,6 +1,6 @@ CORE StringCompare03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 12 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringCompare04/test.desc b/jbmc/regression/jbmc-strings/StringCompare04/test.desc index 176142e064e..1aad9b69926 100644 --- a/jbmc/regression/jbmc-strings/StringCompare04/test.desc +++ b/jbmc/regression/jbmc-strings/StringCompare04/test.desc @@ -1,6 +1,6 @@ CORE StringCompare04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringCompare05/test.desc b/jbmc/regression/jbmc-strings/StringCompare05/test.desc index a182fecf008..5beee5d6e5d 100644 --- a/jbmc/regression/jbmc-strings/StringCompare05/test.desc +++ b/jbmc/regression/jbmc-strings/StringCompare05/test.desc @@ -1,6 +1,6 @@ CORE StringCompare05.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc index 5e66ea01921..4a2799d0b59 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferDet --depth 10000 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.bufferDet --depth 10000 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc index 75f57525803..269c67de0dd 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1' +--refine-strings --max-nondet-string-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1' ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc index 63814912cda..4f2a6ee6723 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc index ac8124eb0b1..621754199db 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc index fbc95cd4df6..bb764a6e617 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1' +--refine-strings --max-nondet-string-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1' ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc index 7022df3ff8d..03b7cad4134 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc index 8821fadda98..bb54862bbca 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDet --depth 10000 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.charBufferDet --depth 10000 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc index 9c3643b0770..1483b826fc6 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc index eee09bad0eb..9f8ba670529 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_string_det.desc b/jbmc/regression/jbmc-strings/StringConcat/test_string_det.desc index d3a8f79fdc1..aaa9125f5fa 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_string_det.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_string_det.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringDet --depth 10000 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.stringDet --depth 10000 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc b/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc index cfce92f3210..95a65ff37e3 100644 --- a/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc +++ b/jbmc/regression/jbmc-strings/StringConcat/test_string_nondet.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10 +--refine-strings --max-nondet-string-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc index 79b0e5636c5..e9d353e63b3 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 ---refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess +--refine-strings --max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 23 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc index 47e0399c5b2..14426fc336a 100644 --- a/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc +++ b/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 10000 --verbosity 10 --function Test.testFail +--refine-strings --max-nondet-string-length 10000 --verbosity 10 --function Test.testFail ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 38 .*: FAILURE diff --git a/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc index 09414c5a3f6..abfffd6ed76 100644 --- a/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc +++ b/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringConcatenation02/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation02/test.desc index 90c299fea1a..c2e106ccdcf 100644 --- a/jbmc/regression/jbmc-strings/StringConcatenation02/test.desc +++ b/jbmc/regression/jbmc-strings/StringConcatenation02/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcatenation03/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation03/test.desc index 2dd24800903..3f0090e04cc 100644 --- a/jbmc/regression/jbmc-strings/StringConcatenation03/test.desc +++ b/jbmc/regression/jbmc-strings/StringConcatenation03/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConcatenation04/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation04/test.desc index 5fbdea80b8a..2663711e7c2 100644 --- a/jbmc/regression/jbmc-strings/StringConcatenation04/test.desc +++ b/jbmc/regression/jbmc-strings/StringConcatenation04/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 8 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringConstructors01/test.desc b/jbmc/regression/jbmc-strings/StringConstructors01/test.desc index 6c3fdfb7af8..87c1ea9a057 100644 --- a/jbmc/regression/jbmc-strings/StringConstructors01/test.desc +++ b/jbmc/regression/jbmc-strings/StringConstructors01/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringConstructors02/test.desc b/jbmc/regression/jbmc-strings/StringConstructors02/test.desc index f39f6dbcf25..ce12d8f4b62 100644 --- a/jbmc/regression/jbmc-strings/StringConstructors02/test.desc +++ b/jbmc/regression/jbmc-strings/StringConstructors02/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConstructors03/test.desc b/jbmc/regression/jbmc-strings/StringConstructors03/test.desc index 3df88975a3e..9f614290566 100644 --- a/jbmc/regression/jbmc-strings/StringConstructors03/test.desc +++ b/jbmc/regression/jbmc-strings/StringConstructors03/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConstructors04/test.desc b/jbmc/regression/jbmc-strings/StringConstructors04/test.desc index 9e889d73812..cbeeee9a64e 100644 --- a/jbmc/regression/jbmc-strings/StringConstructors04/test.desc +++ b/jbmc/regression/jbmc-strings/StringConstructors04/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringConstructors05/test.desc b/jbmc/regression/jbmc-strings/StringConstructors05/test.desc index 80b0ee57307..b5cc7327484 100644 --- a/jbmc/regression/jbmc-strings/StringConstructors05/test.desc +++ b/jbmc/regression/jbmc-strings/StringConstructors05/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors05.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringContains01/test.desc b/jbmc/regression/jbmc-strings/StringContains01/test.desc index 6a299037d6f..c01c85c1b91 100644 --- a/jbmc/regression/jbmc-strings/StringContains01/test.desc +++ b/jbmc/regression/jbmc-strings/StringContains01/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringContains02/test.desc b/jbmc/regression/jbmc-strings/StringContains02/test.desc index 6a299037d6f..c01c85c1b91 100644 --- a/jbmc/regression/jbmc-strings/StringContains02/test.desc +++ b/jbmc/regression/jbmc-strings/StringContains02/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringContains03/test.desc b/jbmc/regression/jbmc-strings/StringContains03/test.desc index b2842da00f2..ae7d2f9156b 100644 --- a/jbmc/regression/jbmc-strings/StringContains03/test.desc +++ b/jbmc/regression/jbmc-strings/StringContains03/test.desc @@ -7,5 +7,5 @@ Test.class file Test.java line 20 .*: FAILURE$ -- -- ---string-max-length is not used on purpose, because this tests the behaviour +--max-nondet-string-length is not used on purpose, because this tests the behaviour of string refinement on very large strings. diff --git a/jbmc/regression/jbmc-strings/StringDependencies/test.desc b/jbmc/regression/jbmc-strings/StringDependencies/test.desc index 9a1485143a8..f0e9adec454 100644 --- a/jbmc/regression/jbmc-strings/StringDependencies/test.desc +++ b/jbmc/regression/jbmc-strings/StringDependencies/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 --function Test.test +--refine-strings --max-nondet-string-length 100 --verbosity 10 --function Test.test ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 20 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringEquals/test.desc b/jbmc/regression/jbmc-strings/StringEquals/test.desc index 1f90caa955f..2f620b4d072 100644 --- a/jbmc/regression/jbmc-strings/StringEquals/test.desc +++ b/jbmc/regression/jbmc-strings/StringEquals/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 40 --function Test.check +--refine-strings --max-nondet-string-length 40 --function Test.check ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 9 .* SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc index 01bf846bfdc..e95fcff8f79 100644 --- a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc +++ b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc @@ -1,6 +1,6 @@ KNOWNBUG Test.class ---refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --throw-runtime-exceptions +--refine-strings --max-nondet-string-length 5 --unwind 10 --function Test.verify --throw-runtime-exceptions ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 60 .* 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 5e62a087b67..1511d344ee9 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 ---refine-strings --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull +--refine-strings --max-nondet-string-length 20 --unwind 30 --function Test.verifyNonNull ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 48 .* SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods01/test.desc b/jbmc/regression/jbmc-strings/StringIndexMethods01/test.desc index 96c8fb19994..f4e91b6df3b 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods01/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods01/test.desc @@ -1,6 +1,6 @@ THOROUGH StringIndexMethods01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods02/test.desc b/jbmc/regression/jbmc-strings/StringIndexMethods02/test.desc index 69250ebae1d..6f6ba479072 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods02/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods02/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods03/test.desc b/jbmc/regression/jbmc-strings/StringIndexMethods03/test.desc index ce9b8e5a339..a548cde1fb5 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods03/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods03/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods04/test.desc b/jbmc/regression/jbmc-strings/StringIndexMethods04/test.desc index f63d2152f09..6fbbb2d267a 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods04/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods04/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods04/test_bug.desc b/jbmc/regression/jbmc-strings/StringIndexMethods04/test_bug.desc index ce351fe8d81..2b231310176 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods04/test_bug.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods04/test_bug.desc @@ -1,6 +1,6 @@ KNOWNBUG StringIndexMethods04.class ---refine-strings --string-max-length 1000 --function StringIndexMethods04.mainBug +--refine-strings --max-nondet-string-length 1000 --function StringIndexMethods04.mainBug ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringIndexMethods05/test.desc b/jbmc/regression/jbmc-strings/StringIndexMethods05/test.desc index 243c43e965a..3fe1f45ff92 100644 --- a/jbmc/regression/jbmc-strings/StringIndexMethods05/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexMethods05/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods05.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringIndexOf/test.desc b/jbmc/regression/jbmc-strings/StringIndexOf/test.desc index 74cda5ee46b..73dfe352ef4 100644 --- a/jbmc/regression/jbmc-strings/StringIndexOf/test.desc +++ b/jbmc/regression/jbmc-strings/StringIndexOf/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --string-max-length 100 --java-assume-inputs-non-null +--refine-strings --function Test.check --unwind 4 --max-nondet-string-length 3 --java-assume-inputs-non-null ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringIndexOf/test2.desc b/jbmc/regression/jbmc-strings/StringIndexOf/test2.desc index 3bb7fe6b973..9a8a462907f 100644 --- a/jbmc/regression/jbmc-strings/StringIndexOf/test2.desc +++ b/jbmc/regression/jbmc-strings/StringIndexOf/test2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +--refine-strings --function Test.check2 --unwind 10 --max-nondet-string-length 10 --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 35 .* SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc b/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc index 8e05fa5bfa7..d9f049381de 100644 --- a/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc +++ b/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc @@ -1,6 +1,6 @@ THOROUGH Test.class ---refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +--refine-strings --function Test.check --unwind 10 --max-nondet-string-length 10 --java-assume-inputs-non-null ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc b/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc index 2e18576f085..dd4034bdeb0 100644 --- a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc +++ b/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.check --refine-strings --string-max-input-length 100 +--function Test.check --refine-strings --max-nondet-string-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 11 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc index 6443a3f37d8..bafc6423241 100644 --- a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc +++ b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous01.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous02/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous02/test.desc index 987299cb4af..9e8fe290104 100644 --- a/jbmc/regression/jbmc-strings/StringMiscellaneous02/test.desc +++ b/jbmc/regression/jbmc-strings/StringMiscellaneous02/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous02.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous03/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous03/test.desc index 7a20ece6152..48786693505 100644 --- a/jbmc/regression/jbmc-strings/StringMiscellaneous03/test.desc +++ b/jbmc/regression/jbmc-strings/StringMiscellaneous03/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous03.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 11 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc index 5657433d8c7..978c91c3679 100644 --- a/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc +++ b/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous04.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringStartEnd01/test.desc b/jbmc/regression/jbmc-strings/StringStartEnd01/test.desc index 21181368d56..09647d38de4 100644 --- a/jbmc/regression/jbmc-strings/StringStartEnd01/test.desc +++ b/jbmc/regression/jbmc-strings/StringStartEnd01/test.desc @@ -1,6 +1,6 @@ THOROUGH StringStartEnd01.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringStartEnd02/test.desc b/jbmc/regression/jbmc-strings/StringStartEnd02/test.desc index deddbb5b902..6cddc1e942b 100644 --- a/jbmc/regression/jbmc-strings/StringStartEnd02/test.desc +++ b/jbmc/regression/jbmc-strings/StringStartEnd02/test.desc @@ -1,6 +1,6 @@ CORE StringStartEnd02.class ---refine-strings --unwind 30 --string-max-length 1000 +--refine-strings --unwind 30 --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 13 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringStartEnd03/test.desc b/jbmc/regression/jbmc-strings/StringStartEnd03/test.desc index ad05b3a1904..9521d5e8824 100644 --- a/jbmc/regression/jbmc-strings/StringStartEnd03/test.desc +++ b/jbmc/regression/jbmc-strings/StringStartEnd03/test.desc @@ -1,6 +1,6 @@ THOROUGH StringStartEnd03.class ---refine-strings --string-max-length 1000 --unwind 15 +--refine-strings --max-nondet-string-length 1000 --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 13 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringSubstring/test.desc b/jbmc/regression/jbmc-strings/StringSubstring/test.desc index 651248f8a5c..9442dd4f3fb 100644 --- a/jbmc/regression/jbmc-strings/StringSubstring/test.desc +++ b/jbmc/regression/jbmc-strings/StringSubstring/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --unwind 10 --string-max-input-length 6 --function Test.testSuccess +--refine-strings --unwind 10 --max-nondet-string-length 6 --function Test.testSuccess ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 21.*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringSubstring/test_fail.desc b/jbmc/regression/jbmc-strings/StringSubstring/test_fail.desc index aa7239263fd..926665b755f 100644 --- a/jbmc/regression/jbmc-strings/StringSubstring/test_fail.desc +++ b/jbmc/regression/jbmc-strings/StringSubstring/test_fail.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --unwind 10 --string-max-input-length 6 --function Test.testFail +--refine-strings --unwind 10 --max-nondet-string-length 6 --function Test.testFail ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 37 .*: FAILURE diff --git a/jbmc/regression/jbmc-strings/StringValueOf01/test.desc b/jbmc/regression/jbmc-strings/StringValueOf01/test.desc index 19dc04f76f3..15ee3457a75 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf01/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf01/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf02/test.desc b/jbmc/regression/jbmc-strings/StringValueOf02/test.desc index 3640d830371..6d3cf43757a 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf02/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf02/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf03/test.desc b/jbmc/regression/jbmc-strings/StringValueOf03/test.desc index 788c99b840c..b5cf18c50b6 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf03/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf03/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf04/test.desc b/jbmc/regression/jbmc-strings/StringValueOf04/test.desc index 1628779f989..2ac0ffa2b07 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf04/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf04/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf04.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf05/test.desc b/jbmc/regression/jbmc-strings/StringValueOf05/test.desc index 281e1787b98..c9a2f823daa 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf05/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf05/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf05.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf06/test.desc b/jbmc/regression/jbmc-strings/StringValueOf06/test.desc index 23d219415d2..40131b40052 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf06/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf06/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf06.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf07/test.desc b/jbmc/regression/jbmc-strings/StringValueOf07/test.desc index af73181177d..d67391c80c1 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf07/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf07/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf07.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 8 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf08/test.desc b/jbmc/regression/jbmc-strings/StringValueOf08/test.desc index 3746e46471f..de8cdd190c5 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf08/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf08/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf08.class ---refine-strings --string-max-length 100 +--refine-strings --max-nondet-string-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf09/test.desc b/jbmc/regression/jbmc-strings/StringValueOf09/test.desc index 583f9fde885..a18810f2eec 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf09/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf09/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf09.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf10/test.desc b/jbmc/regression/jbmc-strings/StringValueOf10/test.desc index 90a38f97794..fc2856cf8e1 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf10/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf10/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf10.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/SubString01/test.desc b/jbmc/regression/jbmc-strings/SubString01/test.desc index f77f04ee2c7..a3ffbe6f49e 100644 --- a/jbmc/regression/jbmc-strings/SubString01/test.desc +++ b/jbmc/regression/jbmc-strings/SubString01/test.desc @@ -1,6 +1,6 @@ CORE SubString01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/SubString02/test.desc b/jbmc/regression/jbmc-strings/SubString02/test.desc index c487dd9ab17..f1ec8539fc0 100644 --- a/jbmc/regression/jbmc-strings/SubString02/test.desc +++ b/jbmc/regression/jbmc-strings/SubString02/test.desc @@ -1,6 +1,6 @@ CORE SubString02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/SubString03/test.desc b/jbmc/regression/jbmc-strings/SubString03/test.desc index 48075842027..af4c645189e 100644 --- a/jbmc/regression/jbmc-strings/SubString03/test.desc +++ b/jbmc/regression/jbmc-strings/SubString03/test.desc @@ -1,6 +1,6 @@ CORE SubString03.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/TokenTest01/test.desc b/jbmc/regression/jbmc-strings/TokenTest01/test.desc index 921e312b85e..9cc2d19129b 100644 --- a/jbmc/regression/jbmc-strings/TokenTest01/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest01/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest01.class ---refine-strings --string-max-length 1000 --unwind 30 +--refine-strings --max-nondet-string-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/TokenTest02/test.desc b/jbmc/regression/jbmc-strings/TokenTest02/test.desc index 0cc1d6a0d26..2a9160121e4 100644 --- a/jbmc/regression/jbmc-strings/TokenTest02/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest02/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest02.class ---refine-strings --string-max-length 1000 --unwind 15 +--refine-strings --max-nondet-string-length 1000 --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/Validate01/test.desc b/jbmc/regression/jbmc-strings/Validate01/test.desc index 7893ef03d1b..9701f10b752 100644 --- a/jbmc/regression/jbmc-strings/Validate01/test.desc +++ b/jbmc/regression/jbmc-strings/Validate01/test.desc @@ -1,6 +1,6 @@ FUTURE Validate01.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/Validate02/test.desc b/jbmc/regression/jbmc-strings/Validate02/test.desc index 36385610844..582d8914f2b 100644 --- a/jbmc/regression/jbmc-strings/Validate02/test.desc +++ b/jbmc/regression/jbmc-strings/Validate02/test.desc @@ -1,6 +1,6 @@ FUTURE Validate02.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc b/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc index 5f238b0d996..ad1f09e57cc 100644 --- a/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc +++ b/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc @@ -1,6 +1,6 @@ THOROUGH Test.class ---function Test.check --refine-strings --string-max-length 50 --unwind 50 --java-assume-inputs-non-null +--function Test.check --refine-strings --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 32 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc index 9c690be3298..ab1b899c87c 100644 --- a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc +++ b/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ \[.*assertion\.1\] .* line 8 .* FAILURE 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 0f52c235798..346db3a4969 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 ---refine-strings --string-max-length 1000 --function StringValueOfLong.main +--refine-strings --max-nondet-string-length 1000 --function StringValueOfLong.main ^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 c0f9b9e2d82..7ed3512ad88 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 ---refine-strings --string-max-length 1000 --function StringValueOfBool.main +--refine-strings --max-nondet-string-length 1000 --function StringValueOfBool.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/instanceof/test.desc b/jbmc/regression/jbmc-strings/instanceof/test.desc index 3c597735589..aec2c287d0f 100644 --- a/jbmc/regression/jbmc-strings/instanceof/test.desc +++ b/jbmc/regression/jbmc-strings/instanceof/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --string-max-length 1000 --function Test.check +--refine-strings --max-nondet-string-length 1000 --function Test.check ^EXIT=0$ ^SIGNAL=0$ assertion at file Test.java line 6 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/java_append_char/test.desc b/jbmc/regression/jbmc-strings/java_append_char/test.desc index 5eba917c237..2bade36e997 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 ---refine-strings --string-max-length 1000 --function test_append_char.main +--refine-strings --max-nondet-string-length 1000 --function test_append_char.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/java_append_int/test.desc b/jbmc/regression/jbmc-strings/java_append_int/test.desc index 8edf69c9fec..97b30f8d625 100644 --- a/jbmc/regression/jbmc-strings/java_append_int/test.desc +++ b/jbmc/regression/jbmc-strings/java_append_int/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test_append_int.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 9.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_append_object/test.desc b/jbmc/regression/jbmc-strings/java_append_object/test.desc index 2af06f2686a..267d66ad752 100644 --- a/jbmc/regression/jbmc-strings/java_append_object/test.desc +++ b/jbmc/regression/jbmc-strings/java_append_object/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test_append_object.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 15.* FAILURE$ 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 5ecb589e1f8..87bb13034c7 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 ---refine-strings --string-max-length 1000 --function test_init.main +--refine-strings --max-nondet-string-length 1000 --function test_init.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_init.java line 31 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/java_char_at/test.desc b/jbmc/regression/jbmc-strings/java_char_at/test.desc index 8507d50a8fb..9f9c3aafdd3 100644 --- a/jbmc/regression/jbmc-strings/java_char_at/test.desc +++ b/jbmc/regression/jbmc-strings/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings --string-max-length 1000 --function test_char_at.main +--refine-strings --max-nondet-string-length 1000 --function test_char_at.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 5.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_compare/test.desc b/jbmc/regression/jbmc-strings/java_compare/test.desc index 0d7310590bc..9f7f808c0d1 100644 --- a/jbmc/regression/jbmc-strings/java_compare/test.desc +++ b/jbmc/regression/jbmc-strings/java_compare/test.desc @@ -1,6 +1,6 @@ CORE test_compare.class ---refine-strings --string-max-length 1000 --function test_compare.main +--refine-strings --max-nondet-string-length 1000 --function test_compare.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_concat/test.desc b/jbmc/regression/jbmc-strings/java_concat/test.desc index b1d47ce246d..fc0727b5f19 100644 --- a/jbmc/regression/jbmc-strings/java_concat/test.desc +++ b/jbmc/regression/jbmc-strings/java_concat/test.desc @@ -1,6 +1,6 @@ CORE test_concat.class ---refine-strings --string-max-length 1000 --function test_concat.main +--refine-strings --max-nondet-string-length 1000 --function test_concat.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/java_delete/test.desc b/jbmc/regression/jbmc-strings/java_delete/test.desc index 44af4af9c68..1bda3525f59 100644 --- a/jbmc/regression/jbmc-strings/java_delete/test.desc +++ b/jbmc/regression/jbmc-strings/java_delete/test.desc @@ -1,6 +1,6 @@ CORE test_delete.class ---refine-strings --string-max-length 1000 --function test_delete.main +--refine-strings --max-nondet-string-length 1000 --function test_delete.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_easychair/test.desc b/jbmc/regression/jbmc-strings/java_easychair/test.desc index 079e02ddee2..307bd8f999a 100644 --- a/jbmc/regression/jbmc-strings/java_easychair/test.desc +++ b/jbmc/regression/jbmc-strings/java_easychair/test.desc @@ -1,6 +1,6 @@ THOROUGH easychair.class ---refine-strings --string-max-length 1000 +--refine-strings --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 30.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_empty/test.desc b/jbmc/regression/jbmc-strings/java_empty/test.desc index 32e54658d79..862273be077 100644 --- a/jbmc/regression/jbmc-strings/java_empty/test.desc +++ b/jbmc/regression/jbmc-strings/java_empty/test.desc @@ -1,6 +1,6 @@ CORE test_empty.class ---refine-strings --string-max-length 1000 --function test_empty.main +--refine-strings --max-nondet-string-length 1000 --function test_empty.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 6.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test.desc b/jbmc/regression/jbmc-strings/java_insert_char/test.desc index 7cd1cde2df7..33be88830c4 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 ---refine-strings --string-max-length 1000 --function test_insert_char.main +--refine-strings --max-nondet-string-length 1000 --function test_insert_char.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_insert_int/test.desc b/jbmc/regression/jbmc-strings/java_insert_int/test.desc index 3fa476250c1..972d6047361 100644 --- a/jbmc/regression/jbmc-strings/java_insert_int/test.desc +++ b/jbmc/regression/jbmc-strings/java_insert_int/test.desc @@ -1,6 +1,6 @@ CORE test_insert_int.class ---refine-strings --string-max-length 1000 --function test_insert_int.main +--refine-strings --max-nondet-string-length 1000 --function test_insert_int.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/long_string/test.desc b/jbmc/regression/jbmc-strings/long_string/test.desc index 7f5301726d3..52c31265c67 100644 --- a/jbmc/regression/jbmc-strings/long_string/test.desc +++ b/jbmc/regression/jbmc-strings/long_string/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check --string-max-input-length 2000000 +--refine-strings --function Test.check --max-nondet-string-length 2000000 ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 21 .* FAILURE diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc index abd5e382ff9..49cd4250995 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc +++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc @@ -1,6 +1,6 @@ CORE IntegerTests.class --refine-strings --string-max-length 100 --function IntegerTests.testMySet --cover location +-refine-strings --max-nondet-string-length 100 --function IntegerTests.testMySet --cover location ^EXIT=0$ ^SIGNAL=0$ coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc index 3f8a4ce6ea3..0384ec25547 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc +++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc @@ -1,6 +1,6 @@ CORE IntegerTests.class --refine-strings --string-max-length 100 --function IntegerTests.testMyGenSet --cover location +-refine-strings --max-nondet-string-length 100 --function IntegerTests.testMyGenSet --cover location ^EXIT=0$ ^SIGNAL=0$ coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED diff --git a/jbmc/regression/jbmc-strings/max-length/test1.desc b/jbmc/regression/jbmc-strings/max-length/test1.desc index db6b0190670..d2261e1929a 100644 --- a/jbmc/regression/jbmc-strings/max-length/test1.desc +++ b/jbmc/regression/jbmc-strings/max-length/test1.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength +--refine-strings --verbosity 10 --max-nondet-string-length 499999 --function Test.checkMaxInputLength ^EXIT=0$ ^SIGNAL=0$ assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS diff --git a/jbmc/regression/jbmc-strings/max-length/test2.desc b/jbmc/regression/jbmc-strings/max-length/test2.desc index b5f70b5658d..70dd2f1447e 100644 --- a/jbmc/regression/jbmc-strings/max-length/test2.desc +++ b/jbmc/regression/jbmc-strings/max-length/test2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength +--refine-strings --verbosity 10 --max-nondet-string-length 500000 --function Test.checkMaxInputLength ^EXIT=10$ ^SIGNAL=0$ assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE diff --git a/jbmc/regression/jbmc-strings/max-length/test3.desc b/jbmc/regression/jbmc-strings/max-length/test3.desc index f8e970cc618..77651489d05 100644 --- a/jbmc/regression/jbmc-strings/max-length/test3.desc +++ b/jbmc/regression/jbmc-strings/max-length/test3.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength +--refine-strings --verbosity 10 --max-nondet-string-length 4001 --function Test.checkMaxLength ^EXIT=10$ ^SIGNAL=0$ assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE diff --git a/jbmc/regression/jbmc-strings/max-length/test4.desc b/jbmc/regression/jbmc-strings/max-length/test4.desc index b1cdfc3d39c..516bad3c4f2 100644 --- a/jbmc/regression/jbmc-strings/max-length/test4.desc +++ b/jbmc/regression/jbmc-strings/max-length/test4.desc @@ -1,11 +1,11 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 4000 --function Test.checkMaxLength +--refine-strings --verbosity 10 --max-nondet-string-length 4000 --function Test.checkMaxLength ^SIGNAL=0$ -- ^EXIT=0$ assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: SUCCESS -- -The solver may give an ERROR because the value of string-max-length is too +The solver may give an ERROR because the value of max-nondet-string-length is too small to give an answer about the assertion. So we just check that the answer is not success. 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 2a9b5555478..16844cdfae5 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 ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_append_char.java line 23 .* SUCCESS diff --git a/jbmc/regression/strings-smoke-tests/java_append_int/test.desc b/jbmc/regression/strings-smoke-tests/java_append_int/test.desc index 71e874d2486..bd1ab61b350 100644 --- a/jbmc/regression/strings-smoke-tests/java_append_int/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_append_int/test.desc @@ -1,6 +1,6 @@ FUTURE test_append_int.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 847ade7776d..5bc08dd649b 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_append_string.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc b/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc index a6272d26347..ba780a90884 100644 --- a/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc +++ b/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc @@ -1,6 +1,6 @@ CORE test_append_string.class ---refine-strings --string-max-input-length 10 --function test_append_string.check --java-assume-inputs-non-null +--refine-strings --max-nondet-string-length 10 --function test_append_string.check --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.*\].* line 22.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_case/test.desc b/jbmc/regression/strings-smoke-tests/java_case/test.desc index 18fa3cccaa9..911dca3d6a1 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_case.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_case.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_case.java line 10 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_char_array/test.desc b/jbmc/regression/strings-smoke-tests/java_char_array/test.desc index 5d9ef1fdd7c..60830c7a9b1 100644 --- a/jbmc/regression/strings-smoke-tests/java_char_array/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_char_array.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_char_array.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_char_array.main ^EXIT=10$ ^SIGNAL=0$ .*assertion.* test_char_array.java line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc index 1b0d5054458..8cadf6b5a7a 100644 --- a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_char_at.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc index 31a1a0340e4..bf38b989546 100644 --- a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc @@ -1,6 +1,6 @@ CORE test_code_point.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_code_point.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_code_point.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test.desc b/jbmc/regression/strings-smoke-tests/java_contains/test.desc index 45af4256612..067bb2784e7 100644 --- a/jbmc/regression/strings-smoke-tests/java_contains/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_contains/test.desc @@ -1,6 +1,6 @@ CORE test_contains.class ---refine-strings --verbosity 10 --string-max-length 100 --function test_contains.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function test_contains.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc index e8b0e0c7c24..d521b0d12e5 100644 --- a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc +++ b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc @@ -1,6 +1,6 @@ KNOWNBUG test_contains.class ---refine-strings --verbosity 10 --string-max-length 100 --string-printable --function test_contains.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --string-printable --function test_contains.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* 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 4f3d210102a..89f5a633421 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_delete_char_at.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc index 4e04e6544ee..4302bbcd0ff 100644 --- a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc @@ -1,6 +1,6 @@ CORE test_endswith.class ---refine-strings --verbosity 10 --string-max-length 100 --function test_endswith.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function test_endswith.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_equal/test.desc b/jbmc/regression/strings-smoke-tests/java_equal/test.desc index 946129f44a6..554966f3583 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 ---refine-strings --verbosity 10 --string-max-length 100 --string-max-length 100 +--refine-strings --verbosity 10 --max-nondet-string-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/strings-smoke-tests/java_equal/test_2.desc b/jbmc/regression/strings-smoke-tests/java_equal/test_2.desc index ab7cb11a7de..2e0b07e2cd6 100644 --- a/jbmc/regression/strings-smoke-tests/java_equal/test_2.desc +++ b/jbmc/regression/strings-smoke-tests/java_equal/test_2.desc @@ -1,6 +1,6 @@ KNOWNBUG test_equal_2.class ---refine-strings --verbosity 10 --string-max-length 100 --string-max-length 100 +--refine-strings --verbosity 10 --max-nondet-string-length 100 ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/strings-smoke-tests/java_float/test.desc b/jbmc/regression/strings-smoke-tests/java_float/test.desc index c0a002b0ede..1ac8eb18d74 100644 --- a/jbmc/regression/strings-smoke-tests/java_float/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_float/test.desc @@ -1,6 +1,6 @@ FUTURE test_float.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_float.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_float.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_format/test.desc b/jbmc/regression/strings-smoke-tests/java_format/test.desc index e8e8666c160..7f8abed85c7 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 ---refine-strings --verbosity 10 --string-max-length 20 --function test.main +--refine-strings --verbosity 10 --max-nondet-string-length 20 --function test.main ^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 f81c6fa17e1..b0d5d078a0d 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 ---refine-strings --verbosity 10 --string-max-length 20 --function test.main +--refine-strings --verbosity 10 --max-nondet-string-length 20 --function test.main ^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 e0a0de54aa4..1a2d0cfa22f 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 ---refine-strings --verbosity 10 --string-max-length 20 --function test.main +--refine-strings --verbosity 10 --max-nondet-string-length 20 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_format4/test.desc b/jbmc/regression/strings-smoke-tests/java_format4/test.desc index 51f9f2b1d29..1b65756d147 100644 --- a/jbmc/regression/strings-smoke-tests/java_format4/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_format4/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test.class ---refine-strings --verbosity 10 --string-max-length 20 +--refine-strings --verbosity 10 --max-nondet-string-length 20 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_format5/test.desc b/jbmc/regression/strings-smoke-tests/java_format5/test.desc index 4e09fa65ada..1900ce57e1e 100644 --- a/jbmc/regression/strings-smoke-tests/java_format5/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_format5/test.desc @@ -1,6 +1,6 @@ THOROUGH test.class ---refine-strings --verbosity 10 --string-max-length 20 +--refine-strings --verbosity 10 --max-nondet-string-length 20 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc index 1392b360f66..87587146a13 100644 --- a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,6 +1,6 @@ CORE test_hash_code.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_hash_code.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_hash_code.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_if/test.desc b/jbmc/regression/strings-smoke-tests/java_if/test.desc index 635e7c094cd..58abdc74d6e 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 ---refine-strings --verbosity 10 --string-max-length 100 --function test.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 11.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc index 6fd524b72c1..c129dcad043 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_index_of.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_index_of.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc index 954e794efde..3db2328b89f 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc @@ -1,6 +1,6 @@ CORE test_index_of2.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_index_of2.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc index 30ce1a9a702..d3535a6b3ee 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_index_of_char.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of_char.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_index_of_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 bcae9bf0ea6..23cb50f5367 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_insert_char.main ^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 53af52fc3ef..947cef03f4f 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char_array.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main ^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 d36dc796a31..d90d40ce976 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_multiple.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main ^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 066e26a74b2..9db9c445404 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_string.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main ^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 a8ace56c37b..e433b8c2562 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test1.main ^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 e068d78d000..5d0e99daa0d 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc index dc7e825073c..99ba72778ba 100644 --- a/jbmc/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc +++ b/jbmc/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc @@ -8,5 +8,5 @@ assertion.* line 10 .* FAILURE$ -- non equal types -- -When string-max-length is not set, the solver can run out of memory in +When max-nondet-string-length is not set, the solver can run out of memory in an unpredictable way. 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 b35b58c87fa..f968c7ba6bb 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test3.main ^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 3630073e1dd..0f190eec085 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test4.main ^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 9fdf756a99d..15036b5d8d8 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc index 4c289d1853c..c46a73355a6 100644 --- a/jbmc/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test.main ^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 f76d7849b64..9d6f1e0006f 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main ^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 b6b50f07cb3..fa6be8629c7 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main ^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 0252051ba90..90bc0e71059 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main ^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 391797533f5..4cf662cfa9b 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main ^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 e37cf5534de..d13e4079f6d 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main ^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 e6ca4960d19..b1a8b9af433 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main ^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 d2f4d7cbb1c..5952cba8b94 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 ---refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main ^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 a223a0e81df..a22dfff66b9 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main ^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 229c999d00c..9200f5bf6c0 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main ^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 8b9c5a50209..cc68e1a7f03 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc index 6d5672788ae..69a6db6958b 100644 --- a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc +++ b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_binary.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc index c5d33723394..23d47e2f8da 100644 --- a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc +++ b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_hex.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc index 135a6d1a4aa..e1d5074627e 100644 --- a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc +++ b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_octal.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_octal.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc index 778cfffeae4..3ca2f42ee21 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_intern/test.desc @@ -1,6 +1,6 @@ CORE test_intern.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_intern.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_intern.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc index 917218b59dd..5a97722e145 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_last_index_of.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of2/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of2/test.desc index 31f2d6afebb..dbadf19e125 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of2/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --max-nondet-string-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc index 451966cbac1..6fbf3e1b742 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of_char.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of_char.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_last_index_of_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_length/test.desc b/jbmc/regression/strings-smoke-tests/java_length/test.desc index f3a7b3e99c7..a24169cab4d 100644 --- a/jbmc/regression/strings-smoke-tests/java_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_length/test.desc @@ -1,6 +1,6 @@ CORE test_length.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_length.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_length.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/java_length2/test.desc b/jbmc/regression/strings-smoke-tests/java_length2/test.desc index 7223a6600d8..6ac6da936e8 100644 --- a/jbmc/regression/strings-smoke-tests/java_length2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_length2/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test.check +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test.check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 a8ace56c37b..e433b8c2562 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc index 45859f9d225..d9f763abd8f 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc @@ -1,6 +1,6 @@ THOROUGH Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc index 8f4c4c1aae9..d0561dc7bc4 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc @@ -1,6 +1,6 @@ THOROUGH Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc index 9f0dea8b275..a1b2a13893d 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc @@ -1,6 +1,6 @@ THOROUGH Test4.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test4.main ^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 9fdf756a99d..15036b5d8d8 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc index 64b50f64e69..b6b8837e7a7 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary1.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc index fe04564fdbc..b8b42fa1921 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary2.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc index 22abe124fb8..f4bcfcbc0f0 100644 --- a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc +++ b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary3.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main ^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 391797533f5..4cf662cfa9b 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main ^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 e37cf5534de..d13e4079f6d 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main ^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 e6ca4960d19..b1a8b9af433 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main ^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 d2f4d7cbb1c..5952cba8b94 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 ---refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main ^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 6543f6938f7..7fba77b9db6 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 ---refine-strings --verbosity 10 --string-max-length 100 --function Test_octal1.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main ^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 7597b88f4be..f464571b15f 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 ---refine-strings --verbosity 10 --string-max-length 100 --function Test_octal2.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function Test_octal2.main ^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 aea786f5b92..4dcfa3b96a8 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 ---refine-strings --verbosity 10 --string-max-length 100 --function Test_octal3.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function Test_octal3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc index 9b4e20397e0..0d1e9c41083 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc index eb61c1ce86a..04ab6041818 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc @@ -1,6 +1,6 @@ CORE Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc index 4f888659004..5e1b8980b16 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* FAILURE$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc index f71c35b54bd..f9c776a2363 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc index 9b4e20397e0..0d1e9c41083 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc index 8ea06b614e0..fe15d7d56fd 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc @@ -1,6 +1,6 @@ CORE Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc index 1e96c531c29..0abe634d775 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc index e0980a2d899..21e0d1c4342 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc @@ -1,6 +1,6 @@ CORE Test4.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test4.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc index b7f35f7dccb..9f1727b8823 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc @@ -1,6 +1,6 @@ CORE Test5.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc index 0f42ae7f205..3f5a5959362 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc @@ -1,6 +1,6 @@ CORE Test6.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test6.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test6.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc index fe1f4d22881..9ba7610d08b 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc index 9243521d9ff..93c96a9d818 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc @@ -1,6 +1,6 @@ CORE Test_binary_min.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary_min.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_binary_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc index 9797e44dff0..a54cdbe6678 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc @@ -1,6 +1,6 @@ CORE Test_decimal_max.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_max.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_decimal_max.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc index e2f1869d29d..a780c232806 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc @@ -1,6 +1,6 @@ CORE Test_decimal_min.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_min.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_decimal_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc index 7a991265f4c..f77bbdf3a3b 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc @@ -1,6 +1,6 @@ CORE Test_hex.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_hex.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc index a35595e7d2c..769fdf82c41 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc @@ -1,6 +1,6 @@ CORE Test_octal.class ---refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function Test_octal.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_replace/test.desc b/jbmc/regression/strings-smoke-tests/java_replace/test.desc index a8536074098..7c9960fac44 100644 --- a/jbmc/regression/strings-smoke-tests/java_replace/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_replace/test.desc @@ -1,6 +1,6 @@ FUTURE test_replace.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --max-nondet-string-length 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 cae6c9a525b..1fb5c827619 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_replace_char.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_replace_char.main ^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 0adb430c3b3..8a2a62eb13e 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test_set_char_at.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_set_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc index 21dd8d95a49..3821ed0a4c0 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc @@ -1,6 +1,6 @@ CORE test_set_length.class ---refine-strings --verbosity 10 --string-max-length 100 --function test_set_length.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function test_set_length.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc index 5a0ca5ea703..bf4e0c438ae 100644 --- a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc @@ -1,6 +1,6 @@ CORE test_starts_with.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_starts_with.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_starts_with.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc index 2debae07cf9..48b04d5479e 100644 --- a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -1,6 +1,6 @@ CORE test_sb_length.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_sb_length.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_sb_length.main ^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 14b0a94e55d..c2e3d975343 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 ---refine-strings --verbosity 10 --function Test.check --string-max-length 100 --string-printable --java-assume-inputs-non-null +--refine-strings --verbosity 10 --function Test.check --max-nondet-string-length 100 --string-printable --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ assertion.* file Test.java line 6 .* SUCCESS diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test_char.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test_char.desc index 8447c321008..76672144285 100644 --- a/jbmc/regression/strings-smoke-tests/java_string_printable/test_char.desc +++ b/jbmc/regression/strings-smoke-tests/java_string_printable/test_char.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --function Test.check_char --string-max-length 100 --string-printable +--refine-strings --verbosity 10 --function Test.check_char --max-nondet-string-length 100 --string-printable ^EXIT=0$ ^SIGNAL=0$ assertion.* file Test.java line 18 .* SUCCESS diff --git a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc index e16da196007..29d246e5584 100644 --- a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc @@ -1,6 +1,6 @@ CORE test_subsequence.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_subsequence.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_subsequence.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_substring/test.desc b/jbmc/regression/strings-smoke-tests/java_substring/test.desc index 5787d80275d..6c9cc4c6828 100644 --- a/jbmc/regression/strings-smoke-tests/java_substring/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_substring/test.desc @@ -1,6 +1,6 @@ CORE test_substring.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test_substring.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test_substring.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_trim/test.desc b/jbmc/regression/strings-smoke-tests/java_trim/test.desc index d60e82f050e..c250779d183 100644 --- a/jbmc/regression/strings-smoke-tests/java_trim/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_trim/test.desc @@ -1,6 +1,6 @@ CORE test_trim.class ---refine-strings --verbosity 10 --string-max-length 100 --function test_trim.main +--refine-strings --verbosity 10 --max-nondet-string-length 100 --function test_trim.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* 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 ed1f8baf6e3..a1ef81cc6ce 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 ---refine-strings --verbosity 10 --function test.check --string-max-length 100 +--refine-strings --verbosity 10 --function test.check --max-nondet-string-length 100 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float_2/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float_2/test.desc index 7eaf4f137af..5de79089ab9 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_float_2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_float_2/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test.class ---refine-strings --verbosity 10 --function test.check --string-max-length 1000 +--refine-strings --verbosity 10 --function test.check --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 6 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float_3/test.desc index a92486ab894..6ddb2a9b28c 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_float_3/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_float_3/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test.check +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 7 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc index e170694c992..e35f31fb44b 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc @@ -1,6 +1,6 @@ THOROUGH test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test.check +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* test.java line 8 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc index d643bd88a4b..bfce78227df 100644 --- a/jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc @@ -1,6 +1,6 @@ THOROUGH test.class ---refine-strings --verbosity 10 --string-max-length 1000 --function test.check +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 6 .* 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 e91920c7478..e0a87dd92b2 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 ---refine-strings --verbosity 10 --string-max-length 1000 --function test.main +--refine-strings --verbosity 10 --max-nondet-string-length 1000 --function test.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 9 .* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest.desc deleted file mode 100644 index 4603a102472..00000000000 --- a/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -MemberTest.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function MemberTest.main -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest2.desc b/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest2.desc deleted file mode 100644 index b4e7b2322e4..00000000000 --- a/jbmc/regression/strings-smoke-tests/max_input_length/MemberTest2.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -MemberTest.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function MemberTest.main -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc index 0943fca690c..97b09c31632 100644 --- a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc +++ b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function Test.main +--refine-strings --verbosity 10 --max-nondet-string-length 31 --function Test.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc index 307bc7db2fc..0e7733ff4e9 100644 --- a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc +++ b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function Test.main +--refine-strings --verbosity 10 --max-nondet-string-length 20 --function Test.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 0283c9346f6..b7183c2cc67 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -243,13 +243,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) } if(!cmdline.isset("no-refine-strings")) - { options.set_option("refine-strings", true); - options.set_option("string-printable", cmdline.isset("string-printable")); - if(cmdline.isset("string-max-length")) - options.set_option( - "string-max-length", cmdline.get_value("string-max-length")); - } + + if(cmdline.isset("string-printable")) + options.set_option("string-printable", true); if(cmdline.isset("max-node-refinement")) options.set_option( @@ -1142,7 +1139,6 @@ void jbmc_parse_optionst::help() " --refine use refinement procedure (experimental)\n" " --no-refine-strings turn off string refinement\n" " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) - " --string-max-length add constraint on the length of strings\n" // NOLINT(*) " --max-nondet-string-length bound the length of nondet (e.g. input) strings\n" // NOLINT(*) " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 9f5da915be3..84ee50675ee 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -58,7 +58,6 @@ class optionst; "(refine-strings)" /* will go away */ \ "(no-refine-strings)" \ "(string-printable)" \ - "(string-max-length):" \ "(string-max-input-length):" /* will go away */ \ "(max-nondet-string-length):" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \