Remove --string-max-input-length from JBMC

Author: peterschrammel

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -75,11 +75,6 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
       safe_string2size_t(cmd.get_value("max-nondet-tree-depth"));
   }
 
-  if(cmd.isset("string-max-input-length")) // will go away
-  {
-    object_factory_parameters.max_nondet_string_length =
-      safe_string2size_t(cmd.get_value("string-max-input-length"));
-  }
   if(cmd.isset("max-nondet-string-length"))
   {
     object_factory_parameters.max_nondet_string_length =

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -491,9 +491,7 @@ int jbmc_parse_optionst::doit()
   object_factory_params.max_nondet_string_length =
     cmdline.isset("max-nondet-string-length")
       ? std::stoul(cmdline.get_value("max-nondet-string-length"))
-      : cmdline.isset("string-max-input-length") // obsolete; will go away
-        ? std::stoul(cmdline.get_value("string-max-input-length"))
-        : MAX_NONDET_STRING_LENGTH;
+      : MAX_NONDET_STRING_LENGTH;
   object_factory_params.max_nondet_tree_depth =
     cmdline.isset("java-max-input-tree-depth")
       ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))

jbmc/src/jbmc/jbmc_parse_options.h

@@ -54,7 +54,6 @@ class optionst;
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(no-refine-strings)" \
   "(string-printable)" \
-  "(string-max-input-length):" /* will go away */ \
   "(max-nondet-string-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \

src/solvers/refinement/string_refinement.cpp

@@ -924,7 +924,7 @@ static optionalt<exprt> get_array(
   {
     stream << "(sr::get_array) long string (size " << format(arr.length())
            << " = " << n << ") " << format(arr) << eom;
-    stream << "(sr::get_array) consider reducing string-max-input-length so "
+    stream << "(sr::get_array) consider reducing max-nondet-string-length so "
               "that no string exceeds "
            << MAX_CONCRETE_STRING_SIZE
            << " in length and "