diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 65da4bee9a9..33d5ce64a0f 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/jbmc/regression/CMakeLists.txt @@ -10,5 +10,4 @@ add_subdirectory(jdiff) add_subdirectory(janalyzer-taint) add_subdirectory(jbmc-concurrency) add_subdirectory(jbmc-inheritance) -add_subdirectory(jbmc-cover) add_subdirectory(jbmc-generics) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 17b0e94bb01..42a479942e2 100644 --- a/jbmc/regression/Makefile +++ b/jbmc/regression/Makefile @@ -4,7 +4,6 @@ DIRS = janalyzer-taint \ jbmc \ jbmc-concurrency \ - jbmc-cover \ jbmc-inheritance \ jbmc-strings \ jdiff \ diff --git a/jbmc/regression/jbmc-cover/CMakeLists.txt b/jbmc/regression/jbmc-cover/CMakeLists.txt deleted file mode 100644 index afe0ea5761a..00000000000 --- a/jbmc/regression/jbmc-cover/CMakeLists.txt +++ /dev/null @@ -1,3 +0,0 @@ -add_test_pl_tests( - "$" -) diff --git a/jbmc/regression/jbmc-cover/Makefile b/jbmc/regression/jbmc-cover/Makefile deleted file mode 100644 index ad6e5381fff..00000000000 --- a/jbmc/regression/jbmc-cover/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-cover/covered1/covered1.class b/jbmc/regression/jbmc-cover/covered1/covered1.class deleted file mode 100644 index 7cb91496b7d..00000000000 Binary files a/jbmc/regression/jbmc-cover/covered1/covered1.class and /dev/null differ diff --git a/jbmc/regression/jbmc-cover/covered1/covered1.java b/jbmc/regression/jbmc-cover/covered1/covered1.java deleted file mode 100644 index 018e65336a6..00000000000 --- a/jbmc/regression/jbmc-cover/covered1/covered1.java +++ /dev/null @@ -1,37 +0,0 @@ -public class covered1 -{ - // this is a variable - int x=1; - //these are two, one line off the first - int y=2; - int z=3; - //this is part of static init - static int z0=0; - - //another non-static - int a; - int b; - static boolean odd; - - static - { - odd=(z0+1)%2==0; - } - - covered1(int a, int b) - { - this.a=a*b; - this.b=a+b; - if(this.a==a) - z0++; - else - odd=!odd; - } - // at the back - int z1=2; - int z2=3; - int z3=4; - // - static int z4=5; - int z5=5; -} diff --git a/jbmc/regression/jbmc-cover/covered1/test.desc b/jbmc/regression/jbmc-cover/covered1/test.desc deleted file mode 100644 index 8f6adc9d0a3..00000000000 --- a/jbmc/regression/jbmc-cover/covered1/test.desc +++ /dev/null @@ -1,33 +0,0 @@ -CORE -covered1.class ---cover location --json-ui --show-properties --function 'covered1.' -^EXIT=0$ -^SIGNAL=0$ -.*\"coveredLines\": \"22\",$ -(.*\"coveredLines\": \"4\")|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"6\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"7\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"23\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"24\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"25\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"31\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"32\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"33\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"36\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"26\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"29\",$ -.*\"coveredLines\": \"18\",$ -.*\"coveredLines\": \"18\",$ -.*\"coveredLines\": \"35\",$ --- -^warning: ignoring --- -The alternation between the grouped and ungrouped reporting formats for coveredLines accommodates the -difference between symex-driven-lazy-loading (which currently causes jbmc to use the grouped format) -and normal loading (which uses the ungrouped format). -The cause of the difference appears to be symex-driven loading being more pessimistic about possible -exceptions coming from callees, which in turn changes the shape of the CFG. diff --git a/jbmc/regression/jbmc-cover/json_trace2/Test.class b/jbmc/regression/jbmc-cover/json_trace2/Test.class deleted file mode 100644 index 68771db843a..00000000000 Binary files a/jbmc/regression/jbmc-cover/json_trace2/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc-cover/json_trace2/Test.java b/jbmc/regression/jbmc-cover/json_trace2/Test.java deleted file mode 100644 index 25608c219d3..00000000000 --- a/jbmc/regression/jbmc-cover/json_trace2/Test.java +++ /dev/null @@ -1,7 +0,0 @@ -public class Test { - boolean test(Object x) { - if(x==null) - return false; - return true; - } -} diff --git a/jbmc/regression/jbmc-cover/json_trace2/test.desc b/jbmc/regression/jbmc-cover/json_trace2/test.desc deleted file mode 100644 index 390b8c6d3d3..00000000000 --- a/jbmc/regression/jbmc-cover/json_trace2/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE -Test.class ---cover location --trace --json-ui --function Test.test -activate-multi-line-match -EXIT=0 -SIGNAL=0 -"outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8 -"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; \} \*" --- -^warning: ignoring diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index a4474d1edd5..7d134f4dfff 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -121,9 +121,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("show-vcc")) options.set_option("show-vcc", true); - if(cmdline.isset("cover")) - parse_cover_options(cmdline, options); - if(cmdline.isset("nondet-static")) options.set_option("nondet-static", true); @@ -189,14 +186,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("assumptions", false); // generate unwinding assertions - if(cmdline.isset("cover")) - options.set_option("unwinding-assertions", false); - else - { - options.set_option( - "unwinding-assertions", - cmdline.isset("unwinding-assertions")); - } + if(cmdline.isset("unwinding-assertions")) + options.set_option("unwinding-assertions", true); // generate unwinding assumptions otherwise options.set_option( @@ -559,12 +550,6 @@ int jbmc_parse_optionst::doit() // particular function: add_failed_symbols(lazy_goto_model.symbol_table); - // If applicable, parse the coverage instrumentation configuration, which - // will be used in process_goto_function: - cover_config = - get_cover_config( - options, lazy_goto_model.symbol_table, get_message_handler()); - // Provide show-goto-functions and similar dump functions after symex // executes. If --paths is active, these dump routines run after every // paths iteration. Its return value indicates that if we ran any dump @@ -782,20 +767,12 @@ void jbmc_parse_optionst::process_goto_function( symbol_table); } - // If using symex-driven function loading we must insert the coverage goals + // If using symex-driven function loading we must label the assertions // now so symex sees its targets; otherwise we leave this until // process_goto_functions, as we haven't run remove_exceptions yet, and that // pass alters the CFG. if(using_symex_driven_loading) { - // instrument cover goals - if(cmdline.isset("cover")) - { - INVARIANT( - cover_config != nullptr, "cover config should have been parsed"); - instrument_cover_goals(*cover_config, function, get_message_handler()); - } - // label the assertions label_properties(goto_function.body); @@ -916,17 +893,9 @@ bool jbmc_parse_optionst::process_goto_functions( remove_unused_functions(goto_model, get_message_handler()); } - // remove skips such that trivial GOTOs are deleted and not considered - // for coverage annotation: + // remove skips such that trivial GOTOs are deleted remove_skip(goto_model); - // instrument cover goals - if(cmdline.isset("cover")) - { - if(instrument_cover_goals(options, goto_model, get_message_handler())) - return true; - } - // label the assertions // This must be done after adding assertions and // before using the argument of the "property" option. @@ -970,7 +939,7 @@ bool jbmc_parse_optionst::process_goto_functions( full_slicer(goto_model); } - // remove any skips introduced since coverage instrumentation + // remove any skips introduced remove_skip(goto_model); } @@ -1079,7 +1048,6 @@ void jbmc_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(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) HELP_REACHABILITY_SLICER " --full-slice run full slicer (experimental)\n" // NOLINT(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index d0c5ad3d094..69d7f5a0a8b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -69,7 +68,7 @@ class optionst; "(verbosity):" \ "(nondet-static)" \ "(version)" \ - "(cover):(symex-coverage-report):" \ + "(symex-coverage-report):" \ OPT_TIMESTAMP \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \ "(ppc-macos)" \ @@ -120,7 +119,6 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; - std::unique_ptr cover_config; path_strategy_choosert path_strategy_chooser; object_factory_parameterst object_factory_params; bool stub_objects_are_not_null;