Group default options into own DEFINE

Author: NlightNFotis

src/ansi-c/goto_check_c.h

@@ -38,7 +38,7 @@ void goto_check_c(
   message_handlert &message_handler);
 
 #define OPT_GOTO_CHECK                                                         \
-  "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
+  "(no-bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
   "(div-by-zero-check)(enum-range-check)"                                      \
   "(signed-overflow-check)(unsigned-overflow-check)"                           \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
@@ -77,31 +77,36 @@ void goto_check_c(
   " {y--no-assumptions} \t ignore user assumptions\n"                          \
   " {y--assert-to-assume} \t convert user assertions to assumptions\n"
 
+// clang-format off
+#define PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options) \
+    options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \
+    options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \
+    options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \
+    options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
+    options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
+    options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+    (void) 0;
+// clang-format on
+
 // clang-format off
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
-  options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \
-  options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \
   options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
   options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \
   options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
-  options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("conversion-check", cmdline.isset("conversion-check")); \
-  options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
   options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("retain-trivial-checks", \
-                     cmdline.isset("retain-trivial-checks")); \
   options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("retain-trivial-checks", \
+                     cmdline.isset("retain-trivial-checks")); \
   options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
   if(cmdline.isset("error-label")) \
-    options.set_option("error-label", cmdline.get_values("error-label")); \
+    options.set_option("error-label", cmdline.get_values("error-label"));      \
   (void)0
 // clang-format on
 

src/cbmc/cbmc_parse_options.cpp

@@ -110,7 +110,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("depth", UINT32_MAX);
 }
 
-void cbmc_parse_optionst::set_soundness_on_by_default(optionst &options)
+void cbmc_parse_optionst::set_default_analysis_flags(optionst &options)
 {
   // Analysis flags on by default
   options.set_option("bounds-check", true);
@@ -135,11 +135,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   cbmc_parse_optionst::set_default_options(options);
   parse_c_object_factory_options(cmdline, options);
 
-  // Enable flags that in combination provide analysis with no surprises
-  // (expected checks and no unsoundness by missing checks).
-  if (options.get_bool_option("standard-checks"))
-    set_soundness_on_by_default(options);
-
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
@@ -328,7 +323,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // all checks supported by goto_check
+  // Enable flags that in combination provide analysis with no surprises
+  // (expected checks and no unsoundness by missing checks).
+  if (!cmdline.isset("no-standard-checks") && options.get_bool_option("standard-checks"))
+    set_default_analysis_flags(options);
+  else
+    PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options);
+
+  // all (non-default) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // generate unwinding assertions

src/cbmc/cbmc_parse_options.h

@@ -34,7 +34,7 @@ class optionst;
 // clang-format off
 #define CBMC_OPTIONS \
   OPT_BMC            \
-  "(standard-checks)" \
+  "(no-standard-checks)" \
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
@@ -91,7 +91,7 @@ class cbmc_parse_optionst : public parse_options_baset
   /// 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 &);
-  static void set_soundness_on_by_default(optionst &options);
+  static void set_default_analysis_flags(optionst &options);
 
   static bool process_goto_program(goto_modelt &, const optionst &, messaget &);