diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 29758db06fd..0261cca045e 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -24,13 +24,10 @@ Author: Peter Schrammel #include #include #include -#include #include #include #include -#include #include -#include #include #include @@ -71,88 +68,9 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cover")) parse_cover_options(cmdline, options); - if(cmdline.isset("mm")) - options.set_option("mm", cmdline.get_value("mm")); - // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options); - 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); - - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); - - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); - options.set_option("show-properties", cmdline.isset("show-properties")); } @@ -247,73 +165,64 @@ bool jdiff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) { - { - // remove function pointers - log.status() << "Removing function pointers and virtual functions" - << messaget::eom; - remove_function_pointers( - ui_message_handler, goto_model, cmdline.isset("pointer-check")); + // remove function pointers + log.status() << "Removing function pointers and virtual functions" + << messaget::eom; + remove_function_pointers( + ui_message_handler, goto_model, cmdline.isset("pointer-check")); - // Java virtual functions -> explicit dispatch tables: - remove_virtual_functions(goto_model); + // Java virtual functions -> explicit dispatch tables: + remove_virtual_functions(goto_model); - // remove Java throw and catch - // This introduces instanceof, so order is important: - remove_exceptions_using_instanceof(goto_model, ui_message_handler); + // remove Java throw and catch + // This introduces instanceof, so order is important: + remove_exceptions_using_instanceof(goto_model, ui_message_handler); - // Java instanceof -> clsid comparison: - class_hierarchyt class_hierarchy(goto_model.symbol_table); - remove_instanceof(goto_model, class_hierarchy, ui_message_handler); + // Java instanceof -> clsid comparison: + class_hierarchyt class_hierarchy(goto_model.symbol_table); + remove_instanceof(goto_model, class_hierarchy, ui_message_handler); - mm_io(goto_model); + mm_io(goto_model); - // instrument library preconditions - instrument_preconditions(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); + // remove returns + remove_returns(goto_model); - // add generic checks - log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check_java(options, goto_model, ui_message_handler); + // add generic checks + log.status() << "Generic Property Instrumentation" << messaget::eom; + goto_check_java(options, goto_model, ui_message_handler); - // checks don't know about adjusted float expressions - adjust_float_expressions(goto_model); + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); - // recalculate numbers, etc. - goto_model.goto_functions.update(); + // recalculate numbers, etc. + goto_model.goto_functions.update(); - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - - // remove skips such that trivial GOTOs are deleted and not considered - // for coverage annotation: + // instrument cover goals + if(cmdline.isset("cover")) + { + // 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")) - { - const auto cover_config = - get_cover_config(options, goto_model.symbol_table, ui_message_handler); - if(instrument_cover_goals(cover_config, goto_model, ui_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(); + const auto cover_config = + get_cover_config(options, goto_model.symbol_table, ui_message_handler); + if(instrument_cover_goals(cover_config, goto_model, ui_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); + return false; } @@ -335,7 +244,7 @@ void jdiff_parse_optionst::help() "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS HELP_SHOW_PROPERTIES - " --syntactic do syntactic diff (default)\n" + " --show-loops show the loops in the programs\n" " -u | --unified output unified diff\n" " --change-impact | \n" " --forward-impact |\n" diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index a37baeaf0bc..f4ad63c8cf5 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -29,6 +29,7 @@ class goto_modelt; "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ + "(show-loops)" \ OPT_GOTO_CHECK_JAVA \ OPT_COVER \ "(verbosity):(version)" \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index b835c65dcb1..9f6ce1f0ffe 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -64,6 +64,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); + options.set_option("show-properties", cmdline.isset("show-properties")); + // Options for process_goto_program options.set_option("rewrite-union", true); } @@ -224,6 +226,7 @@ void goto_diff_parse_optionst::help() "\n" "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS + HELP_SHOW_PROPERTIES " --show-loops show the loops in the programs\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 98bb75fb2e6..0b80a55faed 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -30,6 +30,7 @@ class optionst; #define GOTO_DIFF_OPTIONS \ "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(show-loops)" \ OPT_GOTO_CHECK \ OPT_COVER \