# This is a combination of 2 commits.

# This is the 1st commit message:

Adding options to cbmc for parameters of the string solver

We add the options string-max-length, string-non-empty, and string-printable

# The commit message #2 will be skipped:

#	fixup! Adding options to cbmc for parameters of the string solver

Author: romainbrenguier

src/cbmc/cbmc_parse_options.cpp

@@ -291,7 +291,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("string-refine"))
   {
-    options.set_option("string-refine", true);
+    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(
+        "string-max-length", cmdline.get_value("string-max-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))

src/cbmc/cbmc_parse_options.h

@@ -41,7 +41,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(string-refine)" \
+  "(refine-strings)(string-non-empty)(string-printable)(string-max-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

src/cbmc/cbmc_solvers.cpp

@@ -172,6 +172,16 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
   string_refinementt *string_refinement=new string_refinementt(
     ns, *prop, MAX_NB_REFINEMENT);
   string_refinement->set_ui(ui);
+
+  string_refinement->do_concretizing=options.get_bool_option("trace");
+  if(options.get_bool_option("string-max-length"))
+    string_refinement->set_max_string_length(
+      options.get_signed_int_option("string-max-length"));
+  if(options.get_bool_option("string-non-empty"))
+    string_refinement->enforce_non_empty_string();
+  if(options.get_bool_option("string-printable"))
+    string_refinement->enforce_printable_characters();
+
   return new solvert(string_refinement, prop);
 }