From f4a8b0c91eb712f54d814ca102824d9268ffdcd8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 23:41:39 +0000 Subject: [PATCH 1/7] Replace cout in show_properties All output should be printed to message streams --- src/cbmc/cbmc_parse_options.cpp | 3 +- src/clobber/clobber_parse_options.cpp | 2 +- .../goto_analyzer_parse_options.cpp | 2 +- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/show_properties.cpp | 30 +++++++++++-------- src/goto-programs/show_properties.h | 3 ++ src/jbmc/jbmc_parse_options.cpp | 3 +- 7 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 3496c6bf8ec..9ebe47ea07c 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -534,7 +534,8 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { - show_properties(goto_model, ui_message_handler.get_ui()); + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 3f36a615272..fa04de3bed2 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -150,7 +150,7 @@ int clobber_parse_optionst::doit() if(cmdline.isset("show-properties")) { - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return 0; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2e4a97b3b0e..9fa1daf7ece 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -592,7 +592,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a98acd741f6..3364ef87334 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -532,7 +532,7 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("show-properties")) { const namespacet ns(goto_model.symbol_table); - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 3393923ca75..7abf36cca5e 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -46,13 +46,14 @@ optionalt find_property( return { }; } - void show_properties( const namespacet &ns, const irep_idt &identifier, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program) { + messaget msg(message_handler); for(const auto &ins : goto_program.instructions) { if(!ins.is_assert()) @@ -83,7 +84,7 @@ void show_properties( xml_property.new_element("expression").data= from_expr(ns, identifier, ins.guard); - std::cout << xml_property << '\n'; + msg.result() << xml_property; } break; @@ -92,14 +93,13 @@ void show_properties( break; case ui_message_handlert::uit::PLAIN: - std::cout << "Property " << property_id << ":\n"; + msg.result() << "Property " << property_id << ":\n"; - std::cout << " " << ins.source_location << '\n' - << " " << description << '\n' - << " " << from_expr(ns, identifier, ins.guard) - << '\n'; + msg.result() << " " << ins.source_location << '\n' + << " " << description << '\n' + << " " << from_expr(ns, identifier, ins.guard) << '\n'; - std::cout << '\n'; + msg.result() << messaget::eom; break; default: @@ -147,8 +147,10 @@ void show_properties_json( void show_properties_json( const namespacet &ns, + message_handlert &message_handler, const goto_functionst &goto_functions) { + messaget msg(message_handler); json_arrayt json_properties; for(const auto &fct : goto_functions.function_map) @@ -161,29 +163,31 @@ void show_properties_json( json_objectt json_result; json_result["properties"] = json_properties; - std::cout << ",\n" << json_result; + msg.result() << json_result; } void show_properties( const namespacet &ns, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions) { if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, goto_functions); + show_properties_json(ns, message_handler, goto_functions); else for(const auto &fct : goto_functions.function_map) if(!fct.second.is_inlined()) - show_properties(ns, fct.first, ui, fct.second.body); + show_properties(ns, fct.first, message_handler, ui, fct.second.body); } void show_properties( const goto_modelt &goto_model, + message_handlert &message_handler, ui_message_handlert::uit ui) { const namespacet ns(goto_model.symbol_table); if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, goto_model.goto_functions); + show_properties_json(ns, message_handler, goto_model.goto_functions); else - show_properties(ns, ui, goto_model.goto_functions); + show_properties(ns, message_handler, ui, goto_model.goto_functions); } diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 145a195fa8d..12368870b8a 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -19,13 +19,16 @@ class namespacet; class goto_modelt; class symbol_tablet; class goto_functionst; +class message_handlert; void show_properties( const goto_modelt &, + message_handlert &message_handler, ui_message_handlert::uit ui); void show_properties( const namespacet &ns, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions); diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index dc45b4830ed..21d506cbc63 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -484,7 +484,8 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("show-properties")) { - show_properties(goto_model, ui_message_handler.get_ui()); + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); return 0; // should contemplate EX_OK from sysexits.h } From 937b5f98201e9bd64e8f6408149bcaab0bcd55ae Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 23:42:48 +0000 Subject: [PATCH 2/7] Expose conversion of properties of a goto-program into a JSON array so that it can be reused to goto-diff --- src/goto-programs/show_properties.cpp | 9 ++------- src/goto-programs/show_properties.h | 12 ++++++++++++ 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 7abf36cca5e..6df2f69bf33 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -108,8 +108,7 @@ void show_properties( } } - -void show_properties_json( +void convert_properties_json( json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, @@ -155,11 +154,7 @@ void show_properties_json( for(const auto &fct : goto_functions.function_map) if(!fct.second.is_inlined()) - show_properties_json( - json_properties, - ns, - fct.first, - fct.second.body); + convert_properties_json(json_properties, ns, fct.first, fct.second.body); json_objectt json_result; json_result["properties"] = json_properties; diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 12368870b8a..017fc7595b1 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; class goto_modelt; class symbol_tablet; +class goto_programt; class goto_functionst; class message_handlert; @@ -43,4 +44,15 @@ optionalt find_property( const irep_idt &property, const goto_functionst &goto_functions); +/// \brief Collects the properties in the goto program into a `json_arrayt` +/// \param json_properties: JSON array to hold the properties +/// \param ns: namespace +/// \param identifier: function id of the goto program +/// \param goto_program: the goto program +void convert_properties_json( + json_arrayt &json_properties, + const namespacet &ns, + const irep_idt &identifier, + const goto_programt &goto_program); + #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H From a0c45f4a88601924f7c2d1138b958df8fb907039 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 23:43:34 +0000 Subject: [PATCH 3/7] Factor out show properties command line def and docs to avoid repetition across the CPROVER tools --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/cbmc/cbmc_parse_options.h | 4 ++-- src/clobber/clobber_parse_options.h | 6 +++++- src/goto-analyzer/goto_analyzer_parse_options.cpp | 5 +++-- src/goto-analyzer/goto_analyzer_parse_options.h | 6 +++++- src/goto-instrument/goto_instrument_parse_options.cpp | 4 +++- src/goto-instrument/goto_instrument_parse_options.h | 9 ++++++--- src/goto-programs/show_properties.h | 8 ++++++++ src/jbmc/jbmc_parse_options.cpp | 4 +++- src/jbmc/jbmc_parse_options.h | 3 ++- 10 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 9ebe47ea07c..1048b322a0f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -924,7 +924,7 @@ void cbmc_parse_optionst::help() " cbmc file.c ... source file names\n" "\n" "Analysis options:\n" - " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) + HELP_SHOW_PROPERTIES " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 658c552c22e..c5fe31e6b88 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -53,9 +53,9 @@ class optionst; "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-claims)(claim):(show-properties)" \ "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ @@ -72,7 +72,7 @@ class optionst; "(graphml-witness):" \ "(localize-faults)(localize-faults-method):" \ OPT_GOTO_TRACE \ - "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) + "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on class cbmc_parse_optionst: diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h index eb543f60138..2cbdd3c5523 100644 --- a/src/clobber/clobber_parse_options.h +++ b/src/clobber/clobber_parse_options.h @@ -19,23 +19,27 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include class goto_functionst; class optionst; +// clang-format off #define CLOBBER_OPTIONS \ "(depth):(context-bound):(unwind):" \ OPT_GOTO_CHECK \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(no-assertions)(no-assumptions)" \ "(error-label):(verbosity):(no-library)" \ "(version)" \ "(string-abstraction)" \ - "(show-locs)(show-vcc)(show-properties)(show-trace)" \ + "(show-locs)(show-vcc)(show-trace)" \ "(property):" \ JAVA_BYTECODE_LANGUAGE_OPTIONS +// clang-format on class clobber_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9fa1daf7ece..e686facd388 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -815,6 +815,7 @@ void goto_analyzer_parse_optionst::help() std::cout << " * *\n"; + // clang-format off std::cout << "* * Daniel Kroening, DiffBlue * *\n" "* * kroening@kroening.com * *\n" @@ -898,8 +899,7 @@ void goto_analyzer_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" HELP_SHOW_GOTO_FUNCTIONS - // NOLINTNEXTLINE(whitespace/line_length) - " --show-properties show the properties, but don't run analysis\n" + HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK @@ -908,4 +908,5 @@ void goto_analyzer_parse_optionst::help() " --version show version and exit\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index d47f4ae91d3..ab1ff8b90cf 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -109,6 +109,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -119,6 +120,7 @@ class bmct; class goto_functionst; class optionst; +// clang-format off #define GOTO_ANALYSER_OPTIONS \ OPT_FUNCTIONS \ "D:I:(std89)(std99)(std11)" \ @@ -126,10 +128,11 @@ class optionst; "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)" \ - "(show-properties)(show-reachable-properties)(property):" \ + "(show-reachable-properties)(property):" \ "(verbosity):(version)" \ "(gcc)(arch):" \ "(taint):(show-taint)" \ @@ -147,6 +150,7 @@ class optionst; "(location-sensitive)(concurrent)" \ "(no-simplify-slicing)" \ JAVA_BYTECODE_LANGUAGE_OPTIONS +// clang-format on class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3364ef87334..796a47ae508 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1452,6 +1452,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() /// display command line help void goto_instrument_parse_optionst::help() { + // clang-format off std::cout << "\n" "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" // NOLINT(*) @@ -1475,7 +1476,7 @@ void goto_instrument_parse_optionst::help() "\n" "Diagnosis:\n" " --show-loops show the loops in the program\n" - " --show-properties show the properties\n" + HELP_SHOW_PROPERTIES " --show-symbol-table show symbol table\n" " --list-symbols list symbols with type information\n" HELP_SHOW_GOTO_FUNCTIONS @@ -1570,4 +1571,5 @@ void goto_instrument_parse_optionst::help() " --json-ui use JSON-formatted output\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 19acc24b44f..77e69dded9f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -18,10 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include +// clang-format off #define GOTO_INSTRUMENT_OPTIONS \ "(all)" \ "(document-claims-latex)(document-claims-html)" \ @@ -51,6 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com "(stack-depth):(nondet-static)" \ "(function-enter):(function-exit):(branch):" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(drop-unused-functions)" \ "(show-value-sets)" \ "(show-global-may-alias)" \ @@ -64,7 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_REMOVE_CONST_FUNCTION_POINTERS \ "(print-internal-representation)" \ "(remove-function-pointers)" \ - "(show-claims)(show-properties)(property):" \ + "(show-claims)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ "(cav11)" \ OPT_TIMESTAMP \ @@ -81,8 +84,8 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)(print-path-lengths)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ - "(splice-call):" \ - + "(splice-call):" +// clang-format on class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 017fc7595b1..ce4cb341c25 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -22,6 +22,14 @@ class goto_programt; class goto_functionst; class message_handlert; +// clang-format off +#define OPT_SHOW_PROPERTIES \ + "(show-properties)" + +#define HELP_SHOW_PROPERTIES \ + " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) +// clang-format on + void show_properties( const goto_modelt &, message_handlert &message_handler, diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 21d506cbc63..65075e12abf 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -878,6 +878,7 @@ void jbmc_parse_optionst::help() std::cout << " * *\n"; + // clang-format off std::cout << "* * Daniel Kroening, Edmund Clarke * *\n" "* * Carnegie Mellon University, Computer Science Department * *\n" @@ -889,7 +890,7 @@ void jbmc_parse_optionst::help() " jbmc class name of class to be checked\n" "\n" "Analysis options:\n" - " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) + HELP_SHOW_PROPERTIES " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) @@ -962,4 +963,5 @@ void jbmc_parse_optionst::help() " --verbosity # verbosity level\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 362011b8f33..c2793540805 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -55,7 +56,7 @@ class optionst; OPT_SHOW_GOTO_FUNCTIONS \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-properties)" \ + OPT_SHOW_PROPERTIES \ "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(verbosity):" \ From a0e50637a6fa4255c0b090d8ac18bb4167813946 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 23:44:14 +0000 Subject: [PATCH 4/7] Enable goto check and cover options in goto-diff to be able to compare properties. The java options are added to be able to use --java-throw-runtime-exceptions. --- src/goto-diff/CMakeLists.txt | 1 + src/goto-diff/Makefile | 12 +++ src/goto-diff/goto_diff_parse_options.cpp | 120 ++++++++++++++-------- src/goto-diff/goto_diff_parse_options.h | 6 ++ 4 files changed, 95 insertions(+), 44 deletions(-) diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 39f4bf011ec..2839634244c 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -13,6 +13,7 @@ target_link_libraries(goto-diff-lib linking big-int pointer-analysis + goto-instrument-lib goto-programs assembler analyses diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 986085eb307..22304c2a5b7 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -15,6 +15,18 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../pointer-analysis/pointer-analysis$(LIBEXT) \ + ../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-symex/adjust_float_expressions$(OBJEXT) \ + ../goto-symex/rewrite_union$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 87e8c98e5d2..06bbe92a1c7 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -20,16 +20,23 @@ Author: Peter Schrammel #include #include #include +#include #include #include +#include +#include #include +#include +#include #include +#include #include #include #include #include +#include #include #include #include @@ -39,6 +46,11 @@ Author: Peter Schrammel #include #include +#include +#include + +#include + #include #include @@ -99,7 +111,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-vcc", true); if(cmdline.isset("cover")) - options.set_option("cover", cmdline.get_value("cover")); + parse_cover_options(cmdline, options); if(cmdline.isset("mm")) options.set_option("mm", cmdline.get_value("mm")); @@ -122,22 +134,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) 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("all-claims") || // will go away - cmdline.isset("all-properties")) // use this one - options.set_option("all-properties", true); - else - options.set_option("all-properties", false); - - if(cmdline.isset("unwind")) - options.set_option("unwind", cmdline.get_value("unwind")); - - if(cmdline.isset("depth")) - options.set_option("depth", cmdline.get_value("depth")); + // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); if(cmdline.isset("debug-level")) options.set_option("debug-level", cmdline.get_value("debug-level")); @@ -308,10 +306,6 @@ int goto_diff_parse_optionst::doit() cmdline.isset("forward-impact") || cmdline.isset("backward-impact")) { - // Workaround to avoid deps not propagating between return and end_func - remove_returns(goto_model1); - remove_returns(goto_model2); - impact_modet impact_mode= cmdline.isset("forward-impact") ? impact_modet::FORWARD : @@ -393,6 +387,9 @@ int goto_diff_parse_optionst::get_goto_program( goto_model.goto_functions, ui_message_handler); + if(process_goto_program(options, goto_model)) + return 6; + // if we had a second argument then we will handle it next if(arg2!="") cmdline.args[0]=arg2; @@ -405,46 +402,72 @@ bool goto_diff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) { - symbol_tablet &symbol_table = goto_model.symbol_table; - goto_functionst &goto_functions = goto_model.goto_functions; - try { - namespacet ns(symbol_table); - // Remove inline assembler; this needs to happen before // adding the library. remove_asm(goto_model); // add the library - link_to_library(symbol_table, goto_functions, ui_message_handler); + link_to_library(goto_model, get_message_handler()); // remove function pointers - status() << "Function Pointer Removal" << eom; + status() << "Removal of function pointers and virtual functions" << eom; remove_function_pointers( - get_message_handler(), - symbol_table, - goto_functions, - cmdline.isset("pointer-check")); + get_message_handler(), goto_model, cmdline.isset("pointer-check")); + + // Java virtual functions -> explicit dispatch tables: + remove_virtual_functions(goto_model); + // remove catch and throw + remove_exceptions(goto_model); + // Java instanceof -> clsid comparison: + remove_instanceof(goto_model); - // do partial inlining - status() << "Partial Inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler); + mm_io(goto_model); + + // instrument library preconditions + instrument_preconditions(goto_model); // remove returns, gcc vectors, complex - remove_returns(symbol_table, goto_functions); - remove_vector(symbol_table, goto_functions); - remove_complex(symbol_table, goto_functions); + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + rewrite_union(goto_model); + + // add generic checks + status() << "Generic Property Instrumentation" << eom; + goto_check(options, goto_model); - // add failed symbols - // needs to be done before pointer analysis - add_failed_symbols(symbol_table); + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); + + // 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); + + // remove any skips introduced since coverage instrumentation + remove_skip(goto_model); + goto_model.goto_functions.update(); } catch(const char *e) @@ -459,14 +482,16 @@ bool goto_diff_parse_optionst::process_goto_program( return true; } - catch(int) + 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; } @@ -476,6 +501,7 @@ bool goto_diff_parse_optionst::process_goto_program( /// display command line help void goto_diff_parse_optionst::help() { + // clang-format off std::cout << "\n" // NOLINTNEXTLINE(whitespace/line_length) @@ -498,9 +524,15 @@ void goto_diff_parse_optionst::help() " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" " --compact-output output dependencies in compact mode\n" "\n" + "Program instrumentation options:\n" + HELP_GOTO_CHECK + " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + "Java Bytecode frontend options:\n" + JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP "Other options:\n" " --version show version and exit\n" " --json-ui use JSON-formatted output\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 8eb8e58f1c2..ea6756edcc0 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -12,6 +12,8 @@ Author: Peter Schrammel #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H #define CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H +#include + #include #include #include @@ -24,13 +26,17 @@ Author: Peter Schrammel class goto_modelt; class optionst; +// clang-format off #define GOTO_DIFF_OPTIONS \ "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_GOTO_CHECK \ + "(cover):" \ "(verbosity):(version)" \ OPT_TIMESTAMP \ "u(unified)(change-impact)(forward-impact)(backward-impact)" \ "(compact-output)" +// clang-format on class goto_diff_parse_optionst: public parse_options_baset, From d3eb1f3e42582412f3fb1ebb3cc9fea9ed3da0d9 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 23:44:38 +0000 Subject: [PATCH 5/7] Use CPROVER exit codes --- src/goto-diff/goto_diff_parse_options.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 06bbe92a1c7..c8e35b1bacd 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -242,7 +242,7 @@ int goto_diff_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; + return CPROVER_EXIT_SUCCESS; } // @@ -264,7 +264,7 @@ int goto_diff_parse_optionst::doit() if(cmdline.args.size()!=2) { error() << "Please provide two programs to compare" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } goto_modelt goto_model1, goto_model2; @@ -282,7 +282,7 @@ int goto_diff_parse_optionst::doit() { show_loop_ids(get_ui(), goto_model1); show_loop_ids(get_ui(), goto_model2); - return true; + return CPROVER_EXIT_SUCCESS; } if( @@ -299,7 +299,7 @@ int goto_diff_parse_optionst::doit() get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("change-impact") || @@ -318,7 +318,7 @@ int goto_diff_parse_optionst::doit() impact_mode, cmdline.isset("compact-output")); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("unified") || @@ -328,7 +328,7 @@ int goto_diff_parse_optionst::doit() u(); u.output(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } syntactic_difft sd(goto_model1, goto_model2, get_message_handler()); @@ -336,7 +336,7 @@ int goto_diff_parse_optionst::doit() sd(); sd.output_functions(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } int goto_diff_parse_optionst::get_goto_program( @@ -353,7 +353,7 @@ int goto_diff_parse_optionst::get_goto_program( goto_model.symbol_table, goto_model.goto_functions, languages.get_message_handler())) - return 6; + return CPROVER_EXIT_INCORRECT_TASK; config.set(cmdline); @@ -374,7 +374,7 @@ int goto_diff_parse_optionst::get_goto_program( if(languages.parse() || languages.typecheck() || languages.final()) - return 6; + return CPROVER_EXIT_INCORRECT_TASK; // we no longer need any parse trees or language files languages.clear_parse(); @@ -388,7 +388,7 @@ int goto_diff_parse_optionst::get_goto_program( ui_message_handler); if(process_goto_program(options, goto_model)) - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; // if we had a second argument then we will handle it next if(arg2!="") From a4d3dc3771f9db48adba1b8fcde722424960b56d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 18 Feb 2018 10:16:14 +0000 Subject: [PATCH 6/7] Show properties in goto-diff Shows properties for each new/modified/deleted function. For now, for modified functions all properties are shown regardless of whether they are affected by the modification or not. --- src/goto-diff/goto_diff.h | 44 ++++-- src/goto-diff/goto_diff_base.cpp | 165 ++++++++++++++-------- src/goto-diff/goto_diff_parse_options.cpp | 9 +- src/goto-diff/goto_diff_parse_options.h | 2 + src/goto-diff/syntactic_diff.h | 9 +- 5 files changed, 149 insertions(+), 80 deletions(-) diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h index 23a65221358..0c637363e20 100644 --- a/src/goto-diff/goto_diff.h +++ b/src/goto-diff/goto_diff.h @@ -19,43 +19,57 @@ Author: Peter Schrammel #include +class optionst; + class goto_difft:public messaget { public: - explicit goto_difft( + goto_difft( const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, - message_handlert &_message_handler - ) - : - messaget(_message_handler), - goto_model1(_goto_model1), - goto_model2(_goto_model2), - ui(ui_message_handlert::uit::PLAIN), - total_functions_count(0) - {} + const optionst &_options, + message_handlert &_message_handler) + : messaget(_message_handler), + goto_model1(_goto_model1), + goto_model2(_goto_model2), + options(_options), + ui(ui_message_handlert::uit::PLAIN), + total_functions_count(0) + { + } virtual bool operator()()=0; void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } - virtual std::ostream &output_functions(std::ostream &out) const; + virtual void output_functions() const; protected: const goto_modelt &goto_model1; const goto_modelt &goto_model2; + const optionst &options; ui_message_handlert::uit ui; unsigned total_functions_count; typedef std::set irep_id_sett; irep_id_sett new_functions, modified_functions, deleted_functions; - void convert_function_group( + void output_function_group( + const std::string &group_name, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const; + void output_function( + const irep_idt &function_name, + const goto_modelt &goto_model) const; + + void convert_function_group_json( json_arrayt &result, - const irep_id_sett &function_group) const; - void convert_function( + const irep_id_sett &function_group, + const goto_modelt &goto_model) const; + void convert_function_json( json_objectt &result, - const irep_idt &function_name) const; + const irep_idt &function_name, + const goto_modelt &goto_model) const; }; #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_H diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 32b6b2949af..49f79b9858d 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -11,40 +11,26 @@ Author: Peter Schrammel #include "goto_diff.h" +#include + #include +#include -std::ostream &goto_difft::output_functions(std::ostream &out) const +/// Output diff result +void goto_difft::output_functions() const { - namespacet ns1(goto_model1.symbol_table); - namespacet ns2(goto_model2.symbol_table); switch(ui) { case ui_message_handlert::uit::PLAIN: { - out << "total number of functions: " << total_functions_count << "\n"; - out << "new functions:\n"; - for(irep_id_sett::const_iterator it=new_functions.begin(); - it!=new_functions.end(); ++it) - { - const symbolt &symbol = ns2.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } - - out << "modified functions:\n"; - for(irep_id_sett::const_iterator it=modified_functions.begin(); - it!=modified_functions.end(); ++it) - { - const symbolt &symbol = ns2.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } - - out << "deleted functions:\n"; - for(irep_id_sett::const_iterator it=deleted_functions.begin(); - it!=deleted_functions.end(); ++it) - { - const symbolt &symbol = ns1.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } + result() << "total number of functions: " << total_functions_count + << '\n'; + output_function_group("new functions", new_functions, goto_model2); + output_function_group( + "modified functions", modified_functions, goto_model2); + output_function_group( + "deleted functions", deleted_functions, goto_model1); + result() << eom; break; } case ui_message_handlert::uit::JSON_UI: @@ -52,54 +38,115 @@ std::ostream &goto_difft::output_functions(std::ostream &out) const json_objectt json_result; json_result["totalNumberOfFunctions"]= json_stringt(std::to_string(total_functions_count)); - convert_function_group - (json_result["newFunctions"].make_array(), new_functions); - convert_function_group( - json_result["modifiedFunctions"].make_array(), modified_functions); - convert_function_group( - json_result["deletedFunctions"].make_array(), deleted_functions); - out << ",\n" << json_result; + convert_function_group_json( + json_result["newFunctions"].make_array(), new_functions, goto_model2); + convert_function_group_json( + json_result["modifiedFunctions"].make_array(), + modified_functions, + goto_model2); + convert_function_group_json( + json_result["deletedFunctions"].make_array(), + deleted_functions, + goto_model1); + result() << json_result; break; } case ui_message_handlert::uit::XML_UI: { - out << "not supported yet"; + error() << "XML output not supported yet" << eom; } } - return out; } -void goto_difft::convert_function_group( - json_arrayt &result, - const irep_id_sett &function_group) const +/// Output group of functions in plain text format +/// \param group_name: the name of the group, e.g. "modified functions" +/// \param function_group: set of function ids in the group +/// \param goto_model: the goto model +void goto_difft::output_function_group( + const std::string &group_name, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const { - for(irep_id_sett::const_iterator it=function_group.begin(); - it!=function_group.end(); ++it) + result() << group_name << ":\n"; + for(const auto &function_name : function_group) { - convert_function(result.push_back(jsont()).make_object(), *it); + output_function(function_name, goto_model); } } -void goto_difft::convert_function( - json_objectt &result, - const irep_idt &function_name) const +/// Output function information in plain text format +/// \param function_name: the function id +/// \param goto_model: the goto model +void goto_difft::output_function( + const irep_idt &function_name, + const goto_modelt &goto_model) const +{ + namespacet ns(goto_model.symbol_table); + const symbolt &symbol = ns.lookup(function_name); + + result() << " " << symbol.location.get_file() << ": " << function_name + << '\n'; + + if(options.get_bool_option("show-properties")) + { + const auto goto_function_it = + goto_model.goto_functions.function_map.find(function_name); + CHECK_RETURN( + goto_function_it != goto_model.goto_functions.function_map.end()); + const goto_programt &goto_program = goto_function_it->second.body; + + for(const auto &ins : goto_program.instructions) + { + if(!ins.is_assert()) + continue; + + const source_locationt &source_location = ins.source_location; + irep_idt property_id = source_location.get_property_id(); + result() << " " << property_id << '\n'; + } + } +} + +/// Convert a function group to JSON +/// \param result: the JSON array to be populated +/// \param function_group: set of function ids in the group +/// \param goto_model: the goto model +void goto_difft::convert_function_group_json( + json_arrayt &result, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const { - // the function may be in goto_model1 or goto_model2 - if( - goto_model1.goto_functions.function_map.find(function_name) != - goto_model1.goto_functions.function_map.end()) + for(const auto &function_name : function_group) { - const symbolt &symbol = - namespacet(goto_model1.symbol_table).lookup(function_name); - result["sourceLocation"] = json(symbol.location); + convert_function_json( + result.push_back(jsont()).make_object(), function_name, goto_model); } - else if( - goto_model2.goto_functions.function_map.find(function_name) != - goto_model2.goto_functions.function_map.end()) +} + +/// Convert function information to JSON +/// \param result: the JSON object to be populated +/// \param function_name: the function id +/// \param goto_model: the goto model +void goto_difft::convert_function_json( + json_objectt &result, + const irep_idt &function_name, + const goto_modelt &goto_model) const +{ + namespacet ns(goto_model.symbol_table); + const symbolt &symbol = ns.lookup(function_name); + + result["name"] = json_stringt(id2string(function_name)); + result["sourceLocation"] = json(symbol.location); + + if(options.get_bool_option("show-properties")) { - const symbolt &symbol = - namespacet(goto_model2.symbol_table).lookup(function_name); - result["sourceLocation"] = json(symbol.location); + const auto goto_function_it = + goto_model.goto_functions.function_map.find(function_name); + CHECK_RETURN( + goto_function_it != goto_model.goto_functions.function_map.end()); + const goto_programt &goto_program = goto_function_it->second.body; + + convert_properties_json( + result["properties"].make_array(), ns, function_name, goto_program); } - result["name"]=json_stringt(id2string(function_name)); } diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c8e35b1bacd..232ebf029b3 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -53,6 +53,8 @@ Author: Peter Schrammel #include +#include + #include #include @@ -234,6 +236,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) << " must not be given together" << eom; exit(1); } + + options.set_option("show-properties", cmdline.isset("show-properties")); } /// invoke main modules @@ -331,10 +335,10 @@ int goto_diff_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } - syntactic_difft sd(goto_model1, goto_model2, get_message_handler()); + syntactic_difft sd(goto_model1, goto_model2, options, get_message_handler()); sd.set_ui(get_ui()); sd(); - sd.output_functions(std::cout); + sd.output_functions(); return CPROVER_EXIT_SUCCESS; } @@ -516,6 +520,7 @@ void goto_diff_parse_optionst::help() "\n" "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS + HELP_SHOW_PROPERTIES " --syntactic do syntactic diff (default)\n" " -u | --unified output unified diff\n" " --change-impact | \n" diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index ea6756edcc0..48dcb89aa43 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -20,6 +20,7 @@ Author: Peter Schrammel #include #include +#include #include "goto_diff_languages.h" @@ -30,6 +31,7 @@ class optionst; #define GOTO_DIFF_OPTIONS \ "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ "(cover):" \ "(verbosity):(version)" \ diff --git a/src/goto-diff/syntactic_diff.h b/src/goto-diff/syntactic_diff.h index 8496eb8165e..b5a2b3216e2 100644 --- a/src/goto-diff/syntactic_diff.h +++ b/src/goto-diff/syntactic_diff.h @@ -16,12 +16,13 @@ Author: Peter Schrammel class syntactic_difft:public goto_difft { - public: - explicit syntactic_difft( +public: + syntactic_difft( const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, - message_handlert &_message_handler): - goto_difft(_goto_model1, _goto_model2, _message_handler) + const optionst &_options, + message_handlert &_message_handler) + : goto_difft(_goto_model1, _goto_model2, _options, _message_handler) { } From df9aab51ab141cecc1466d2e364bccece4d61aaf Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Feb 2018 22:53:14 +0000 Subject: [PATCH 7/7] Test for goto-diff show properties --- regression/goto-diff/java-properties/new.jar | Bin 0 -> 775 bytes .../goto-diff/java-properties/new/Test.java | 19 ++++++++++++++++++ regression/goto-diff/java-properties/old.jar | Bin 0 -> 770 bytes .../goto-diff/java-properties/old/Test.java | 19 ++++++++++++++++++ .../goto-diff/java-properties/test.desc | 10 +++++++++ 5 files changed, 48 insertions(+) create mode 100644 regression/goto-diff/java-properties/new.jar create mode 100644 regression/goto-diff/java-properties/new/Test.java create mode 100644 regression/goto-diff/java-properties/old.jar create mode 100644 regression/goto-diff/java-properties/old/Test.java create mode 100644 regression/goto-diff/java-properties/test.desc diff --git a/regression/goto-diff/java-properties/new.jar b/regression/goto-diff/java-properties/new.jar new file mode 100644 index 0000000000000000000000000000000000000000..d77d86e9ce37e311fb6664592c6921bd4b8b1741 GIT binary patch literal 775 zcmWIWW@Zs#;Nak3c)m5zhXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EVuUN6pm~7{ zC>xSmT%wnplUQ6F8*tF?kb}saT<=WpiCv47K0ffZ=wN^B`snD97M8CJh96U=MQ!O= z+qlU7$;58MHWy+01N}zl%y?Cn-TeOT>}>PR>+Sc?zt6z8@$CT@)qY-fDJ`?Z%ebN| zLs+>cyQnR!pUg7Z<-nUSGx}M3*5tJY&X~jTqWY`$qU9fR6#`zh1Qr<9zF~hn?@fQl zi)M?o>h-bt+#zsR3^8hp)U@q<)@UY0e}>`#4}lV>CQ`(We>j%`MFVuVO#VU(;KTEBb_`zAWv+?9t6TbofIx&Fk}v@_o~U&*mtRhQp*&9!1p zMtWgY>Bpw5S4TE)F$rF9X6C1+ZIhE6{Prk+pTDXs!aMi+e{jH8sNFp5$jHEO9f$+G z8JR>FP*V>qX@F7>Du5>kP+CIQiX5Myw1WV)Kqg!(Qc6NL0Tl1Z4g 10) { + return x; + } else { + return x * 10; + } + } + + public void newfun() { + } +} diff --git a/regression/goto-diff/java-properties/old.jar b/regression/goto-diff/java-properties/old.jar new file mode 100644 index 0000000000000000000000000000000000000000..273b209df38e4f78270695c446fede39e5a16f12 GIT binary patch literal 770 zcmWIWW@Zs#;Nak3xVtsbhXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EVuUL$qj`Y~ zC>xSmT%wnplUQ6F8{q4I$U$Vz(xn&pSw0F|O6nhQ)H~LFq`Q-o^A%&#qmx^s)8TvLnKX7OoFY|5IHx@2;--rbW z7c9Rty|6-i@k)^mRm_h%8)kl;TOo5gm~rvNJ!;j{?zu8OjkD>~OJA%oi|3DmV)C8k zn#X(dHfsmG^0u$p^`%C(ldw&WjIc?LjfWmy6}T4I=}?O&|{NW@Hj! zKutKXQ~^pjr~sZ4K* 10) { + return x; + } else { + return x * 10; + } + } + + public void obsolete() { + } +} diff --git a/regression/goto-diff/java-properties/test.desc b/regression/goto-diff/java-properties/test.desc new file mode 100644 index 00000000000..a615e2bf421 --- /dev/null +++ b/regression/goto-diff/java-properties/test.desc @@ -0,0 +1,10 @@ +CORE +new.jar +old.jar --json-ui --show-properties --cover location +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 + "deletedFunctions": \[\n {\n "name": "java::Test\.obsolete:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.2",\n "sourceLocation": {\n "bytecodeIndex": "3",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.3",\n "sourceLocation": {\n "bytecodeIndex": "5",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4,7",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.4",\n "sourceLocation": {\n "bytecodeIndex": "6",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n {\n "name": "java::Test\.newfun:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n +-- +^warning: ignoring