Move the declaration and description of options that configt handles into config.h

.gitignore

@@ -61,6 +61,7 @@ regression/**/tests-*.log
 regression/**/*.goto-cc-saved
 regression/**/*.gb
 regression/**/*.smt2
+regression/solver-hardness/solver-hardness-simple/solver_hardness.json
 jbmc/regression/**/tests.log
 jbmc/regression/**/tests-symex-driven-loading.log
 

scripts/expected_doxygen_warnings.txt

@@ -84,7 +84,7 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/cbmc/cbmc_parse_options.cpp

@@ -203,9 +203,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("mm"))
     options.set_option("mm", cmdline.get_value("mm"));
 
-  if(cmdline.isset("c89"))
-    config.ansi_c.set_c89();
-
   if(cmdline.isset("symex-complexity-limit"))
     options.set_option(
       "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
@@ -215,21 +212,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       "symex-complexity-failed-child-loops-limit",
       cmdline.get_value("symex-complexity-failed-child-loops-limit"));
 
-  if(cmdline.isset("c99"))
-    config.ansi_c.set_c99();
-
-  if(cmdline.isset("c11"))
-    config.ansi_c.set_c11();
-
-  if(cmdline.isset("cpp98"))
-    config.cpp.set_cpp98();
-
-  if(cmdline.isset("cpp03"))
-    config.cpp.set_cpp03();
-
-  if(cmdline.isset("cpp11"))
-    config.cpp.set_cpp11();
-
   if(cmdline.isset("property"))
     options.set_option("property", cmdline.get_values("property"));
 
@@ -1016,46 +998,14 @@ void cbmc_parse_optionst::help()
     "                              (implies --trace)\n"
     "\n"
     "C/C++ frontend options:\n"
-    " -I path                      set include path (C/C++)\n"
-    " -D macro                     define preprocessor macro (C/C++)\n"
     " --preprocess                 stop after preprocessing\n"
-    " --16, --32, --64             set width of int\n"
-    " --LP64, --ILP64, --LLP64,\n"
-    "   --ILP32, --LP32            set width of int, long and pointers\n"
-    " --little-endian              allow little-endian word-byte conversions\n"
-    " --big-endian                 allow big-endian word-byte conversions\n"
-    " --unsigned-char              make \"char\" unsigned by default\n"
-    " --mm model                   set memory model (default: sc)\n"
-    " --arch                       set architecture (default: "
-                                   << configt::this_architecture() << ")\n"
-    " --os                         set operating system (default: "
-                                   << configt::this_operating_system() << ")\n"
-    " --c89/99/11                  set C language standard (default: "
-                                   << (configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C89?"c89":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C99?"c99":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
-    " --cpp98/03/11                set C++ language standard (default: "
-                                   << (configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
-    #ifdef _WIN32
-    " --gcc                        use GCC as preprocessor\n"
-    #endif
-    " --no-arch                    don't set up an architecture\n"
-    " --no-library                 disable built-in abstract C library\n"
-    " --round-to-nearest           rounding towards nearest even (default)\n"
-    " --round-to-plus-inf          rounding towards plus infinity\n"
-    " --round-to-minus-inf         rounding towards minus infinity\n"
-    " --round-to-zero              rounding towards zero\n"
+    HELP_CONFIG_C_CPP
     HELP_ANSI_C_LANGUAGE
     HELP_FUNCTIONS
     "\n"
+    "Platform options:\n"
+    HELP_CONFIG_PLATFORM
+    "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show loaded symbol table\n"
@@ -1064,12 +1014,8 @@ void cbmc_parse_optionst::help()
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     HELP_COVER
-    " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --malloc-fail-assert         set malloc failure mode to assert-then-assume\n"
-    " --malloc-fail-null           set malloc failure mode to return null\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --malloc-may-fail            allow malloc calls to return a null pointer\n"
+    " --mm MM                      memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
+    HELP_CONFIG_LIBRARY
     HELP_REACHABILITY_SLICER
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
@@ -1086,7 +1032,7 @@ void cbmc_parse_optionst::help()
     HELP_BMC
     "\n"
     "Backend options:\n"
-    " --object-bits n              number of bits used for object addresses\n"
+    HELP_CONFIG_BACKEND
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
     " --localize-faults            localize faults (experimental)\n"

src/cbmc/cbmc_parse_options.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 
+#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -50,11 +51,11 @@ class optionst;
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "(write-solver-stats-to):"  \
   "(show-array-constraints)"  \
-  "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
-  "(object-bits):" \
+  OPT_CONFIG_C_CPP \
+  OPT_CONFIG_PLATFORM \
+  OPT_CONFIG_BACKEND \
+  OPT_CONFIG_LIBRARY \
   OPT_GOTO_CHECK \
-  "(malloc-fail-assert)(malloc-fail-null)" \
-  "(malloc-may-fail)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
@@ -64,8 +65,6 @@ class optionst;
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   OPT_STRING_REFINEMENT_CBMC \
-  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
-  "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \
@@ -79,11 +78,7 @@ class optionst;
   "(symex-coverage-report):" \
   "(mm):" \
   OPT_TIMESTAMP \
-  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
-  "(ppc-macos)(unsigned-char)" \
   "(arrays-uf-always)(arrays-uf-never)" \
-  "(string-abstraction)(no-arch)(arch):" \
-  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   OPT_FLUSH \
   "(localize-faults)" \
   OPT_GOTO_TRACE \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -101,26 +101,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-#if 0
-  if(cmdline.isset("c89"))
-    config.ansi_c.set_c89();
-
-  if(cmdline.isset("c99"))
-    config.ansi_c.set_c99();
-
-  if(cmdline.isset("c11"))
-    config.ansi_c.set_c11();
-
-  if(cmdline.isset("cpp98"))
-    config.cpp.set_cpp98();
-
-  if(cmdline.isset("cpp03"))
-    config.cpp.set_cpp03();
-
-  if(cmdline.isset("cpp11"))
-    config.cpp.set_cpp11();
-#endif
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
@@ -962,36 +942,12 @@ void goto_analyzer_parse_optionst::help()
     " --taint file_name            perform taint analysis using rules in given file\n"
     "\n"
     "C/C++ frontend options:\n"
-    " -I path                      set include path (C/C++)\n"
-    " -D macro                     define preprocessor macro (C/C++)\n"
-    " --arch X                     set architecture (default: "
-                                   << configt::this_architecture() << ")\n"
-    " --os                         set operating system (default: "
-                                   << configt::this_operating_system() << ")\n"
-    " --c89/99/11                  set C language standard (default: "
-                                   << (configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C89?"c89":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C99?"c99":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C11?
-                                         "c11":"") << ")\n"
-    " --cpp98/03/11                set C++ language standard (default: "
-                                   << (configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP98?
-                                         "cpp98":
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP03?
-                                         "cpp03":
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP11?
-                                         "cpp11":"") << ")\n"
-    #ifdef _WIN32
-    " --gcc                        use GCC as preprocessor\n"
-    #endif
-    " --no-library                 disable built-in abstract C library\n"
+    HELP_CONFIG_C_CPP
     HELP_FUNCTIONS
     "\n"
+    "Platform options:\n"
+    HELP_CONFIG_PLATFORM
+    "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show loaded symbol table\n"
@@ -1000,6 +956,7 @@ void goto_analyzer_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
+    HELP_CONFIG_LIBRARY
     "\n"
     "Other options:\n"
     HELP_VALIDATE

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -89,6 +89,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
+#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -157,18 +158,15 @@ class optionst;
 
 #define GOTO_ANALYSER_OPTIONS \
   OPT_FUNCTIONS \
-  "D:I:(std89)(std99)(std11)" \
-  "(classpath):(cp):(main-class):" \
-  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
-  "(little-endian)(big-endian)" \
+  OPT_CONFIG_C_CPP \
+  OPT_CONFIG_PLATFORM \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
   "(show-reachable-properties)(property):" \
   "(verbosity):(version)" \
-  "(gcc)(arch):" \
   OPT_FLUSH \
   OPT_TIMESTAMP \
   OPT_VALIDATE \

src/goto-diff/goto_diff_parse_options.cpp

@@ -97,24 +97,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("mm"))
     options.set_option("mm", cmdline.get_value("mm"));
 
-  if(cmdline.isset("c89"))
-    config.ansi_c.set_c89();
-
-  if(cmdline.isset("c99"))
-    config.ansi_c.set_c99();
-
-  if(cmdline.isset("c11"))
-    config.ansi_c.set_c11();
-
-  if(cmdline.isset("cpp98"))
-    config.cpp.set_cpp98();
-
-  if(cmdline.isset("cpp03"))
-    config.cpp.set_cpp03();
-
-  if(cmdline.isset("cpp11"))
-    config.cpp.set_cpp11();
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

src/util/config.cpp

@@ -1127,6 +1127,24 @@ bool configt::set(const cmdlinet &cmdline)
 
   ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
 
+  if(cmdline.isset("c89"))
+    ansi_c.set_c89();
+
+  if(cmdline.isset("c99"))
+    ansi_c.set_c99();
+
+  if(cmdline.isset("c11"))
+    ansi_c.set_c11();
+
+  if(cmdline.isset("cpp98"))
+    cpp.set_cpp98();
+
+  if(cmdline.isset("cpp03"))
+    cpp.set_cpp03();
+
+  if(cmdline.isset("cpp11"))
+    cpp.set_cpp11();
+
   return false;
 }