diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index ee589ca9e70..73f9b2caac4 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -29,13 +29,13 @@ void goto_check( const optionst &options, goto_modelt &goto_model); -#define GOTO_CHECK_OPTIONS \ +#define OPT_GOTO_CHECK \ "(bounds-check)(pointer-check)(memory-leak-check)" \ "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \ "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)" -#define GOTO_CHECK_HELP \ +#define HELP_GOTO_CHECK \ " --bounds-check enable array bounds checks\n" \ " --pointer-check enable pointer checks\n" \ " --memory-leak-check enable memory leak checks\n" \ @@ -48,7 +48,7 @@ void goto_check( " --float-overflow-check check floating-point for +/-Inf\n" \ " --nan-check check floating-point for NaN\n" \ -#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \ +#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ options.set_option("pointer-check", cmdline.isset("pointer-check")); \ options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 35a5002572d..443010d6191 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -220,7 +220,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("propagation", true); // all checks supported by goto_check - GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -1114,10 +1114,10 @@ void cbmc_parse_optionst::help() "Program representations:\n" " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" - " --show-goto-functions show goto program\n" + HELP_SHOW_GOTO_FUNCTIONS "\n" "Program instrumentation options:\n" - GOTO_CHECK_HELP + HELP_GOTO_CHECK " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 72387bcb4fc..f14eafc2d81 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -30,7 +30,7 @@ class optionst; "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \ "(classpath):(cp):(main-class):" \ "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ - GOTO_CHECK_OPTIONS \ + OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ "(xml-ui)(xml-interface)(json-ui)" \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index bff5e163c4f..e8d325db38b 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -112,7 +112,7 @@ void clobber_parse_optionst::get_command_line_options(optionst &options) options.set_option("unwindset", cmdline.get_value("unwindset")); // all checks supported by goto_check - GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -425,7 +425,7 @@ bool clobber_parse_optionst::process_goto_program( // show it? if(cmdline.isset("show-goto-functions")) { - goto_functions.output(ns, std::cout); + show_goto_functions(ns, get_ui(), goto_functions); return true; } } @@ -655,7 +655,7 @@ void clobber_parse_optionst::help() " --unsigned-char make \"char\" unsigned by default\n" " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" - " --show-goto-functions show goto program\n" + HELP_SHOW_GOTO_FUNCTIONS " --ppc-macos set MACOS/PPC architecture\n" " --mm model set memory model (default: sc)\n" " --arch set architecture (default: " @@ -673,7 +673,7 @@ void clobber_parse_optionst::help() " --round-to-zero IEEE floating point rounding mode\n" "\n" "Program instrumentation options:\n" - GOTO_CHECK_HELP + HELP_GOTO_CHECK " --show-properties show the properties\n" " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h index 8d1705cf0e0..ffd897c9155 100644 --- a/src/clobber/clobber_parse_options.h +++ b/src/clobber/clobber_parse_options.h @@ -15,13 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include class goto_functionst; class optionst; #define CLOBBER_OPTIONS \ "(depth):(context-bound):(unwind):" \ - GOTO_CHECK_OPTIONS \ + OPT_GOTO_CHECK \ + OPT_SHOW_GOTO_FUNCTIONS \ "(no-assertions)(no-assumptions)" \ "(error-label):(verbosity):(no-library)" \ "(version)" \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4b29d4b8548..8b36f6e71a4 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -406,9 +406,7 @@ bool goto_analyzer_parse_optionst::process_goto_program( // show it? if(cmdline.isset("show-goto-functions")) { - namespacet ns(goto_model.symbol_table); - - goto_model.goto_functions.output(ns, std::cout); + show_goto_functions(goto_model, get_ui()); return true; } @@ -521,7 +519,7 @@ void goto_analyzer_parse_optionst::help() "Program representations:\n" " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" - " --show-goto-functions show goto program\n" + HELP_SHOW_GOTO_FUNCTIONS " --show-properties show the properties, but don't run analysis\n" "\n" "Other options:\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 19b44c21910..7b319c8b99b 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include class bmct; class goto_functionst; @@ -26,7 +27,8 @@ class optionst; "(classpath):(cp):(main-class):" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ - "(show-goto-functions)(show-loops)" \ + OPT_SHOW_GOTO_FUNCTIONS \ + "(show-loops)" \ "(show-symbol-table)(show-parse-tree)" \ "(show-properties)(show-reachable-properties)(property):" \ "(verbosity):(version)" \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c819d1537d0..841230e8e32 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -335,13 +335,8 @@ int goto_diff_parse_optionst::doit() if(cmdline.isset("show-goto-functions")) { - //ENHANCE: make UI specific - std::cout << "*******************************************************\n"; - namespacet ns1(goto_model1.symbol_table); - goto_model1.goto_functions.output(ns1, std::cout); - std::cout << "*******************************************************\n"; - namespacet ns2(goto_model2.symbol_table); - goto_model2.goto_functions.output(ns2, std::cout); + show_goto_functions(goto_model1, get_ui()); + show_goto_functions(goto_model2, get_ui()); return 0; } @@ -513,7 +508,7 @@ bool goto_diff_parse_optionst::process_goto_program( // show it? if(cmdline.isset("show-goto-functions")) { - goto_functions.output(ns, std::cout); + show_goto_functions(ns, get_ui(), goto_functions); return true; } } @@ -570,7 +565,7 @@ void goto_diff_parse_optionst::help() " goto_diff old new goto binaries to be compared\n" "\n" "Diff options:\n" - " --show-functions show functions (default)\n" + HELP_SHOW_GOTO_FUNCTIONS " --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 822fd59a678..e78bd1537e7 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -15,6 +15,7 @@ Author: Peter Schrammel #include #include +#include #include "goto_diff_languages.h" @@ -23,7 +24,7 @@ class optionst; #define GOTO_DIFF_OPTIONS \ "(json-ui)" \ - "(show-goto-functions)" \ + OPT_SHOW_GOTO_FUNCTIONS \ "(verbosity):(version)" \ "u(unified)(change-impact)(forward-impact)(backward-impact)" \ "(compact-output)" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 11c3ffc6620..823227c04cc 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -576,7 +576,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-goto-functions")) { namespacet ns(symbol_table); - goto_functions.output(ns, std::cout); + show_goto_functions(ns, get_ui(), goto_functions); return 0; } @@ -885,7 +885,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() options.set_option("assert-to-assume", false); // all checks supported by goto_check - GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -1457,14 +1457,14 @@ void goto_instrument_parse_optionst::help() " --show-properties show the properties\n" " --show-symbol-table show symbol table\n" " --list-symbols list symbols with type information\n" - " --show-goto-functions show goto program\n" + HELP_SHOW_GOTO_FUNCTIONS " --list-undefined-functions list functions without body\n" " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*) " --show-natural-loops show natural loop heads\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" - GOTO_CHECK_HELP + HELP_GOTO_CHECK " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*) " --error-label label check that label is unreachable\n" " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 70bc292b85a..c8c992f23e7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -22,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com "(document-claims-latex)(document-claims-html)" \ "(document-properties-latex)(document-properties-html)" \ "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \ - GOTO_CHECK_OPTIONS \ + OPT_GOTO_CHECK \ /* no-X-check are deprecated and ignored */ \ "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \ "(no-nan-check)" \ @@ -43,7 +44,8 @@ Author: Daniel Kroening, kroening@kroening.com "(nondet-volatile)(isr):" \ "(stack-depth):(nondet-static)" \ "(function-enter):(function-exit):(branch):" \ - "(show-goto-functions)(show-value-sets)" \ + OPT_SHOW_GOTO_FUNCTIONS \ + "(show-value-sets)" \ "(show-global-may-alias)" \ "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ "(show-escape-analysis)(escape-analysis)" \ diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index 1ce37a4cee9..5bb7320963e 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -15,6 +15,12 @@ class goto_functionst; class namespacet; class goto_modelt; +#define OPT_SHOW_GOTO_FUNCTIONS \ + "(show-goto-functions)" + +#define HELP_SHOW_GOTO_FUNCTIONS \ + " --show-goto-functions show goto program\n" + void show_goto_functions( const namespacet &ns, ui_message_handlert::uit ui, diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 7a9227e6f58..ae6859624dc 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -119,7 +119,7 @@ void symex_parse_optionst::get_command_line_options(optionst &options) options.set_option("unwindset", cmdline.get_value("unwindset")); // all checks supported by goto_check - GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -409,8 +409,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // show it? if(cmdline.isset("show-goto-functions")) { - const namespacet ns(goto_model.symbol_table); - goto_model.goto_functions.output(ns, std::cout); + show_goto_functions(goto_model, get_ui()); return true; } } @@ -677,7 +676,7 @@ void symex_parse_optionst::help() " --unsigned-char make \"char\" unsigned by default\n" " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" - " --show-goto-functions show goto program\n" + HELP_SHOW_GOTO_FUNCTIONS " --ppc-macos set MACOS/PPC architecture\n" " --mm model set memory model (default: sc)\n" " --arch set architecture (default: " @@ -696,7 +695,7 @@ void symex_parse_optionst::help() " --function name set main function name\n" "\n" "Program instrumentation options:\n" - GOTO_CHECK_HELP + HELP_GOTO_CHECK " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 0ae56a9c6b8..a67469d71e5 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -27,7 +28,7 @@ class optionst; "(function):" \ "D:I:" \ "(depth):(context-bound):(branch-bound):(unwind):" \ - GOTO_CHECK_OPTIONS \ + OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ @@ -39,7 +40,8 @@ class optionst; "(ppc-macos)(unsigned-char)" \ "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ - "(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \ + "(show-locs)(show-vcc)(show-properties)" \ + OPT_SHOW_GOTO_FUNCTIONS \ "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ "(no-simplify)(no-unwinding-assertions)(no-propagation)" // the last line is for CBMC-regression testing only