Use defines for string options and help text

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1084,9 +1084,7 @@ void jbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --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 n bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
+    HELP_STRING_REFINEMENT
     " --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(*)

jbmc/src/jbmc/jbmc_parse_options.h

@@ -29,6 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/path_storage.h>
 
+#include <solvers/refinement/string_refinement.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 
 class bmct;
@@ -52,9 +54,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(no-refine-strings)" \
-  "(string-printable)" \
-  "(max-nondet-string-length):" \
+  OPT_STRING_REFINEMENT \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_CLASS_HIERARCHY \

jbmc/src/jbmc/module_dependencies.txt

@@ -9,4 +9,5 @@ jbmc
 langapi # should go away
 linking
 pointer-analysis
+solvers/refinement
 util

src/cbmc/cbmc_parse_options.cpp

@@ -959,8 +959,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --refine-strings             use string refinement (experimental)\n"
-    " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
+    HELP_STRING_REFINEMENT_CBMC
     " --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

@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_trace.h>
 
+#include <solvers/refinement/string_refinement.h>
+
 #include "bmc.h"
 #include "xml_interface.h"
 #include "cbmc_solvers.h"
@@ -48,8 +50,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
-  "(string-printable)" \
+  OPT_STRING_REFINEMENT_CBMC \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \

src/solvers/refinement/string_refinement.h

@@ -29,6 +29,28 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_refinement_util.h>
 
+// clang-format off
+#define OPT_STRING_REFINEMENT \
+  "(no-refine-strings)" \
+  "(string-printable)" \
+  "(max-nondet-string-length):"
+
+#define HELP_STRING_REFINEMENT \
+  " --no-refine-strings          turn off string refinement\n" \
+  " --string-printable           restrict to printable strings (experimental)\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.
+#define OPT_STRING_REFINEMENT_CBMC \
+  "(refine-strings)" \
+  "(string-printable)"
+
+#define HELP_STRING_REFINEMENT_CBMC \
+  " --refine-strings             use string refinement (experimental)\n" \
+  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */
+// clang-format on
+
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 
 class string_refinementt final: public bv_refinementt