[FIXUP] Add missing no-div-by-zero check and eliminate standard checks option

Author: NlightNFotis

src/ansi-c/goto_check_c.h

@@ -49,7 +49,7 @@ void goto_check_c(
   "(no-assertions)(no-assumptions)"                                            \
   "(assert-to-assume)"                                                         \
   "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
-  "(no-pointer-primitive-check)(no-undefined-shift-check)"
+  "(no-pointer-primitive-check)(no-undefined-shift-check)(no-div-by-zero-check)"
 
 #define HELP_GOTO_CHECK                                                        \
   " {y--bounds-check} \t enable array bounds checks\n"                         \

src/cbmc/cbmc_parse_options.cpp

@@ -92,9 +92,6 @@ ::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);
@@ -137,13 +134,16 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   cbmc_parse_optionst::set_default_options(options);
-  cbmc_parse_optionst::set_default_analysis_flags(options);
   parse_c_object_factory_options(cmdline, options);
 
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
+  if(
+    cmdline.isset("cover") &&
+    // The option is set by default, or passed in the by the user.
+    (options.is_set("unwinding-assertions") ||
+     cmdline.isset("unwinding-assertions")))
   {
     log.error()
       << "--cover and --unwinding-assertions must not be given together"
@@ -284,7 +284,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwind"))
   {
     options.set_option("unwind", cmdline.get_value("unwind"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(
+      !options.is_set("unwinding-assertions") &&
+      !cmdline.isset("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -311,7 +313,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option(
       "unwindset", cmdline.get_comma_separated_values("unwindset"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(
+      !options.is_set("unwinding-assertions") &&
+      !cmdline.isset("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -330,11 +334,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   // 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"))
+  if(!cmdline.isset("no-standard-checks"))
   {
-    set_default_analysis_flags(options);
+    cbmc_parse_optionst::set_default_analysis_flags(options);
     PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options);
   }
   else if(cmdline.isset("no-standard-checks"))
@@ -346,7 +348,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // generate unwinding assertions
-  if(cmdline.isset("unwinding-assertions"))
+  if(
+    options.is_set("unwinding-assertions") ||
+    cmdline.isset("unwinding-assertions"))
   {
     options.set_option("unwinding-assertions", true);
     options.set_option("paths-symex-explore-all", true);