From 525b85dff016eea32bc620a07f58b9afa4efdf8f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 3 Mar 2018 15:00:43 +0000 Subject: [PATCH 1/3] split out ccover from cbmc --- .gitignore | 2 + CMakeLists.txt | 2 + regression/ccover/Makefile | 19 + .../pointer-function-parameters-2/main.c | 0 .../pointer-function-parameters-2/test.desc | 0 .../pointer-function-parameters/main.c | 0 .../pointer-function-parameters/test.desc | 0 .../reachability-slice/test.c | 0 .../reachability-slice/test.desc | 0 .../reachability-slice/test2.desc | 0 .../reachability-slice/test3.desc | 0 .../{cbmc => ccover}/simple_assert/main.c | 0 .../{cbmc => ccover}/simple_assert/test.desc | 0 src/CMakeLists.txt | 1 + src/Makefile | 4 + src/ccover/CMakeLists.txt | 35 + src/ccover/Makefile | 76 ++ src/{cbmc => ccover}/bmc_cover.cpp | 10 +- src/ccover/ccover_bmc.cpp | 199 +++++ src/ccover/ccover_bmc.h | 100 +++ src/ccover/ccover_main.cpp | 39 + src/ccover/ccover_parse_options.cpp | 752 ++++++++++++++++++ src/ccover/ccover_parse_options.h | 91 +++ 23 files changed, 1325 insertions(+), 5 deletions(-) create mode 100644 regression/ccover/Makefile rename regression/{cbmc => ccover}/pointer-function-parameters-2/main.c (100%) rename regression/{cbmc => ccover}/pointer-function-parameters-2/test.desc (100%) rename regression/{cbmc => ccover}/pointer-function-parameters/main.c (100%) rename regression/{cbmc => ccover}/pointer-function-parameters/test.desc (100%) rename regression/{cbmc => ccover}/reachability-slice/test.c (100%) rename regression/{cbmc => ccover}/reachability-slice/test.desc (100%) rename regression/{cbmc => ccover}/reachability-slice/test2.desc (100%) rename regression/{cbmc => ccover}/reachability-slice/test3.desc (100%) rename regression/{cbmc => ccover}/simple_assert/main.c (100%) rename regression/{cbmc => ccover}/simple_assert/test.desc (100%) create mode 100644 src/ccover/CMakeLists.txt create mode 100644 src/ccover/Makefile rename src/{cbmc => ccover}/bmc_cover.cpp (98%) create mode 100644 src/ccover/ccover_bmc.cpp create mode 100644 src/ccover/ccover_bmc.h create mode 100644 src/ccover/ccover_main.cpp create mode 100644 src/ccover/ccover_parse_options.cpp create mode 100644 src/ccover/ccover_parse_options.h diff --git a/.gitignore b/.gitignore index c10ff2decde..7cbe1dcb4dd 100644 --- a/.gitignore +++ b/.gitignore @@ -96,6 +96,8 @@ src/memory-models/mm_y.tab.h # binaries src/cbmc/cbmc src/cbmc/cbmc.exe +src/ccover/ccover +src/ccover/ccover.exe src/goto-analyzer/goto-analyzer src/goto-analyzer/goto-analyzer.exe src/goto-cc/goto-cc diff --git a/CMakeLists.txt b/CMakeLists.txt index fea650dbac1..8e844c398ce 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -52,6 +52,8 @@ set_target_properties( big-int cbmc cbmc-lib + ccover + ccover-lib cpp driver goto-analyzer diff --git a/regression/ccover/Makefile b/regression/ccover/Makefile new file mode 100644 index 00000000000..6ecfb9d1c97 --- /dev/null +++ b/regression/ccover/Makefile @@ -0,0 +1,19 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/ccover/ccover -X smt-backend + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/ccover/ccover -X smt-backend + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/cbmc/pointer-function-parameters-2/main.c b/regression/ccover/pointer-function-parameters-2/main.c similarity index 100% rename from regression/cbmc/pointer-function-parameters-2/main.c rename to regression/ccover/pointer-function-parameters-2/main.c diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/ccover/pointer-function-parameters-2/test.desc similarity index 100% rename from regression/cbmc/pointer-function-parameters-2/test.desc rename to regression/ccover/pointer-function-parameters-2/test.desc diff --git a/regression/cbmc/pointer-function-parameters/main.c b/regression/ccover/pointer-function-parameters/main.c similarity index 100% rename from regression/cbmc/pointer-function-parameters/main.c rename to regression/ccover/pointer-function-parameters/main.c diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/ccover/pointer-function-parameters/test.desc similarity index 100% rename from regression/cbmc/pointer-function-parameters/test.desc rename to regression/ccover/pointer-function-parameters/test.desc diff --git a/regression/cbmc/reachability-slice/test.c b/regression/ccover/reachability-slice/test.c similarity index 100% rename from regression/cbmc/reachability-slice/test.c rename to regression/ccover/reachability-slice/test.c diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/ccover/reachability-slice/test.desc similarity index 100% rename from regression/cbmc/reachability-slice/test.desc rename to regression/ccover/reachability-slice/test.desc diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/ccover/reachability-slice/test2.desc similarity index 100% rename from regression/cbmc/reachability-slice/test2.desc rename to regression/ccover/reachability-slice/test2.desc diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/ccover/reachability-slice/test3.desc similarity index 100% rename from regression/cbmc/reachability-slice/test3.desc rename to regression/ccover/reachability-slice/test3.desc diff --git a/regression/cbmc/simple_assert/main.c b/regression/ccover/simple_assert/main.c similarity index 100% rename from regression/cbmc/simple_assert/main.c rename to regression/ccover/simple_assert/main.c diff --git a/regression/cbmc/simple_assert/test.desc b/regression/ccover/simple_assert/test.desc similarity index 100% rename from regression/cbmc/simple_assert/test.desc rename to regression/ccover/simple_assert/test.desc diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4022889e456..6111649f6de 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -97,6 +97,7 @@ add_subdirectory(util) add_subdirectory(xmllang) add_subdirectory(cbmc) +add_subdirectory(ccover) add_subdirectory(goto-cc) add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) diff --git a/src/Makefile b/src/Makefile index a75535d49bc..beffa777260 100644 --- a/src/Makefile +++ b/src/Makefile @@ -3,6 +3,7 @@ DIRS = analyses \ assembler \ big-int \ cbmc \ + ccover \ cpp \ goto-analyzer \ goto-cc \ @@ -21,6 +22,7 @@ DIRS = analyses \ # Empty last line all: cbmc.dir \ + ccover.dir \ goto-analyzer.dir \ goto-cc.dir \ goto-diff.dir \ @@ -53,6 +55,8 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \ pointer-analysis.dir goto-programs.dir linking.dir \ goto-instrument.dir +ccover.dir: cbmc.dir + goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \ json.dir goto-instrument.dir diff --git a/src/ccover/CMakeLists.txt b/src/ccover/CMakeLists.txt new file mode 100644 index 00000000000..b77ceee6ae9 --- /dev/null +++ b/src/ccover/CMakeLists.txt @@ -0,0 +1,35 @@ +# Library +file(GLOB_RECURSE sources "*.cpp" "*.h") +list(REMOVE_ITEM sources + ${CMAKE_CURRENT_SOURCE_DIR}/ccover_main.cpp +) +add_library(ccover-lib ${sources}) + +generic_includes(ccover-lib) + +target_link_libraries(ccover-lib + analyses + ansi-c + assembler + big-int + cbmc-lib + cpp + goto-instrument-lib + goto-programs + goto-symex + java_bytecode + json + langapi + linking + pointer-analysis + solvers + util + xml +) + +add_if_library(ccover-lib bv_refinement) +add_if_library(ccover-lib jsil) + +# Executable +add_executable(ccover ccover_main.cpp) +target_link_libraries(ccover ccover-lib) diff --git a/src/ccover/Makefile b/src/ccover/Makefile new file mode 100644 index 00000000000..2c70274ca19 --- /dev/null +++ b/src/ccover/Makefile @@ -0,0 +1,76 @@ +SRC = ccover_bmc.cpp \ + bmc_cover.cpp \ + ccover_main.cpp \ + ccover_parse_options.cpp \ + # Empty last line + +OBJ += ../ansi-c/ansi-c$(LIBEXT) \ + ../cpp/cpp$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ + ../big-int/big-int$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../goto-symex/goto-symex$(LIBEXT) \ + ../pointer-analysis/value_set$(OBJEXT) \ + ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \ + ../pointer-analysis/value_set_domain_fi$(OBJEXT) \ + ../pointer-analysis/value_set_fi$(OBJEXT) \ + ../pointer-analysis/value_set_dereference$(OBJEXT) \ + ../pointer-analysis/dereference_callback$(OBJEXT) \ + ../pointer-analysis/add_failed_symbols$(OBJEXT) \ + ../pointer-analysis/rewrite_index$(OBJEXT) \ + ../pointer-analysis/goto_program_dereference$(OBJEXT) \ + ../goto-instrument/full_slicer$(OBJEXT) \ + ../goto-instrument/nondet_static$(OBJEXT) \ + ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_basic_blocks$(OBJEXT) \ + ../goto-instrument/cover_filter$(OBJEXT) \ + ../goto-instrument/cover_instrument_branch$(OBJEXT) \ + ../goto-instrument/cover_instrument_condition$(OBJEXT) \ + ../goto-instrument/cover_instrument_decision$(OBJEXT) \ + ../goto-instrument/cover_instrument_location$(OBJEXT) \ + ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-instrument/cover_instrument_other$(OBJEXT) \ + ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-instrument/unwindset$(OBJEXT) \ + ../analyses/analyses$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../xmllang/xmllang$(LIBEXT) \ + ../assembler/assembler$(LIBEXT) \ + ../solvers/solvers$(LIBEXT) \ + ../util/util$(LIBEXT) \ + ../json/json$(LIBEXT) \ + ../cbmc/bv_cbmc$(OBJEXT) \ + ../cbmc/cbmc_dimacs$(OBJEXT) \ + ../cbmc/cbmc_solvers$(OBJEXT) \ + ../cbmc/symex_bmc$(OBJEXT) + +INCLUDES= -I .. + +LIBS = + +include ../config.inc +include ../common + +CLEANFILES = ccover$(EXEEXT) + +all: ccover$(EXEEXT) + +ifneq ($(wildcard ../bv_refinement/Makefile),) + OBJ += ../bv_refinement/bv_refinement$(LIBEXT) + CP_CXXFLAGS += -DHAVE_BV_REFINEMENT +endif + +ifneq ($(wildcard ../jsil/Makefile),) + OBJ += ../jsil/jsil$(LIBEXT) + CP_CXXFLAGS += -DHAVE_JSIL +endif + +############################################################################### + +ccover$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: ccover-mac-signed + +ccover-mac-signed: ccover$(EXEEXT) + strip ccover$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) ccover$(EXEEXT) diff --git a/src/cbmc/bmc_cover.cpp b/src/ccover/bmc_cover.cpp similarity index 98% rename from src/cbmc/bmc_cover.cpp rename to src/ccover/bmc_cover.cpp index 12d9ef66bb6..e599ee0b684 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/ccover/bmc_cover.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Test-Suite Generation with BMC -#include "bmc.h" +#include "ccover_bmc.h" #include #include @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "bv_cbmc.h" +#include class bmc_covert: public cover_goalst::observert, @@ -38,7 +38,7 @@ class bmc_covert: public: bmc_covert( const goto_functionst &_goto_functions, - bmct &_bmc): + ccover_bmct &_bmc): goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc) { } @@ -141,7 +141,7 @@ class bmc_covert: protected: const goto_functionst &goto_functions; prop_convt &solver; - bmct &bmc; + ccover_bmct &bmc; }; static bool is_failed_assumption_step( @@ -420,7 +420,7 @@ bool bmc_covert::operator()() } /// Try to cover all goals -bool bmct::cover(const goto_functionst &goto_functions) +bool ccover_bmct::cover(const goto_functionst &goto_functions) { bmc_covert bmc_cover(goto_functions, *this); bmc_cover.set_message_handler(get_message_handler()); diff --git a/src/ccover/ccover_bmc.cpp b/src/ccover/ccover_bmc.cpp new file mode 100644 index 00000000000..6d9c0fc0b4d --- /dev/null +++ b/src/ccover/ccover_bmc.cpp @@ -0,0 +1,199 @@ +/*******************************************************************\ + +Module: Bounded Model Checking for Test Suite Generation + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking for Test Suite Generation + +#include "ccover_bmc.h" + +#include +#include +#include + +#include + +#include +#include +#include +#include + +#include + +#include + +void ccover_bmct::do_conversion() +{ + status() << "converting SSA" << eom; + + // convert SSA + equation.convert(prop_conv); +} + +void ccover_bmct::get_memory_model() +{ + const std::string mm=options.get_option("mm"); + + if(mm.empty() || mm=="sc") + memory_model=util_make_unique(ns); + else if(mm=="tso") + memory_model=util_make_unique(ns); + else if(mm=="pso") + memory_model=util_make_unique(ns); + else + { + error() << "Invalid memory model " << mm + << " -- use one of sc, tso, pso" << eom; + throw "invalid memory model"; + } +} + +void ccover_bmct::setup() +{ + get_memory_model(); + + { + const symbolt *init_symbol; + if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) + symex.language_mode=init_symbol->mode; + } + + status() << "Starting Bounded Model Checking" << eom; + + symex.last_source_location.make_nil(); + + symex.unwindset.parse_unwind(options.get_option("unwind")); + symex.unwindset.parse_unwindset(options.get_option("unwindset")); +} + +void ccover_bmct::run(abstract_goto_modelt &goto_model) +{ + setup(); + + auto get_goto_function = [&goto_model](const irep_idt &id) -> + const goto_functionst::goto_functiont & + { + return goto_model.get_goto_function(id); + }; + + // perform symbolic execution + symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); + + // Borrow a reference to the goto functions map. This reference, or + // iterators pointing into it, must not be stored by this function or its + // callees, as goto_model.get_goto_function (as used by symex) + // will have side-effects on it. + const goto_functionst &goto_functions = + goto_model.get_goto_functions(); + + // add a partial ordering, if required + if(equation.has_threads()) + { + memory_model->set_message_handler(get_message_handler()); + (*memory_model)(equation); + } + + statistics() << "size of program expression: " + << equation.SSA_steps.size() + << " steps" << eom; + + slice(); + +// const optionst::value_listt criteria= +// options.get_list_option("cover"); + + cover(goto_functions); +} + +void ccover_bmct::slice() +{ + // any properties to check at all? + if(equation.has_threads()) + { + // we should build a thread-aware SSA slicer + statistics() << "no slicing due to threads" << eom; + } + else + { + if(options.get_bool_option("slice-formula")) + { + ::slice(equation); + statistics() << "slicing removed " + << equation.count_ignored_SSA_steps() + << " assignments" << eom; + } + else + { + if(options.get_list_option("cover").empty()) + { + simple_slice(equation); + statistics() << "simple slicing removed " + << equation.count_ignored_SSA_steps() + << " assignments" << eom; + } + } + } + + statistics() << "Generated " + << symex.total_vccs<<" VCC(s), " + << symex.remaining_vccs + << " remaining after simplification" << eom; +} + +/// Perform core BMC, using an abstract model to supply GOTO function bodies +/// (perhaps created on demand). +/// \param opts: command-line options affecting BMC +/// \param model: provides goto function bodies and the symbol table, perhaps +// creating those function bodies on demand. +/// \param ui: user-interface mode (plain text, XML output, JSON output, ...) +/// \param message_handler: used for logging +int ccover_bmct::do_bmc( + const optionst &opts, + abstract_goto_modelt &model, + const ui_message_handlert::uit &ui, + message_handlert &message_handler) +{ + const symbol_tablet &symbol_table = model.get_symbol_table(); + messaget message(message_handler); + + path_strategy_choosert path_strategy_chooser; + std::unique_ptr path_storage= + path_strategy_chooser.get("lifo"); + + try + { + cbmc_solverst solvers(opts, symbol_table, message_handler); + solvers.set_ui(ui); + std::unique_ptr cbmc_solver; + cbmc_solver = solvers.get_solver(); + prop_convt &pc = cbmc_solver->prop_conv(); + ccover_bmct bmc(opts, symbol_table, message_handler, pc, *path_storage); + bmc.set_ui(ui); + bmc.run(model); + return CPROVER_EXIT_SUCCESS; + } + catch(const char *error_msg) + { + message.error() << error_msg << message.eom; + return CPROVER_EXIT_EXCEPTION; + } + catch(const std::string &error_msg) + { + message.error() << error_msg << message.eom; + return CPROVER_EXIT_EXCEPTION; + } + catch(const std::bad_alloc &) + { + message.error() << "Out of memory" << eom; + return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; + } + catch(...) + { + message.error() << "unable to get solver" << message.eom; + return CPROVER_EXIT_EXCEPTION; + } +} diff --git a/src/ccover/ccover_bmc.h b/src/ccover/ccover_bmc.h new file mode 100644 index 00000000000..194115908ec --- /dev/null +++ b/src/ccover/ccover_bmc.h @@ -0,0 +1,100 @@ +/*******************************************************************\ + +Module: Bounded Model Checking for Test Suite Generation + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking for Test Suite Generation + +#ifndef CPROVER_CCOVER_CCOVER_BMC_H +#define CPROVER_CCOVER_CCOVER_BMC_H + +#include + +#include + +#include + +#include +#include +#include + +#include + +class optionst; + +class ccover_bmct:public messaget +{ +public: + ccover_bmct( + const optionst &_options, + const symbol_tablet &outer_symbol_table, + message_handlert &_message_handler, + prop_convt &_prop_conv, + path_storaget &_path_storage) + : messaget(_message_handler), + options(_options), + outer_symbol_table(outer_symbol_table), + ns(outer_symbol_table, symex_symbol_table), + equation(), + path_storage(_path_storage), + symex(_message_handler, outer_symbol_table, equation, _options, path_storage), + prop_conv(_prop_conv), + ui(ui_message_handlert::uit::PLAIN) + { + symex.constant_propagation=options.get_bool_option("propagation"); + symex.record_coverage= + !options.get_option("symex-coverage-report").empty(); + } + + void run(abstract_goto_modelt &); + + virtual ~ccover_bmct() { } + + void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } + + static int do_bmc( + const optionst &opts, + abstract_goto_modelt &goto_model, + const ui_message_handlert::uit &ui, + message_handlert &); + +protected: + const optionst &options; + /// \brief symbol table for the goto-program that we will execute + + const symbol_tablet &outer_symbol_table; + /// \brief symbol table generated during symbolic execution + + symbol_tablet symex_symbol_table; + namespacet ns; + symex_target_equationt equation; + path_storaget &path_storage; + symex_bmct symex; + prop_convt &prop_conv; + std::unique_ptr memory_model; + // use gui format + ui_message_handlert::uit ui; + + // unwinding + void setup_unwind(); + void do_conversion(); + + trace_optionst trace_options() + { + return trace_optionst(options); + } + + void setup(); + void get_memory_model(); + void slice(); + + bool cover(const goto_functionst &); + + friend class bmc_covert; +}; + +#endif // CPROVER_CCOVER_CCOVER_BMC_H diff --git a/src/ccover/ccover_main.cpp b/src/ccover/ccover_main.cpp new file mode 100644 index 00000000000..0190c23dd05 --- /dev/null +++ b/src/ccover/ccover_main.cpp @@ -0,0 +1,39 @@ +/*******************************************************************\ + +Module: ccover Main Module + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// ccover Main Module + +/* + + ccover + Test suite generation for ANSI-C + Copyright (C) 2018 Daniel Kroening + +*/ + +#include "ccover_parse_options.h" + +#include + +#ifdef _MSC_VER +int wmain(int argc, const wchar_t **argv_wide) +{ + auto vec=narrow_argv(argc, argv_wide); + auto narrow=to_c_str_array(std::begin(vec), std::end(vec)); + auto argv=narrow.data(); +#else +int main(int argc, const char **argv) +{ +#endif + ccover_parse_optionst parse_options(argc, argv); + + int res=parse_options.main(); + + return res; +} diff --git a/src/ccover/ccover_parse_options.cpp b/src/ccover/ccover_parse_options.cpp new file mode 100644 index 00000000000..6a2722f30ce --- /dev/null +++ b/src/ccover/ccover_parse_options.cpp @@ -0,0 +1,752 @@ +/*******************************************************************\ + +Module: CBMC Command Line Option Processing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// CBMC Command Line Option Processing + +#include "ccover_parse_options.h" + +#include +#include // exit() +#include +#include + +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include + +#include +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include +#include +#include + +#include + +#include + +ccover_parse_optionst::ccover_parse_optionst(int argc, const char **argv): + parse_options_baset(CCOVER_OPTIONS, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("ccover ") + CBMC_VERSION) +{ +} + +void ccover_parse_optionst::eval_verbosity() +{ + // this is our default verbosity + unsigned int v=messaget::M_STATISTICS; + + if(cmdline.isset("verbosity")) + { + v=unsafe_string2unsigned(cmdline.get_value("verbosity")); + if(v>10) + v=10; + } + + ui_message_handler.set_verbosity(v); +} + +void ccover_parse_optionst::get_command_line_options(optionst &options) +{ + if(config.set(cmdline)) + { + usage_error(); + exit(CPROVER_EXIT_USAGE_ERROR); + } + + if(cmdline.isset("paths")) + options.set_option("paths", true); + + if(cmdline.isset("show-vcc")) + options.set_option("show-vcc", true); + + if(cmdline.isset("cover")) + parse_cover_options(cmdline, options); + else // default criterion + options.set_option("cover", std::list({"location"})); + + if(cmdline.isset("mm")) + options.set_option("mm", cmdline.get_value("mm")); + + if(cmdline.isset("c89")) + config.ansi_c.set_c89(); + + if(cmdline.isset("c99")) + config.ansi_c.set_c99(); + + if(cmdline.isset("c11")) + config.ansi_c.set_c11(); + + if(cmdline.isset("cpp98")) + config.cpp.set_cpp98(); + + if(cmdline.isset("cpp03")) + config.cpp.set_cpp03(); + + if(cmdline.isset("cpp11")) + config.cpp.set_cpp11(); + + if(cmdline.isset("no-simplify")) + options.set_option("simplify", false); + else + options.set_option("simplify", true); + + if(cmdline.isset("trace")) + options.set_option("trace", true); + + if(cmdline.isset("unwind")) + options.set_option("unwind", cmdline.get_value("unwind")); + + if(cmdline.isset("depth")) + options.set_option("depth", cmdline.get_value("depth")); + + if(cmdline.isset("debug-level")) + options.set_option("debug-level", cmdline.get_value("debug-level")); + + if(cmdline.isset("unwindset")) + options.set_option("unwindset", cmdline.get_value("unwindset")); + + // constant propagation + if(cmdline.isset("no-propagation")) + options.set_option("propagation", false); + else + options.set_option("propagation", true); + + // use assumptions + if(cmdline.isset("no-assumptions")) + options.set_option("assumptions", false); + else + options.set_option("assumptions", true); + + // remove unused equations + options.set_option( + "slice-formula", + cmdline.isset("slice-formula")); + + // simplify if conditions and branches + if(cmdline.isset("no-simplify-if")) + options.set_option("simplify-if", false); + else + options.set_option("simplify-if", true); + + if(cmdline.isset("arrays-uf-always")) + options.set_option("arrays-uf", "always"); + else if(cmdline.isset("arrays-uf-never")) + options.set_option("arrays-uf", "never"); + else + options.set_option("arrays-uf", "auto"); + + if(cmdline.isset("refine-arrays")) + { + options.set_option("refine", true); + options.set_option("refine-arrays", true); + } + + if(cmdline.isset("refine-arithmetic")) + { + options.set_option("refine", true); + options.set_option("refine-arithmetic", true); + } + + if(cmdline.isset("refine")) + { + options.set_option("refine", true); + options.set_option("refine-arrays", true); + options.set_option("refine-arithmetic", true); + } + + if(cmdline.isset("refine-strings")) + { + options.set_option("refine-strings", true); + options.set_option("string-printable", cmdline.isset("string-printable")); + if(cmdline.isset("string-max-length")) + options.set_option( + "string-max-length", cmdline.get_value("string-max-length")); + } + + if(cmdline.isset("max-node-refinement")) + options.set_option( + "max-node-refinement", + cmdline.get_value("max-node-refinement")); + + if(cmdline.isset("aig")) + options.set_option("aig", true); + + if(cmdline.isset("fpa")) + options.set_option("fpa", true); + + if(cmdline.isset("boolector")) + { + options.set_option("boolector", true); + options.set_option("smt2", true); + } + + if(cmdline.isset("mathsat")) + { + options.set_option("mathsat", true); + options.set_option("smt2", true); + } + + if(cmdline.isset("cvc4")) + { + options.set_option("cvc4", true); + options.set_option("smt2", true); + } + + if(cmdline.isset("yices")) + { + options.set_option("yices", true); + options.set_option("smt2", true); + } + + if(cmdline.isset("z3")) + { + options.set_option("z3", true); + options.set_option("smt2", true); + } + + if(cmdline.isset("beautify")) + options.set_option("beautify", true); + + if(cmdline.isset("no-sat-preprocessor")) + options.set_option("sat-preprocessor", false); + else + options.set_option("sat-preprocessor", true); + + if(cmdline.isset("outfile")) + options.set_option("outfile", cmdline.get_value("outfile")); + + PARSE_OPTIONS_GOTO_TRACE(cmdline, options); +} + +/// invoke main modules +int ccover_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << '\n'; + return CPROVER_EXIT_SUCCESS; + } + + // + // command line options + // + + optionst options; + try + { + get_command_line_options(options); + } + + catch(const char *error_msg) + { + error() << error_msg << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(const std::string &error_msg) + { + error() << error_msg << eom; + return CPROVER_EXIT_EXCEPTION; + } + + eval_verbosity(); + + // + // Print a banner + // + status() << "CBMC version " << CBMC_VERSION << ' ' + << sizeof(void *)*8 << "-bit " + << config.this_architecture() << ' ' + << config.this_operating_system() << eom; + + // + // Unwinding of transition systems is done by hw-cbmc. + // + + if(cmdline.isset("module") || + cmdline.isset("gen-interface")) + { + error() << "This version of CBMC has no support for " + " hardware modules. Please use hw-cbmc." << eom; + return CPROVER_EXIT_USAGE_ERROR; + } + + register_language(new_ansi_c_language); + register_language(new_cpp_language); + + if(cmdline.isset("test-preprocessor")) + return test_c_preprocessor(get_message_handler()) + ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED + : CPROVER_EXIT_SUCCESS; + + if(cmdline.isset("preprocess")) + { + preprocessing(); + return CPROVER_EXIT_SUCCESS; + } + + if(cmdline.isset("show-parse-tree")) + { + if(cmdline.args.size()!=1 || + is_goto_binary(cmdline.args[0])) + { + error() << "Please give exactly one source file" << eom; + return CPROVER_EXIT_INCORRECT_TASK; + } + + std::string filename=cmdline.args[0]; + + #ifdef _MSC_VER + std::ifstream infile(widen(filename)); + #else + std::ifstream infile(filename); + #endif + + if(!infile) + { + error() << "failed to open input file `" + << filename << "'" << eom; + return CPROVER_EXIT_INCORRECT_TASK; + } + + std::unique_ptr language= + get_language_from_filename(filename); + + if(language==nullptr) + { + error() << "failed to figure out type of file `" + << filename << "'" << eom; + return CPROVER_EXIT_INCORRECT_TASK; + } + + language->get_language_options(cmdline); + language->set_message_handler(get_message_handler()); + + status() << "Parsing " << filename << eom; + + if(language->parse(infile, filename)) + { + error() << "PARSING ERROR" << eom; + return CPROVER_EXIT_INCORRECT_TASK; + } + + language->show_parse(std::cout); + return CPROVER_EXIT_SUCCESS; + } + + int get_goto_program_ret=get_goto_program(options); + + if(get_goto_program_ret!=-1) + return get_goto_program_ret; + + return ccover_bmct::do_bmc( + options, goto_model, ui_message_handler.get_ui(), get_message_handler()); +} + +int ccover_parse_optionst::get_goto_program( + const optionst &options) +{ + if(cmdline.args.empty()) + { + error() << "Please provide a program to test" << eom; + return CPROVER_EXIT_INCORRECT_TASK; + } + + try + { + goto_model=initialize_goto_model(cmdline, get_message_handler()); + + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table(goto_model, ui_message_handler.get_ui()); + return CPROVER_EXIT_SUCCESS; + } + + if(process_goto_program(options)) + return CPROVER_EXIT_INTERNAL_ERROR; + + // show it? + if(cmdline.isset("show-loops")) + { + show_loop_ids(ui_message_handler.get_ui(), goto_model); + return CPROVER_EXIT_SUCCESS; + } + + // show it? + if( + cmdline.isset("show-goto-functions") || + cmdline.isset("list-goto-functions")) + { + show_goto_functions( + goto_model, + get_message_handler(), + ui_message_handler.get_ui(), + cmdline.isset("list-goto-functions")); + return CPROVER_EXIT_SUCCESS; + } + + status() << config.object_bits_info() << eom; + } + + catch(const char *e) + { + error() << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(const std::string &e) + { + error() << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(int e) + { + error() << "Numeric exception : " << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(const std::bad_alloc &) + { + error() << "Out of memory" << eom; + return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; + } + + return -1; // no error, continue +} + +void ccover_parse_optionst::preprocessing() +{ + try + { + if(cmdline.args.size()!=1) + { + error() << "Please provide one program to preprocess" << eom; + return; + } + + std::string filename=cmdline.args[0]; + + std::ifstream infile(filename); + + if(!infile) + { + error() << "failed to open input file" << eom; + return; + } + + std::unique_ptr language=get_language_from_filename(filename); + language->get_language_options(cmdline); + + if(language==nullptr) + { + error() << "failed to figure out type of file" << eom; + return; + } + + language->set_message_handler(get_message_handler()); + + if(language->preprocess(infile, filename, std::cout)) + error() << "PREPROCESSING ERROR" << eom; + } + + catch(const char *e) + { + error() << e << eom; + } + + catch(const std::string &e) + { + error() << e << eom; + } + + catch(int e) + { + error() << "Numeric exception : " << e << eom; + } + + catch(const std::bad_alloc &) + { + error() << "Out of memory" << eom; + exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); + } +} + +bool ccover_parse_optionst::process_goto_program( + const optionst &options) +{ + try + { + // Remove inline assembler; this needs to happen before + // adding the library. + remove_asm(goto_model); + + // add the library + link_to_library( + goto_model, get_message_handler(), cprover_cpp_library_factory); + link_to_library( + goto_model, get_message_handler(), cprover_c_library_factory); + + if(cmdline.isset("string-abstraction")) + string_instrumentation(goto_model, get_message_handler()); + + // remove function pointers + status() << "Removal of function pointers and virtual functions" << eom; + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + + mm_io(goto_model); + + // instrument library preconditions + instrument_preconditions(goto_model); + + // remove returns, gcc vectors, complex + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + rewrite_union(goto_model); + + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); + + // ignore default/user-specified initialization + // of variables with static lifetime + if(cmdline.isset("nondet-static")) + { + status() << "Adding nondeterministic initialization " + "of static/global variables" << eom; + nondet_static(goto_model); + } + + if(cmdline.isset("string-abstraction")) + { + status() << "String Abstraction" << eom; + string_abstraction( + goto_model, + get_message_handler()); + } + + // add failed symbols + // needs to be done before pointer analysis + add_failed_symbols(goto_model.symbol_table); + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + // add loop ids + goto_model.goto_functions.compute_loop_numbers(); + + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing unused functions" << eom; + remove_unused_functions(goto_model, get_message_handler()); + } + + // remove skips such that trivial GOTOs are deleted and not considered + // for coverage annotation: + 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. + // Do not re-label after using the property slicer because + // this would cause the property identifiers to change. + label_properties(goto_model); + + // full slice? + if(cmdline.isset("full-slice")) + { + status() << "Performing a full slice" << eom; + if(cmdline.isset("property")) + property_slicer(goto_model, cmdline.get_values("property")); + else + full_slicer(goto_model); + } + + // remove any skips introduced since coverage instrumentation + remove_skip(goto_model); + } + + catch(const char *e) + { + error() << e << eom; + return true; + } + + catch(const std::string &e) + { + error() << e << eom; + return true; + } + + catch(int e) + { + error() << "Numeric exception : " << e << eom; + return true; + } + + catch(const std::bad_alloc &) + { + error() << "Out of memory" << eom; + exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); + return true; + } + + return false; +} + +/// display command line help +void ccover_parse_optionst::help() +{ + // clang-format off + std::cout << '\n' << banner_string("ccover", CBMC_VERSION) << '\n'; + + std::cout << + "* * Daniel Kroening * *\n" + "* * University of Oxford Computer, Science Department * *\n" + "* * kroening@kroening.com * *\n" + "\n" + "Usage: Purpose:\n" + "\n" + " ccover [-?] [-h] [--help] show help\n" + " cccover file.c ... source file names\n" + "\n" + "Test suite generation options:\n" + " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + " criteria supported are location, branch,\n" + " condition, decision, mcdc\n" + " default: location\n" + "\n" + "C/C++ frontend options:\n" + " -I path set include path (C/C++)\n" + " -D macro define preprocessor macro (C/C++)\n" + " --preprocess stop after preprocessing\n" + " --16, --32, --64 set width of int\n" + " --LP64, --ILP64, --LLP64,\n" + " --ILP32, --LP32 set width of int, long and pointers\n" + " --little-endian allow little-endian word-byte conversions\n" + " --big-endian allow big-endian word-byte conversions\n" + " --unsigned-char make \"char\" unsigned by default\n" + " --mm model set memory model (default: sc)\n" + " --arch set architecture (default: " + << configt::this_architecture() << ")\n" + " --os set operating system (default: " + << configt::this_operating_system() << ")\n" + " --c89/99/11 set C language standard (default: " + << (configt::ansi_ct::default_c_standard()== + configt::ansi_ct::c_standardt::C89?"c89": + configt::ansi_ct::default_c_standard()== + configt::ansi_ct::c_standardt::C99?"c99": + configt::ansi_ct::default_c_standard()== + configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*) + " --cpp98/03/11 set C++ language standard (default: " + << (configt::cppt::default_cpp_standard()== + configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*) + configt::cppt::default_cpp_standard()== + configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*) + configt::cppt::default_cpp_standard()== + configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*) + #ifdef _WIN32 + " --gcc use GCC as preprocessor\n" + #endif + " --no-arch don't set up an architecture\n" + " --no-library disable built-in abstract C library\n" + " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) + " --round-to-nearest rounding towards nearest even (default)\n" + " --round-to-plus-inf rounding towards plus infinity\n" + " --round-to-minus-inf rounding towards minus infinity\n" + " --round-to-zero rounding towards zero\n" + HELP_FUNCTIONS + "\n" + "Program instrumentation options:\n" + " --no-assumptions ignore user assumptions\n" + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + "\n" + "Semantic transformations:\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --nondet-static add nondeterministic initialization of variables with static lifetime\n" + "\n" + "BMC options:\n" + HELP_BMC + "\n" + "Solver options:\n" + " --object-bits n number of bits used for object addresses\n" + " --dimacs generate CNF in DIMACS format\n" + " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*) + " --boolector use Boolector\n" + " --mathsat use MathSAT\n" + " --cvc4 use CVC4\n" + " --yices use Yices\n" + " --z3 use Z3\n" + " --refine use refinement procedure (experimental)\n" + " --refine-strings use string refinement (experimental)\n" + " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) + " --string-max-length add constraint on the length of strings\n" // NOLINT(*) + " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) + " --outfile filename output formula to given file\n" + " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) + " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) + "\n" + "Other options:\n" + " --version show version and exit\n" + " --xml-ui use XML-formatted output\n" + " --json-ui use JSON-formatted output\n" + HELP_GOTO_TRACE + " --verbosity # verbosity level\n" + HELP_TIMESTAMP + "\n"; + // clang-format on +} diff --git a/src/ccover/ccover_parse_options.h b/src/ccover/ccover_parse_options.h new file mode 100644 index 00000000000..f58461d6c11 --- /dev/null +++ b/src/ccover/ccover_parse_options.h @@ -0,0 +1,91 @@ +/*******************************************************************\ + +Module: CBMC Command Line Option Processing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// CBMC Command Line Option Processing + +#ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H +#define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H + +#include +#include + +#include + +#include + +#include + +#include "ccover_bmc.h" + +class optionst; + +// clang-format off +#define CCOVER_OPTIONS \ + OPT_BMC \ + "(preprocess)(slice-by-trace):" \ + OPT_FUNCTIONS \ + "(no-simplify)(full-slice)" \ + "(debug-level):(no-propagation)(no-simplify-if)" \ + "(document-subgoals)(outfile):(test-preprocessor)" \ + "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ + "(object-bits):" \ + "(no-assumptions)" \ + "(xml-ui)(xml-interface)(json-ui)" \ + "(smt2)(fpa)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ + "(no-sat-preprocessor)" \ + "(beautify)" \ + "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ + "(refine-strings)" \ + "(string-printable)" \ + "(string-max-length):" \ + "(string-max-input-length):" \ + "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ + "(little-endian)(big-endian)" \ + OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ + "(show-symbol-table)(show-parse-tree)" \ + "(drop-unused-functions)" \ + "(verbosity):(no-library)" \ + "(nondet-static)" \ + "(version)" \ + "(cover):" \ + "(mm):" \ + OPT_TIMESTAMP \ + "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ + "(ppc-macos)(unsigned-char)" \ + "(arrays-uf-always)(arrays-uf-never)" \ + "(string-abstraction)(no-arch)(arch):" \ + "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ + OPT_GOTO_TRACE \ + "(fixedbv)" +// clang-format on + +class ccover_parse_optionst: + public parse_options_baset, + public messaget +{ +public: + virtual int doit() override; + virtual void help() override; + + ccover_parse_optionst(int argc, const char **argv); + +protected: + goto_modelt goto_model; + ui_message_handlert ui_message_handler; + + void eval_verbosity(); + void register_languages(); + void get_command_line_options(optionst &); + void preprocessing(); + int get_goto_program(const optionst &); + bool process_goto_program(const optionst &); +}; + +#endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H From 4fe02e42708e646d13fd51b93b5947a413a4f492 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 1 Aug 2018 16:03:28 +0100 Subject: [PATCH 2/3] ccover: remove preconditions --- src/ccover/ccover_parse_options.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ccover/ccover_parse_options.cpp b/src/ccover/ccover_parse_options.cpp index 6a2722f30ce..279690b96e9 100644 --- a/src/ccover/ccover_parse_options.cpp +++ b/src/ccover/ccover_parse_options.cpp @@ -542,8 +542,8 @@ bool ccover_parse_optionst::process_goto_program( mm_io(goto_model); - // instrument library preconditions - instrument_preconditions(goto_model); + // remove library preconditions + remove_preconditions(goto_model); // remove returns, gcc vectors, complex remove_returns(goto_model); From f4eb1da8ff244943887fc1094dd1dfc93023a0c0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 20 Mar 2018 15:09:53 +0000 Subject: [PATCH 3/3] cleanout test suite generation from cbmc --- jbmc/src/jbmc/Makefile | 1 - jbmc/src/jbmc/jbmc_parse_options.cpp | 27 +++++---------------------- regression/cbmc-cover/Makefile | 4 ++-- src/cbmc/Makefile | 1 - src/cbmc/bmc.cpp | 6 ------ src/cbmc/bmc.h | 5 ----- src/cbmc/cbmc_parse_options.cpp | 14 +------------- src/cbmc/cbmc_parse_options.h | 2 +- unit/Makefile | 1 - 9 files changed, 9 insertions(+), 52 deletions(-) diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index ab8c2c962aa..32a1b8d4681 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -40,7 +40,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \ diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index a4474d1edd5..8173c707693 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,9 @@ 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")); - } + options.set_option( + "unwinding-assertions", + cmdline.isset("unwinding-assertions")); // generate unwinding assumptions otherwise options.set_option( @@ -916,17 +908,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 +954,7 @@ bool jbmc_parse_optionst::process_goto_functions( full_slicer(goto_model); } - // remove any skips introduced since coverage instrumentation + // remove any skips remove_skip(goto_model); } @@ -1079,7 +1063,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/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile index 486a8c750f7..f2c4e334c5a 100644 --- a/regression/cbmc-cover/Makefile +++ b/regression/cbmc-cover/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -p -c ../../../src/cbmc/cbmc + @../test.pl -p -c ../../../src/ccover/ccover tests.log: ../test.pl - @../test.pl -p -c ../../../src/cbmc/cbmc + @../test.pl -p -c ../../../src/ccover/ccover show: @for dir in *; do \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index e1045b7bc9c..78d57081039 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -1,6 +1,5 @@ SRC = all_properties.cpp \ bmc.cpp \ - bmc_cover.cpp \ bv_cbmc.cpp \ cbmc_dimacs.cpp \ cbmc_languages.cpp \ diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 0fbc50aaa15..2b096a33135 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -380,12 +380,6 @@ safety_checkert::resultt bmct::execute( return safety_checkert::resultt::SAFE; // to indicate non-error } - if(!options.get_list_option("cover").empty()) - { - return cover(goto_functions)? - safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE; - } - if(options.get_option("localize-faults")!="") { fault_localizationt fault_localization( diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 8e812e8e1da..1068e5ff066 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -223,12 +223,7 @@ class bmct:public safety_checkert void slice(); void show(); - bool cover(const goto_functionst &goto_functions); - friend class bmc_all_propertiest; - friend class bmc_covert; - template