Add --cover-failed-assertions option

This adds an option `--cover-failed-assertions` that prevents the
default behaviour of coverage stopping at failed assertions by turning
assertions into skips rather than assumes (which is the default
behaviour for coverage criteria other than `assertion`, which behaves
the same with or without the flag).

Author: hannes-steffenhagen-diffblue

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--cover location --pointer-check --malloc-may-fail --malloc-fail-null
+\[main.coverage.4\] file test.c line \d+ function main block 4 \(lines test.c:main:12,13\): SATISFIED
+\[main.coverage.3\] file test.c line \d+ function main block 3 \(lines test.c:main:10\): FAILED
+\[main.coverage.2\] file test.c line \d+ function main block 2 \(lines test.c:main:4,5,7,9\): SATISFIED
+\[main.coverage.1\] file test.c line \d+ function main block 1 \(lines test.c:main:4\): SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/cover-failed-assertions/test.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *ptr = malloc(sizeof(*ptr));
+  int a;
+
+  a = *ptr;
+
+  if(ptr == NULL)
+    a = 1;
+
+  return 0;
+}

regression/cbmc/cover-failed-assertions/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null
+\[main.coverage.4\] file test.c line \d+ function main block 4 \(lines test.c:main:12,13\): SATISFIED
+\[main.coverage.3\] file test.c line \d+ function main block 3 \(lines test.c:main:10\): SATISFIED
+\[main.coverage.2\] file test.c line \d+ function main block 2 \(lines test.c:main:4,5,7,9\): SATISFIED
+\[main.coverage.1\] file test.c line \d+ function main block 1 \(lines test.c:main:4\): SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-instrument/cover.cpp

@@ -164,6 +164,8 @@ void parse_cover_options(const cmdlinet &cmdline, optionst &options)
   options.set_option(
     "cover-traces-must-terminate",
     cmdline.isset("cover-traces-must-terminate"));
+  options.set_option(
+    "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
 }
 
 /// Build data structures controlling coverage from command-line options.
@@ -223,6 +225,9 @@ cover_configt get_cover_config(
   cover_config.traces_must_terminate =
     options.get_bool_option("cover-traces-must-terminate");
 
+  cover_config.cover_failed_assertions =
+    options.get_bool_option("cover-failed-assertions");
+
   return cover_config;
 }
 
@@ -285,16 +290,22 @@ static void instrument_cover_goals(
       // Simplify the common case where we have ASSERT(x); ASSUME(x):
       if(i_it->is_assert())
       {
-        auto successor = std::next(i_it);
-        if(
-          successor != function.body.instructions.end() &&
-          successor->is_assume() &&
-          successor->get_condition() == i_it->get_condition())
+        if(!cover_config.cover_failed_assertions)
         {
-          successor->turn_into_skip();
+          auto successor = std::next(i_it);
+          if(
+            successor != function.body.instructions.end() &&
+            successor->is_assume() &&
+            successor->get_condition() == i_it->get_condition())
+          {
+            successor->turn_into_skip();
+          }
+          i_it->type = goto_program_instruction_typet::ASSUME;
+        }
+        else
+        {
+          i_it->turn_into_skip();
         }
-
-        i_it->type = goto_program_instruction_typet::ASSUME;
       }
     }
   }

src/goto-instrument/cover.h

@@ -22,9 +22,17 @@ class message_handlert;
 class cmdlinet;
 class optionst;
 
-#define OPT_COVER "(cover):"
-#define HELP_COVER \
-  " --cover CC                   create test-suite with coverage criterion CC\n"
+#define OPT_COVER                                                              \
+  "(cover):"                                                                   \
+  "(cover-failed-assertions)"
+
+#define HELP_COVER                                                             \
+  " --cover CC                   create test-suite with coverage criterion "   \
+  "CC\n"                                                                       \
+  " --cover-failed-assertions    do not stop coverage checking at failed "     \
+  "assertions\n"                                                               \
+  "                              (this is the default for --cover "            \
+  "assertions)\n"
 
 enum class coverage_criteriont
 {
@@ -41,6 +49,7 @@ enum class coverage_criteriont
 struct cover_configt
 {
   bool keep_assertions;
+  bool cover_failed_assertions;
   bool traces_must_terminate;
   irep_idt mode;
   function_filterst function_filters;