From cefd3ce45dd7da46647494fc3b6f3b39ddbe1123 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 27 Nov 2020 16:53:28 +0000 Subject: [PATCH 1/9] Extract constants for --cover help message and options These were previously duplicated between 3 different executables. --- jbmc/src/jdiff/jdiff_parse_options.cpp | 2 +- jbmc/src/jdiff/jdiff_parse_options.h | 4 +++- src/cbmc/cbmc_parse_options.cpp | 2 +- src/cbmc/cbmc_parse_options.h | 7 +++++-- src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-diff/goto_diff_parse_options.h | 4 +++- src/goto-instrument/cover.h | 4 ++++ 7 files changed, 18 insertions(+), 7 deletions(-) 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/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..b9769fd5db6 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; @@ -73,8 +75,9 @@ class optionst; "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ - "(version)" \ - "(cover):(symex-coverage-report):" \ + "(version)" \ + 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.h b/src/goto-instrument/cover.h index fd5dfde7267..5a43de40d0f 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -22,6 +22,10 @@ class message_handlert; class cmdlinet; class optionst; +#define OPT_COVER "(cover):" +#define HELP_COVER \ + " --cover CC create test-suite with coverage criterion CC\n" + enum class coverage_criteriont { LOCATION, From a442dbb4b6ac1825b6c751e38b0d8fa804db3fea Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 27 Nov 2020 18:41:34 +0000 Subject: [PATCH 2/9] 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). --- .../test-no-failed-assertions.desc | 11 ++++++++ .../cbmc/cover-failed-assertions/test.c | 14 ++++++++++ .../cbmc/cover-failed-assertions/test.desc | 11 ++++++++ src/goto-instrument/cover.cpp | 27 +++++++++++++------ src/goto-instrument/cover.h | 15 ++++++++--- 5 files changed, 67 insertions(+), 11 deletions(-) create mode 100644 regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc create mode 100644 regression/cbmc/cover-failed-assertions/test.c create mode 100644 regression/cbmc/cover-failed-assertions/test.desc 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..930cf9ac491 --- /dev/null +++ b/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 diff --git a/regression/cbmc/cover-failed-assertions/test.c b/regression/cbmc/cover-failed-assertions/test.c new file mode 100644 index 00000000000..3f5cf35854d --- /dev/null +++ b/regression/cbmc/cover-failed-assertions/test.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int *ptr = malloc(sizeof(*ptr)); + int a; + + 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..6d187373bcf --- /dev/null +++ b/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 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 5a43de40d0f..585dede7674 100644 --- a/src/goto-instrument/cover.h +++ b/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; From d3bfa2b514633c8748f48140085d948695f3f7a4 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 27 Nov 2020 19:09:23 +0000 Subject: [PATCH 3/9] Update cbmc README.md with --cover-failed-assertions flag --- src/cbmc/README.md | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) 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"). From b3d0bfade05441d4b1cc093bc1c98d1c4d355b90 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 3 Dec 2020 14:29:42 +0000 Subject: [PATCH 4/9] Update regexes in test to match actual lines matched. --- .../test-no-failed-assertions.desc | 8 ++++---- regression/cbmc/cover-failed-assertions/test.desc | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 930cf9ac491..bf8a5518528 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,10 +1,10 @@ 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 +\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:13,14\): SATISFIED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): FAILED +\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED +\[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc index 6d187373bcf..c82014eeb26 100644 --- a/regression/cbmc/cover-failed-assertions/test.desc +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -1,10 +1,10 @@ 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 +\[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:13,14\): SATISFIED +\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): SATISFIED +\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED +\[main.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ -- From c039da3c3ebc23a9fb4bc46042ca176357972bb4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 7 Dec 2020 15:20:10 +0000 Subject: [PATCH 5/9] Mark new tests as expected failures for paths flag. The tests are failing when the `--paths` flag is set. This is because we understand that the paths code hasn't been exercised thoroughly, and as a result this behaviour may or may not indicate a potential issue - we need to investigate this at a later point. --- .../cbmc/cover-failed-assertions/test-no-failed-assertions.desc | 2 +- regression/cbmc/cover-failed-assertions/test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index bf8a5518528..63f485e2d47 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,4 +1,4 @@ -CORE +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:13,14\): SATISFIED diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc index c82014eeb26..252bc082c84 100644 --- a/regression/cbmc/cover-failed-assertions/test.desc +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -1,4 +1,4 @@ -CORE +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:13,14\): SATISFIED From a86ffc7dba57d61c6a1922fce92490130f73974e Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 10 Dec 2020 11:37:51 +0000 Subject: [PATCH 6/9] Do not check XML traces on --cover tests --- regression/validate-trace-xml-schema/check.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 374502139f9..9d0f57e232b 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 including 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'], From e93654c2326250500868da94c1b137926d0f06c7 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 17 Dec 2020 14:26:07 +0000 Subject: [PATCH 7/9] Fix typo --- regression/validate-trace-xml-schema/check.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 9d0f57e232b..d4ee217ae04 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -34,7 +34,7 @@ ['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 including in the schema + # 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 From 3d21a85ca8f2427bdf2cc89940b951ff9d3a84f1 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 17 Dec 2020 14:26:43 +0000 Subject: [PATCH 8/9] Fix spacing --- src/cbmc/cbmc_parse_options.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index b9769fd5db6..af9e265f782 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -75,7 +75,7 @@ class optionst; "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ - "(version)" \ + "(version)" \ OPT_COVER \ "(symex-coverage-report):" \ "(mm):" \ From bad0d162647f25128b848ee6d820cd95e4925985 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 17 Dec 2020 15:49:26 +0000 Subject: [PATCH 9/9] Add comments to tests --- .../test-no-failed-assertions.desc | 9 ++++++--- regression/cbmc/cover-failed-assertions/test.c | 4 ++++ regression/cbmc/cover-failed-assertions/test.desc | 8 +++++--- 3 files changed, 15 insertions(+), 6 deletions(-) diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 63f485e2d47..0544dcdb715 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,11 +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:13,14\): SATISFIED -\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): FAILED -\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED +\[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 index 3f5cf35854d..61c894cf382 100644 --- a/regression/cbmc/cover-failed-assertions/test.c +++ b/regression/cbmc/cover-failed-assertions/test.c @@ -5,6 +5,10 @@ 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) diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc index 252bc082c84..2b07b32fe2d 100644 --- a/regression/cbmc/cover-failed-assertions/test.desc +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -1,11 +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:13,14\): SATISFIED -\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:11\): SATISFIED -\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,8,10\): SATISFIED +\[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