diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 627d324152d..e84e0d96599 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -367,7 +367,7 @@ void jdiff_parse_optionst::help() "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK - " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + HELP_COVER "Java Bytecode frontend options:\n" JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP "Other options:\n" diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index c5d4fe736f4..9dd5b49b63d 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -23,6 +23,8 @@ Author: Peter Schrammel #include #include +#include + class goto_modelt; // clang-format off @@ -31,7 +33,7 @@ class goto_modelt; OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ - "(cover):" \ + OPT_COVER \ "(verbosity):(version)" \ "(no-lazy-methods)" /* should go away */ \ "(no-refine-strings)" /* should go away */ \ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc new file mode 100644 index 00000000000..0544dcdb715 --- /dev/null +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -0,0 +1,14 @@ +CORE paths-lifo-expected-failure +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:17,18\): SATISFIED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED +\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED +\[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This is checking that without the --cover-failed-assertions flag we still get the same result as we did before adding +it in this example. diff --git a/regression/cbmc/cover-failed-assertions/test.c b/regression/cbmc/cover-failed-assertions/test.c new file mode 100644 index 00000000000..61c894cf382 --- /dev/null +++ b/regression/cbmc/cover-failed-assertions/test.c @@ -0,0 +1,18 @@ +#include + +int main() +{ + int *ptr = malloc(sizeof(*ptr)); + int a; + + // pointer check would detect the dereference of a null pointer here + // default --cover lines behaviour is to treat non-cover assertions as + // assumptions instead, so in the ptr == NULL case we don't get past this line + // leading to failed coverage for the body of the if statement down below + a = *ptr; + + if(ptr == NULL) + a = 1; + + return 0; +} diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc new file mode 100644 index 00000000000..2b07b32fe2d --- /dev/null +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -0,0 +1,13 @@ +CORE paths-lifo-expected-failure +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:17,18\): SATISFIED +\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): SATISFIED +\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED +\[main.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This is checking that the if statement body can actually be covered with the new flag diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 374502139f9..d4ee217ae04 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -34,6 +34,9 @@ ['unknown-argument-suggestion', 'test.desc'], # this one produces XML intermingled with main XML output when used with --xml-ui ['graphml_witness2', 'test.desc'], + # these are producing coverage goals which aren't included in the schema + ['cover-failed-assertions', 'test.desc'], + ['cover-failed-assertions', 'test-no-failed-assertions.desc'], # produces intermingled XML on the command line ['coverage_report1', 'test.desc'], ['coverage_report1', 'paths.desc'], diff --git a/src/cbmc/README.md b/src/cbmc/README.md index 32fccb387f2..947987d920e 100644 --- a/src/cbmc/README.md +++ b/src/cbmc/README.md @@ -76,13 +76,15 @@ by other mechanism may categorise their properties differently. ### Coverage mode -There is one further BMC mode that differs more fundamentally: when `--cover` is -passed, assertions in the program text are converted into assumptions (these +There is one further BMC mode that differs more fundamentally: when `--cover` +is passed, assertions in the program text are converted into assumptions (these must hold for control flow to proceed past them, but are not goals for the -equation solver), while new `assert(false)` statements are added throughout the -source program representing coverage goals. The equation solving process then -proceeds the same as in all-properties mode. Coverage solving is implemented by -`bmc_covert`, but is structurally practically identical to +equation solver; In cases where this behaviour is undesirable you can pass the +`--cover-failed-assertions` which makes coverage checking continue even for +paths where assertions fail), while new `assert(false)` statements are added +throughout the source program representing coverage goals. The equation solving +process then proceeds the same as in all-properties mode. Coverage solving is +implemented by `bmc_covert`, but is structurally practically identical to `bmc_all_propertiest`-- only the reporting differs (goals are called "covered" rather than "failed"). diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cf1c034c6a2..7f378685f0d 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1118,7 +1118,7 @@ void cbmc_parse_optionst::help() " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" - " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + HELP_COVER " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) // NOLINTNEXTLINE(whitespace/line_length) " --malloc-fail-assert set malloc failure mode to assert-then-assume\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 78a7822f289..af9e265f782 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -34,6 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + class goto_functionst; class optionst; @@ -74,7 +76,8 @@ class optionst; "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ "(version)" \ - "(cover):(symex-coverage-report):" \ + OPT_COVER \ + "(symex-coverage-report):" \ "(mm):" \ OPT_TIMESTAMP \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index dbde87f5afe..f0478bd24c4 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -411,7 +411,7 @@ void goto_diff_parse_optionst::help() "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK - " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + HELP_COVER "Other options:\n" " --version show version and exit\n" " --json-ui use JSON-formatted output\n" diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index e46977d2fac..8fed8a68786 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -22,6 +22,8 @@ Author: Peter Schrammel #include #include +#include + class goto_modelt; class optionst; @@ -31,7 +33,7 @@ class optionst; OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ - "(cover):" \ + OPT_COVER \ "(verbosity):(version)" \ OPT_FLUSH \ OPT_TIMESTAMP \ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 5dac8217361..3103f3e3269 100644 --- a/src/goto-instrument/cover.cpp +++ b/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; } } } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index fd5dfde7267..585dede7674 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -22,6 +22,18 @@ class message_handlert; class cmdlinet; class optionst; +#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 { LOCATION, @@ -37,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;