Merge pull request #1729 from romainbrenguier/refactor/unused-nonempty-option

Remove the string-non-empty function which had no effect

Author: martin-cs

src/cbmc/cbmc_parse_options.cpp

@@ -271,7 +271,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
-    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
     options.set_option("string-printable", cmdline.isset("string-printable"));
     if(cmdline.isset("string-max-length"))
       options.set_option(
@@ -1009,7 +1008,6 @@ void cbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
-    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
     " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -44,7 +44,6 @@ class optionst;
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
-  "(string-non-empty)" \
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \

src/cbmc/cbmc_solvers.cpp

@@ -178,7 +178,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.ui=ui;
   if(options.get_bool_option("string-max-length"))
     info.string_max_length=options.get_signed_int_option("string-max-length");
-  info.string_non_empty=options.get_bool_option("string-non-empty");
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=

src/jbmc/jbmc_parse_options.cpp

@@ -246,7 +246,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
-    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
     options.set_option("string-printable", cmdline.isset("string-printable"));
     if(cmdline.isset("string-max-length"))
       options.set_option(
@@ -912,7 +911,6 @@ void jbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
-    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
     " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)

src/jbmc/jbmc_parse_options.h

@@ -44,7 +44,6 @@ class optionst;
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
-  "(string-non-empty)" \
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \

src/solvers/refinement/string_refinement.h

@@ -49,8 +49,6 @@ class string_refinementt final: public bv_refinementt
   struct configt
   {
     std::size_t refinement_bound=0;
-    /// Make non-deterministic character arrays have at least one character
-    bool string_non_empty=false;
     /// Concretize strings after solver is finished
     bool trace=false;
     bool use_counter_example=true;