Merge pull request #8109 from NlightNFotis/no_unwinding_assertions

Add support for a `--no-unwinding-assertions` flag

src/cbmc/cbmc_parse_options.cpp

@@ -120,7 +120,12 @@ void cbmc_parse_optionst::set_default_analysis_flags(
 
   // Unwinding assertions required in certain cases for sound verification
   // results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
-  options.set_option("unwinding-assertions", enabled);
+  // As the unwinding-assertions is processed earlier, we set it only if it has
+  // not been set yet.
+  if(!options.is_set("unwinding-assertions"))
+  {
+    options.set_option("unwinding-assertions", enabled);
+  }
 }
 
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
@@ -145,6 +150,35 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  // We want to warn the user that if we are using standard checks (that enables
+  // unwinding-assertions) and we did not disable them manually.
+  if(
+    cmdline.isset("cover") && !cmdline.isset("no-standard-checks") &&
+    !cmdline.isset("no-unwinding-assertions"))
+  {
+    log.warning() << "--cover is incompatible with --unwinding-assertions, so "
+                     "unwinding-assertions will be defaulted to false"
+                  << messaget::eom;
+  }
+
+  // We want to set the unwinding-assertions option as early as we can,
+  // otherwise we come across two issues: 1) there's no way to deactivate it
+  // with `--no-unwinding-assertions`, as the `--no-xxx` flags are set by
+  // `goto_check_c` which doesn't provide handling for the options, and 2) we
+  // handle it only when we use `--no-standard-checks`, but if we do so, we have
+  // already printed a couple times to the screen that `--unwinding-assertions`
+  // must be passed because of some activation/sensitive further down below.
+  if(cmdline.isset("unwinding-assertions"))
+  {
+    options.set_option("unwinding-assertions", true);
+    options.set_option("paths-symex-explore-all", true);
+  }
+  else if(cmdline.isset("no-unwinding-assertions"))
+  {
+    options.set_option("unwinding-assertions", false);
+    options.set_option("paths-symex-explore-all", false);
+  }
+
   if(cmdline.isset("max-field-sensitivity-array-size"))
   {
     options.set_option(
@@ -340,15 +374,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
-  // generate unwinding assertions
-  if(
-    options.get_bool_option("unwinding-assertions") ||
-    cmdline.isset("unwinding-assertions"))
-  {
-    options.set_option("unwinding-assertions", true);
-    options.set_option("paths-symex-explore-all", true);
-  }
-
   if(cmdline.isset("partial-loops"))
   {
     options.set_option("partial-loops", true);