diff --git a/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc b/jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc index 30ce2644914..f87bf19d58b 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 +--max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion at file test.java line 8 .* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc index 4d82786d6ef..223f1bdf8d0 100644 --- a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.testme +--no-refine-strings --function Test.testme ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ @@ -8,5 +8,5 @@ Test.class type mismatch -- Before cbmc#2472 this would assume that StringBuilder's direct parent was -java.lang.Object, causing a type mismatch when --refine-strings was not in use +java.lang.Object, causing a type mismatch when --no-refine-strings was in use (which at the time would assume that parent-child relationship) diff --git a/jbmc/regression/jbmc-strings/RegexMatches01/test.desc b/jbmc/regression/jbmc-strings/RegexMatches01/test.desc index 4a95eb71ab0..0364705273b 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 +--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..10e3a8aef3b 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 +--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..5bbdc78a27f 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 +--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..11af4f9b40e 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 +--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..ed4d11ba8ad 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 +--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..28ea226d684 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 +--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..28c69f8650b 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 +--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..3e02ea3ee0f 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 +--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..8c5dd9ae374 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 +--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..e14a448021f 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 +--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..9459dcc6879 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 +--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..e8135aa2944 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 +--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..84ed8e34e82 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 +--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..e863abf2ff9 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 +--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..57c4d8e9eb6 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 +--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..17267a3f8c6 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 +--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..0d177fcd774 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 +--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..7a55841400e 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 +--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..d75e4e17729 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 +--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..fa49145f51c 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 +--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..aad7f07a270 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 +--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..e07f191cdd2 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 +--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..15885dce3b6 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 +--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..ade8a43206b 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 +--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..0923359deef 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 +--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..6876ee28585 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 +--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..feb9eed49ec 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 +--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..cfbea436519 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 +--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..34d23766599 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 +--max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc index 68b636a5d67..c085d3c6925 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check +--function Test.check ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 13 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc index 5c347f7792a..828b9e74b6e 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 +--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..a8e2cbcea18 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 +--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..94feb4c1ba4 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 +--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..d2cdf1e0b2b 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 +--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..e92dfe97c43 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 +--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..d45432179eb 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 +--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..effc9f3b6dc 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 +--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..24bf5fb6d37 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 +--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..f7f8c7311b5 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 +--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..e242a113574 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' +--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..3a416040694 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 +--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..28637b9e88a 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 +--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..3c03d52da53 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' +--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..ff8a641bea4 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 +--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..729edb5fdab 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 +--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..8f7d58040bb 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 +--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..2b206567e67 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 +--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..70e80692a47 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 +--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..a19dc1fcb33 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 +--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..09c05d89840 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 +--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..24c66c5fb57 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 +--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..3b16b6472cc 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 +--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..7d19a58382b 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 +--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..8a044652d45 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 +--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..2557139bdae 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 +--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..c99525e7596 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 +--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..112a8731ee6 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 +--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..03e0d7f40ca 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 +--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..86d572bd7c5 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 +--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..9cef6268e3e 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 +--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..4bc3626b3b0 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 +--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..4bc3626b3b0 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 +--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..c40eeaa688f 100644 --- a/jbmc/regression/jbmc-strings/StringContains03/test.desc +++ b/jbmc/regression/jbmc-strings/StringContains03/test.desc @@ -1,11 +1,11 @@ CORE Test.class ---refine-strings --function Test.check +--function Test.check ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ 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..c24b73552dc 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 +--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..2a4995cc7b0 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 +--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..af74c877f50 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 +--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..5a6493cc9dd 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 +--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..fd81013c23a 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 +--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..069eb7b64ee 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 +--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..f59873b9774 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 +--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..918e5eae3fa 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 +--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..6599b437f58 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 +--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..c109a8a3823 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 +--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..6f03e6e0f8b 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 +--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..ac88153db76 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 +--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..f90f27e4a91 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 +--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..9e2a476ee03 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 --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..b6fc0921c0c 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 +--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..9f6c94dec04 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 +--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..c147beb269f 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 +--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..77004d943d0 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 +--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..5eb1c733197 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 +--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..7d5ffcaee82 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 +--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..7a62fcd4612 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 +--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..7d212539658 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 +--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..c7aeccd9215 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 +--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..89f2a08336e 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 +--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..354c20c239b 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 +--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..d44990b4910 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 +--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..6dd28b97a01 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 +--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..aab18c3bad6 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 +--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..0bd02bf0492 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 +--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..234ff205769 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 +--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..db32c5fef09 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 +--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..a7d67344a20 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 +--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..783cd2935dc 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 +--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..8f6e86bcba9 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 +--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..47757796d1e 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 +--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..8af455c48db 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 +--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..2de78f35997 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 +--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..b065ddf0d67 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 +--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..401e4cf5fa2 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 +--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..e6073126082 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 +--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..47166124a31 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 --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..25b7c86bea2 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 +--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..2a4950dbf45 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 +--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..2631500be00 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 +--max-nondet-string-length 1000 --function StringValueOfBool.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc index fea3171d5b6..46c23067a93 100644 --- a/jbmc/regression/jbmc-strings/char_escape/test.desc +++ b/jbmc/regression/jbmc-strings/char_escape/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.test --cover location --trace --json-ui +--function Test.test --cover location --trace --json-ui ^EXIT=0$ ^SIGNAL=0$ 20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\) diff --git a/jbmc/regression/jbmc-strings/instanceof/test.desc b/jbmc/regression/jbmc-strings/instanceof/test.desc index 3c597735589..80374910bea 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 +--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..71043e73f19 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 +--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..1283ec2242b 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 +--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..3c91ecee3b3 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 +--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..d73e3c7dbac 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 +--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..67f87337d17 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 +--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..126fdb83bde 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 +--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..c26d99b0669 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 +--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..4c7a93aed7e 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 +--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..cc68fbb7f2f 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 +--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..87b16a3df5a 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 +--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..9a83cbda83c 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 +--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..72fa2dc1467 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 +--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/literal-length/test.desc b/jbmc/regression/jbmc-strings/literal-length/test.desc index c9e7816e08c..7e264338c3c 100644 --- a/jbmc/regression/jbmc-strings/literal-length/test.desc +++ b/jbmc/regression/jbmc-strings/literal-length/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check + --function Test.check assertion at file Test.java line 6 .* SUCCESS assertion at file Test.java line 8 .* FAILURE ^EXIT=10$ diff --git a/jbmc/regression/jbmc-strings/long_string/test.desc b/jbmc/regression/jbmc-strings/long_string/test.desc index 7f5301726d3..80168d9729d 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 +--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/long_string/test_abort.desc b/jbmc/regression/jbmc-strings/long_string/test_abort.desc index 8daa50acd1a..16e6b93c80d 100644 --- a/jbmc/regression/jbmc-strings/long_string/test_abort.desc +++ b/jbmc/regression/jbmc-strings/long_string/test_abort.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.checkAbort --trace +--function Test.checkAbort --trace ^EXIT=10$ ^SIGNAL=0$ dynamic_object[0-9]*=\(assignment removed\) 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..e712029ce44 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 +--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..ca374b5183c 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 +--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..ac1d66e8982 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 +--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..35637e7c5ee 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 +--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..50ab0ab32b7 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 +--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..9bd15e68cfd 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 +--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/jbmc/NullPointer1/test.desc b/jbmc/regression/jbmc/NullPointer1/test.desc index 64fd6a24f69..6db1ebbcbf5 100644 --- a/jbmc/regression/jbmc/NullPointer1/test.desc +++ b/jbmc/regression/jbmc/NullPointer1/test.desc @@ -1,6 +1,6 @@ CORE NullPointer1.class ---pointer-check --stop-on-fail +--stop-on-fail ^EXIT=10$ ^SIGNAL=0$ ^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode-index 9$ diff --git a/jbmc/regression/jbmc/NullPointer2/test.desc b/jbmc/regression/jbmc/NullPointer2/test.desc index 366d28f8b02..ce76dda2e8d 100644 --- a/jbmc/regression/jbmc/NullPointer2/test.desc +++ b/jbmc/regression/jbmc/NullPointer2/test.desc @@ -1,6 +1,6 @@ CORE NullPointer2.class ---pointer-check --stop-on-fail +--stop-on-fail ^EXIT=10$ ^SIGNAL=0$ ^ file NullPointer2.java line 9 function java::NullPointer2.main:\(\[Ljava/lang/String;\)V diff --git a/jbmc/regression/jbmc/NullPointer3/test.desc b/jbmc/regression/jbmc/NullPointer3/test.desc index 3cf4998f5aa..664e6ad1b7d 100644 --- a/jbmc/regression/jbmc/NullPointer3/test.desc +++ b/jbmc/regression/jbmc/NullPointer3/test.desc @@ -1,6 +1,6 @@ CORE NullPointer3.class ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^.*Null pointer check: FAILURE$ diff --git a/jbmc/regression/jbmc/NullPointer4/test.desc b/jbmc/regression/jbmc/NullPointer4/test.desc index fbe3588bfff..e4552020a9a 100644 --- a/jbmc/regression/jbmc/NullPointer4/test.desc +++ b/jbmc/regression/jbmc/NullPointer4/test.desc @@ -1,6 +1,6 @@ CORE NullPointer4.class ---pointer-check --stop-on-fail +--stop-on-fail ^EXIT=10$ ^SIGNAL=0$ ^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode-index 4$ diff --git a/jbmc/regression/jbmc/pointer_check1/test.desc b/jbmc/regression/jbmc/pointer_check1/test.desc index 046a52ad894..b1b015d7f9c 100644 --- a/jbmc/regression/jbmc/pointer_check1/test.desc +++ b/jbmc/regression/jbmc/pointer_check1/test.desc @@ -1,6 +1,6 @@ CORE pointer_check1.class ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/static_method1/test.desc b/jbmc/regression/jbmc/static_method1/test.desc index 2881b8787ce..349416098cb 100644 --- a/jbmc/regression/jbmc/static_method1/test.desc +++ b/jbmc/regression/jbmc/static_method1/test.desc @@ -1,6 +1,6 @@ CORE static_method1.class ---function 'static_method1.f' --div-by-zero-check +--function 'static_method1.f' ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ 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..ac1c9428a67 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 +--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..e4be36b1c8f 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 +--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..6f95d07fc09 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 +--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..dfc4db41940 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 + --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..1d6ecc944c3 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 +--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..1004ac1cdb9 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 +--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..ca5635aee65 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 +--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..90fc679b755 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 +--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..35f4d2a9914 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 +--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..c3cbb10a72c 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 +--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..778e65ea7c3 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 +--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..5085a523ee4 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 +--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..116034ea133 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 +--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..c0b3df9ba0b 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 +--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..a3c6a656ebc 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 +--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..596c113a269 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 +--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..f8e74ee54e1 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 +--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..47a451b32d1 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 +--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..ec3feac3b5a 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 +--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..a2408125b74 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 +--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..7b22b4ecde6 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 +--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..13181d89185 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 +--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..47841cb9904 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 +--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..c59c94a2e69 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 +--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..03f6b84ef00 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 +--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..a9502c6fcca 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 +--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..1d763c7bc2f 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 +--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..af69a7a96b3 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 +--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..5e399123ae3 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 +--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..2836a8e301a 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 +--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..89d011bd40b 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 +--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..f7fd7b0e69e 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 @@ -1,6 +1,6 @@ KNOWNBUG Test2.class ---refine-strings --verbosity 10 --function Test2.main +--verbosity 10 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ @@ -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..24fa815010f 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 +--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..38bd06e75c4 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 +--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..af9f367a40a 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 +--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..400a76bea31 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 +--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..bea25418b87 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 +--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..ffe64c3c60a 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 +--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..101333b4532 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 +--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..ca902955ffd 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 +--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..ee6a2476f08 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 +--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..b4cdac17a5f 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 +--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..e8f2161cd07 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 +--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..56d6b4e18d1 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 +--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..7905d63513f 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 +--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..afbf33b8565 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 +--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..bfa55388eef 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 +--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..0032e4fa6f1 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 +--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..c8abb4272cb 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 +--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..42f1e4cdd52 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 +--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..e3c48084b53 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 +--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..9c651f31117 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 +--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..b86f36d27a8 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 +--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..bc66c069708 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 +--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..a25dd11fd15 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 +--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..2836a8e301a 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 +--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..6e99f203a57 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 +--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..9b62c8d151c 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 +--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..985b11eb594 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 +--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..af9f367a40a 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 +--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..251f49d489e 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 +--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..53274ddeaf9 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 +--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..d800b1661f2 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 +--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..ca902955ffd 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 +--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..ee6a2476f08 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 +--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..b4cdac17a5f 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 +--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..e8f2161cd07 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 +--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..98a4ff52518 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 +--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..5111865d119 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 +--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..612a31faed9 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 +--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..645e005f695 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 +--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..9bbba29c733 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 +--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..c8241a07529 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 +--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..945aebdc763 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 +--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..645e005f695 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 +--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..6a5514b41bb 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 +--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..f9502a65496 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 +--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..f871eae988f 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 +--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..f61714e1262 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 +--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..b8e30caaed8 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 +--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..2d739d94b5f 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 +--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..afbd8d0b33f 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 +--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..dc7239c52e7 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 +--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..81df1aef999 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 +--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..266d66658f0 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 +--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..1960ef81064 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 +--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..7504f6cdd94 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 +--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..2df369dfaea 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 +--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..b394b585a0e 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 +--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..59073921427 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 +--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..affcad324a0 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 +--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..5431e96a460 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 +--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..6884c820757 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 +--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..eaa7be7df33 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 +--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..4865271de81 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 +--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..cbb1594ff2c 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 +--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..0252776cd9c 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 +--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..567d75e441e 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 +--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..cd2a6ba2a77 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 +--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..3c8ed3c7213 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 +--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..b9205856f3a 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 +--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..13a50ef2102 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 +--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..a2bb2d0d696 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 +--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..5794a8b3b6b 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 +--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..25cc34d2516 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 +--verbosity 10 --max-nondet-string-length 20 --function Test.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 9a742b37099..20885ed689c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -35,43 +35,47 @@ Author: Daniel Kroening, kroening@kroening.com "(throw-runtime-exceptions)" \ "(java-max-input-array-length):" /* will go away */ \ "(max-nondet-array-length):" \ - "(java-max-input-tree-depth):" /* will go away */ \ + "(java-max-input-tree-depth):" /* will go away */ \ "(max-nondet-tree-depth):" \ "(java-max-vla-length):" \ "(java-cp-include-files):" \ - "(lazy-methods)" /* will go away */ \ + "(lazy-methods)" /* will go away */ \ "(no-lazy-methods)" \ "(lazy-methods-extra-entry-point):" \ "(java-load-class):" \ "(java-no-load-class):" -#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ - " --disable-uncaught-exception-check" \ - " ignore uncaught exceptions and errors\n" \ - " --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \ - " assert statements instead of failing\n" \ - " at the location of the assert statement\n" /* NOLINT(*) */ \ - " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ - " entry point with null\n" /* NOLINT(*) */ \ - " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ - " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ - " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ - " at level N references are set to null\n" /* NOLINT(*) */ \ - " --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \ - " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \ - " --no-lazy-methods load and translate all methods given on the command line\n" /* NOLINT(*) */ \ - " and in --classpath\n" /* NOLINT(*) */ \ - " Default is to load methods that appear to be\n" /* NOLINT(*) */ \ - " reachable from the --function entry point or main class\n" /* NOLINT(*) */ \ - " Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \ - " are restricted to loaded methods by default\n" /* NOLINT(*) */ \ - " --lazy-methods-extra-entry-point METHODNAME\n" /* NOLINT(*) */ \ - " treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \ - " the purpose of lazy method loading\n" /* NOLINT(*) */ \ - " METHODNAME can be a regex that will be matched against\n" /* NOLINT(*) */ \ - " all symbols. If missing a java:: prefix will be added\n" /* NOLINT(*) */ \ - " If no descriptor is found, all overloads of a method will\n"/* NOLINT(*) */ \ - " also be added." /* NOLINT(*) */ +#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ + " --disable-uncaught-exception-check\n" \ + " ignore uncaught exceptions and errors\n" \ + " --throw-assertion-error throw java.lang.AssertionError on violated\n" \ + " assert statements instead of failing\n" \ + " at the location of the assert statement\n" \ + " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ + " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ + " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ + " at level N references are set to null\n" /* NOLINT(*) */ \ + " --java-assume-inputs-non-null\n" \ + " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ + " entry point with null\n" /* NOLINT(*) */ \ + " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \ + " --java-cp-include-files r regexp or JSON list of files to load\n" \ + " (with '@' prefix)\n" \ + " --no-lazy-methods load and translate all methods given on\n" \ + " the command line and in --classpath\n" \ + " Default is to load methods that appear to be\n" /* NOLINT(*) */ \ + " reachable from the --function entry point\n" \ + " or main class\n" \ + " Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \ + " and --show-properties output are restricted to\n" /* NOLINT(*) */ \ + " loaded methods by default.\n" \ + " --lazy-methods-extra-entry-point METHODNAME\n" \ + " treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \ + " point for the purpose of lazy method loading\n" /* NOLINT(*) */ \ + " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \ + " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \ + " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \ + " overloads of a method will also be added.\n" // clang-format on class symbolt; diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 0283c9346f6..00e11ad3bcc 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -80,6 +80,23 @@ ::jbmc_parse_optionst::jbmc_parse_optionst( { } +void jbmc_parse_optionst::set_default_options(optionst &options) +{ + // Default true + options.set_option("assertions", true); + options.set_option("assumptions", true); + options.set_option("built-in-assertions", true); + options.set_option("pretty-names", true); + options.set_option("propagation", true); + options.set_option("refine-strings", true); + options.set_option("sat-preprocessor", true); + options.set_option("simplify", true); + options.set_option("simplify-if", true); + + // Other default + options.set_option("arrays-uf", "auto"); +} + void jbmc_parse_optionst::get_command_line_options(optionst &options) { if(config.set(cmdline)) @@ -88,6 +105,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) exit(1); // should contemplate EX_USAGE from sysexits.h } + jbmc_parse_optionst::set_default_options(options); + if(cmdline.isset("show-symex-strategies")) { std::cout << path_strategy_chooser.show_strategies(); @@ -107,15 +126,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-simplify")) options.set_option("simplify", false); - else - options.set_option("simplify", true); if(cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") || cmdline.isset("outfile")) options.set_option("stop-on-fail", true); - else - options.set_option("stop-on-fail", false); if(cmdline.isset("trace") || cmdline.isset("stop-on-fail")) @@ -148,8 +163,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) // constant propagation if(cmdline.isset("no-propagation")) options.set_option("propagation", false); - else - options.set_option("propagation", true); // transform self loops to assumptions options.set_option( @@ -166,18 +179,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); - else - options.set_option("assertions", true); // use assumptions if(cmdline.isset("no-assumptions")) options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); // generate unwinding assertions if(cmdline.isset("cover")) @@ -210,15 +215,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) // simplify if conditions and branches if(cmdline.isset("no-simplify-if")) options.set_option("simplify-if", false); - else - options.set_option("simplify-if", true); if(cmdline.isset("arrays-uf-always")) options.set_option("arrays-uf", "always"); else if(cmdline.isset("arrays-uf-never")) options.set_option("arrays-uf", "never"); - else - options.set_option("arrays-uf", "auto"); if(cmdline.isset("dimacs")) options.set_option("dimacs", true); @@ -242,13 +243,23 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("refine-arithmetic", true); } - if(!cmdline.isset("no-refine-strings")) + if(cmdline.isset("no-refine-strings")) + options.set_option("refine-strings", false); + + if(cmdline.isset("string-printable")) + options.set_option("string-printable", true); + + if(cmdline.isset("no-refine-strings") && cmdline.isset("string-printable")) { - 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")); + warning() << "--string-printable ignored due to --no-refine-strings" << eom; + } + + if( + cmdline.isset("no-refine-strings") && + cmdline.isset("max-nondet-string-length")) + { + warning() << "--max-nondet-string-length ignored due to " + << "--no-refine-strings" << eom; } if(cmdline.isset("max-node-refinement")) @@ -257,22 +268,15 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.get_value("max-node-refinement")); // SMT Options - bool version_set=false; if(cmdline.isset("smt1")) { - options.set_option("smt1", true); - options.set_option("smt2", false); - version_set=true; + error() << "--smt1 is no longer supported" << eom; + exit(CPROVER_EXIT_USAGE_ERROR); } if(cmdline.isset("smt2")) - { - // If both are given, smt2 takes precedence - options.set_option("smt1", false); options.set_option("smt2", true); - version_set=true; - } if(cmdline.isset("fpa")) options.set_option("fpa", true); @@ -282,83 +286,52 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("boolector")) { options.set_option("boolector", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("mathsat")) { options.set_option("mathsat", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; - } - - if(cmdline.isset("cvc3")) - { - options.set_option("cvc3", true), solver_set=true; - if(!version_set) - options.set_option("smt1", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("cvc4")) { options.set_option("cvc4", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("yices")) { options.set_option("yices", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("z3")) { options.set_option("z3", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; - } - - if(cmdline.isset("opensmt")) - { - options.set_option("opensmt", true), solver_set=true; - if(!version_set) - options.set_option("smt1", true), version_set=true; + options.set_option("smt2", true); } - if(version_set && !solver_set) + if(cmdline.isset("smt2") && !solver_set) { if(cmdline.isset("outfile")) { // outfile and no solver should give standard compliant SMT-LIB - options.set_option("generic", true), solver_set=true; + options.set_option("generic", true); } else { - if(options.get_bool_option("smt1")) - { - options.set_option("boolector", true), solver_set=true; - } - else - { - INVARIANT(options.get_bool_option("smt2"), "smt2 set"); - options.set_option("z3", true), solver_set=true; - } + // the default smt2 solver + options.set_option("z3", true); } } - // Either have solver and standard version set, or neither. - INVARIANT(version_set==solver_set, "solver and version set"); - if(cmdline.isset("beautify")) options.set_option("beautify", true); if(cmdline.isset("no-sat-preprocessor")) options.set_option("sat-preprocessor", false); - else - options.set_option("sat-preprocessor", true); options.set_option( "pretty-names", @@ -1097,11 +1070,11 @@ void jbmc_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + " --drop-unused-functions drop functions trivially unreachable\n" + " from main function\n" HELP_SHOW_CLASS_HIERARCHY "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" @@ -1116,13 +1089,14 @@ void jbmc_parse_optionst::help() JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP // This one is handled by jbmc_parse_options not by the Java frontend, // hence its presence here: - " --java-threading enable experimental support for java multi-threading\n"// NOLINT(*) - " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*) + " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*) + " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*) // Currently only supported in the JBMC frontend: - " --symex-driven-lazy-loading only load functions when first entered by symbolic execution\n" // NOLINT(*) - " Note --show-symbol-table/goto-functions/properties output\n" // NOLINT(*) - " will be restricted to loaded methods in this case, and only\n" // NOLINT(*) - " output after the symex phase\n" + " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*) + " execution. Note that --show-symbol-table,\n" + " --show-goto-functions/properties output\n" + " will be restricted to loaded methods in this case,\n" // NOLINT(*) + " and only output after the symex phase.\n" "\n" "BMC options:\n" HELP_BMC @@ -1141,8 +1115,7 @@ void jbmc_parse_optionst::help() " --z3 use Z3\n" " --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(*) + " --string-printable restrict to printable strings (experimental)\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..b4fab93735c 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -47,9 +47,7 @@ class optionst; "(document-subgoals)(outfile):" \ "(object-bits):" \ "(classpath):(cp):(main-class):" \ - OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ - "(no-built-in-assertions)" \ "(xml-ui)(json-ui)" \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ "(no-sat-preprocessor)" \ @@ -58,7 +56,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)" \ @@ -100,6 +97,12 @@ class jbmc_parse_optionst: const char **argv, const std::string &extra_options); + /// \brief Set the options that have default values + /// + /// This function can be called from clients that wish to emulate JBMC's + /// default behaviour, for example unit tests. + static void set_default_options(optionst &); + void process_goto_function( goto_model_functiont &function, const abstract_goto_modelt &, diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 24204c061b4..5c9cd1c4633 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -43,7 +43,6 @@ class optionst; "(object-bits):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ - "(no-built-in-assertions)" \ "(xml-ui)(xml-interface)(json-ui)" \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ "(no-sat-preprocessor)" \ diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 976fbcc5923..913d570b7e8 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -32,13 +32,14 @@ void reachability_slicer( const std::list &properties, const bool include_forward_reachability); -#define OPT_REACHABILITY_SLICER \ +// clang-format off +#define OPT_REACHABILITY_SLICER \ "(reachability-slice)(reachability-slice-fb)" // NOLINT(*) -#define HELP_REACHABILITY_SLICER \ - " --reachability-slice remove instructions that cannot appear on a " \ - "trace from entry point to a property\n" \ - " --reachability-slice-fb remove instructions that cannot appear on a " \ - "trace from entry point through a property\n" // NOLINT(*) - +#define HELP_REACHABILITY_SLICER \ + " --reachability-slice remove instructions that cannot appear on\n" \ + " a trace from entry point to a property\n" \ + " --reachability-slice-fb remove instructions that cannot appear on\n" \ + " a trace from entry point through a property\n" // NOLINT(*) +// clang-format on #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H