diff --git a/jbmc/regression/jbmc-strings/StringContains03/test.desc b/jbmc/regression/jbmc-strings/StringContains03/test.desc index a191de45da5..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 ---function Test.check --max-nondet-string-length 1000000000 +--function Test.check ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ file Test.java line 20 .*: FAILURE$ -- -- -This tests the behaviour of string refinement on very large strings. -max-nondet-string-length is set big enough to cause an overflow. +--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/long_string/test_abort.desc b/jbmc/regression/jbmc-strings/long_string/test_abort.desc index b7f744ef549..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 ---function Test.checkAbort --trace --max-nondet-string-length 1000000000 +--function Test.checkAbort --trace ^EXIT=10$ ^SIGNAL=0$ dynamic_object[0-9]*=\(assignment removed\) @@ -8,4 +8,3 @@ dynamic_object[0-9]*=\(assignment removed\) -- This tests that the object does not appear in the trace, because concretizing a string of the required length may take too much memory. -max-nondet-string-length is set big enough to cause an overflow. diff --git a/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc index 4367dab85aa..ce942f21ec6 100644 --- a/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc +++ b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkMinLength --string-non-empty --max-nondet-string-length 2000000000 +--function Test.checkMinLength --string-non-empty ^EXIT=10$ ^SIGNAL=0$ assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS @@ -9,5 +9,3 @@ assertion.* line 17 function java::Test.checkMinLength.*: FAILURE assertion.* line 19 function java::Test.checkMinLength.*: FAILURE -- ^Building error trace --- -max-nondet-string-length is set big enough to cause an overflow. diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h index a1644bfd93d..22616d63b51 100644 --- a/src/solvers/strings/string_refinement.h +++ b/src/solvers/strings/string_refinement.h @@ -21,7 +21,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H #include -#include #include #include #include @@ -46,8 +45,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com " --string-input-value st restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \ " the switch can be used multiple times to give\n" /* NOLINT(*) */ \ " several strings\n" /* NOLINT(*) */ \ - " --max-nondet-string-length n bound the length of nondet (e.g. input) strings;\n" /* NOLINT(*) */ \ - " set to " + std::to_string(MAX_NONDET_STRING_LENGTH_DEFAULT) + " by default\n" /* NOLINT(*) */ + " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */ // The integration of the string solver into CBMC is incomplete. Therefore, // it is not turned on by default and not all options are available. diff --git a/src/util/magic.h b/src/util/magic.h index 24fd0d1acf5..2f086f6cbff 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -16,6 +16,4 @@ const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26; // The top end of the range of integers for which dstrings are precomputed constexpr std::size_t DSTRING_NUMBERS_MAX = 64; -const int MAX_NONDET_STRING_LENGTH_DEFAULT = 10000; - #endif diff --git a/src/util/object_factory_parameters.cpp b/src/util/object_factory_parameters.cpp index a0da2a8a844..9926f6e86d9 100644 --- a/src/util/object_factory_parameters.cpp +++ b/src/util/object_factory_parameters.cpp @@ -8,9 +8,8 @@ Author: Diffblue Ltd #include "object_factory_parameters.h" -#include "cmdline.h" -#include "magic.h" -#include "options.h" +#include +#include void object_factory_parameterst::set(const optionst &options) { @@ -69,19 +68,12 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) options.set_option( "min-null-tree-depth", cmdline.get_value("min-null-tree-depth")); } - if(cmdline.isset("max-nondet-string-length")) { options.set_option( "max-nondet-string-length", cmdline.get_value("max-nondet-string-length")); } - else if(!cmdline.isset("no-refine-strings")) - { - options.set_option( - "max-nondet-string-length", MAX_NONDET_STRING_LENGTH_DEFAULT); - } - if(cmdline.isset("string-printable")) { options.set_option("string-printable", true);