[WIP] Enable default flags on for checks

Author: NlightNFotis

src/ansi-c/goto_check_c.h

@@ -79,21 +79,21 @@ void goto_check_c(
 
 // clang-format off
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
-  options.set_option("bounds-check", cmdline.isset("bounds-check")); \
-  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
+  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("div-by-zero-check")); \
+  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("signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \
+  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("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
+  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("pointer-primitive-check")); /* 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) */ \

src/cbmc/cbmc_parse_options.cpp

@@ -93,6 +93,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
 
 void cbmc_parse_optionst::set_default_options(optionst &options)
 {
+  // Enable the standard checks by default, unless a user overrides.
+  options.set_option("standard-checks", true);
+
   // Default true
   options.set_option("built-in-assertions", true);
   options.set_option("propagation", true);
@@ -107,6 +110,20 @@ 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)
+{
+  // Analysis flags on by default
+  options.set_option("bounds-check", true);
+  options.set_option("pointer-check", true);
+  options.set_option("pointer-primitive-check", true);
+  options.set_option("malloc-may-fail", true);
+  // TODO: Default malloc-fail-profile
+  options.set_option("div-by-zero-check", true);
+  options.set_option("signed-overflow-check", true);
+  options.set_option("undefined-shift-check", true);
+  options.set_option("unwinding-assertions", true);
+}
+
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -118,6 +135,11 @@ 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"));
 
@@ -310,8 +332,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // generate unwinding assertions
-  if(cmdline.isset("unwinding-assertions"))
+  // TODO: Fotis: revisit
+  if(cmdline.isset("no-unwinding-assertions"))
   {
+    options.set_option("unwinding-assertions", false);
+    options.set_option("paths-symex-explore-all", false);
+  } else {
+    // Not really needed, as it's now on by default, but keeping it here
+    // for completeness' sake.
     options.set_option("unwinding-assertions", true);
     options.set_option("paths-symex-explore-all", true);
   }

src/cbmc/cbmc_parse_options.h

@@ -33,7 +33,8 @@ class optionst;
 
 // clang-format off
 #define CBMC_OPTIONS \
-  OPT_BMC \
+  OPT_BMC            \
+  "(standard-checks)" \
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
@@ -90,6 +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 bool process_goto_program(goto_modelt &, const optionst &, messaget &);