Remove obsolete string options from CBMC

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1087,7 +1087,7 @@ void jbmc_parse_optionst::help()
     " --refine                     use refinement procedure (experimental)\n"
     " --no-refine-strings          turn off string refinement\n"
     " --string-printable           restrict to printable strings (experimental)\n" // NOLINT(*)
-    " --max-nondet-string-length   bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
+    " --max-nondet-string-length n 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(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.cpp

@@ -300,9 +300,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
-    if(cmdline.isset("string-max-length"))
-      options.set_option(
-        "string-max-length", cmdline.get_value("string-max-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -964,9 +961,6 @@ void cbmc_parse_optionst::help()
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
-    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
-    " --string-max-length          add constraint on the length of strings\n"
-    "                              (deprecated: use string-max-input-length instead)\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -50,8 +50,6 @@ class optionst;
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
   "(string-printable)" \
-  "(string-max-length):" \
-  "(string-max-input-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \