Factor out default CBMC options to static method

CBMC parse options that have default values are all set in a single
place---a static method that may also be called from any client that
needs to emulate CBMC's default options (e.g. unit tests). Previous to
this commit, there were a lot of

    if(cmdline.isset("no-foo"))
      options.set_option("foo", false);
    else
      options.set_option("foo", true);

This commit removes all the else cases.

Author: karkhaz

src/cbmc/cbmc_parse_options.cpp

@@ -85,6 +85,28 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
 {
 }
 
+void cbmc_parse_optionst::set_default_options(optionst &options)
+{
+  // Default true
+  options.set_option("assertions", true);
+  options.set_option("assumptions", true);
+  options.set_option("built-in-assertions", true);
+  options.set_option("pretty-names", true);
+  options.set_option("propagation", true);
+  options.set_option("sat-preprocessor", true);
+  options.set_option("simplify", true);
+  options.set_option("simplify-if", true);
+
+  // Default false
+  options.set_option("partial-loops", false);
+  options.set_option("slice-formula", false);
+  options.set_option("stop-on-fail", false);
+  options.set_option("unwinding-assertions", false);
+
+  // Other
+  options.set_option("arrays-uf", "auto");
+}
+
 void cbmc_parse_optionst::eval_verbosity()
 {
   // this is our default verbosity
@@ -108,6 +130,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  cbmc_parse_optionst::set_default_options(options);
+
   if(cmdline.isset("paths"))
     options.set_option("paths", true);
 
@@ -143,15 +167,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
-  else
-    options.set_option("simplify", true);
 
   if(cmdline.isset("stop-on-fail") ||
      cmdline.isset("dimacs") ||
      cmdline.isset("outfile"))
     options.set_option("stop-on-fail", true);
-  else
-    options.set_option("stop-on-fail", false);
 
   if(cmdline.isset("trace") ||
      cmdline.isset("stop-on-fail"))
@@ -184,43 +204,36 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   // constant propagation
   if(cmdline.isset("no-propagation"))
     options.set_option("propagation", false);
-  else
-    options.set_option("propagation", true);
 
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
     options.set_option("assertions", false);
-  else
-    options.set_option("assertions", true);
 
   // use assumptions
   if(cmdline.isset("no-assumptions"))
     options.set_option("assumptions", false);
-  else
-    options.set_option("assumptions", true);
 
   // magic error label
   if(cmdline.isset("error-label"))
     options.set_option("error-label", cmdline.get_values("error-label"));
 
   // generate unwinding assertions
-  if(cmdline.isset("cover"))
-    options.set_option("unwinding-assertions", false);
-  else
+  if(cmdline.isset("unwinding-assertions"))
+    options.set_option("unwinding-assertions", true);
+
+  if(cmdline.isset("partial-loops"))
+    options.set_option("partial-loops", true);
+
+  if(options.is_set("cover") && options.get_bool_option("unwinding-assertions"))
   {
-    options.set_option(
-      "unwinding-assertions",
-      cmdline.isset("unwinding-assertions"));
+    error() << "--cover and --unwinding-assertions "
+            << "must not be given together" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
-  // generate unwinding assumptions otherwise
-  options.set_option(
-    "partial-loops",
-    cmdline.isset("partial-loops"));
-
   if(options.get_bool_option("partial-loops") &&
      options.get_bool_option("unwinding-assertions"))
   {
@@ -230,22 +243,17 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   // remove unused equations
-  options.set_option(
-    "slice-formula",
-    cmdline.isset("slice-formula"));
+  if(cmdline.isset("slice-formula"))
+    options.set_option("slice-formula", true);
 
   // simplify if conditions and branches
   if(cmdline.isset("no-simplify-if"))
     options.set_option("simplify-if", false);
-  else
-    options.set_option("simplify-if", true);
 
   if(cmdline.isset("arrays-uf-always"))
     options.set_option("arrays-uf", "always");
   else if(cmdline.isset("arrays-uf-never"))
     options.set_option("arrays-uf", "never");
-  else
-    options.set_option("arrays-uf", "auto");
 
   if(cmdline.isset("dimacs"))
     options.set_option("dimacs", true);
@@ -387,12 +395,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("no-sat-preprocessor"))
     options.set_option("sat-preprocessor", false);
-  else
-    options.set_option("sat-preprocessor", true);
 
-  options.set_option(
-    "pretty-names",
-    !cmdline.isset("no-pretty-names"));
+  if(cmdline.isset("no-pretty-names"))
+    options.set_option("pretty-names", false);
 
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));

src/cbmc/cbmc_parse_options.h

@@ -91,6 +91,12 @@ class cbmc_parse_optionst:
     const char **argv,
     const std::string &extra_options);
 
+  /// \brief Set the options that have default values
+  ///
+  /// This function can be called from clients that wish to emulate CBMC's
+  /// default behaviour, for example unit tests.
+  static void set_default_options(optionst &);
+
 protected:
   goto_modelt goto_model;
   ui_message_handlert ui_message_handler;