Merge pull request #4660 from diffblue/revert-4643-max-nondet-string-length-default

Revert "Set max-nondet-string-length to 10000 by default"

Author: tautschnig

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.

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -1,11 +1,10 @@
 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\)
 --
 --
 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.

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.

src/solvers/strings/string_refinement.h

@@ -21,7 +21,6 @@ Author: Alberto Griggio, [email protected]
 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
 
 #include <limits>
-#include <util/magic.h>
 #include <util/replace_expr.h>
 #include <util/string_expr.h>
 #include <util/union_find_replace.h>
@@ -46,8 +45,7 @@ Author: Alberto Griggio, [email protected]
   " --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.

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

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 <util/cmdline.h>
+#include <util/options.h>
 
 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);