-
Notifications
You must be signed in to change notification settings - Fork 273
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[RFC] Refactor command line options #4404
Open
peterschrammel
wants to merge
2
commits into
diffblue:develop
Choose a base branch
from
peterschrammel:refactor-parse-options
base: develop
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected] | |
| #include <util/make_unique.h> | ||
| #include <util/unicode.h> | ||
| #include <util/version.h> | ||
| #include <util/xml.h> | ||
|
|
||
| #include <langapi/language.h> | ||
|
|
||
|
|
@@ -83,7 +84,7 @@ Author: Daniel Kroening, [email protected] | |
| #include "xml_interface.h" | ||
|
|
||
| cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) | ||
| : parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler), | ||
| : parse_options_baset(cbmc_options.to_option_string(), argc, argv, ui_message_handler), | ||
| xml_interfacet(cmdline), | ||
| messaget(ui_message_handler), | ||
| ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) | ||
|
|
@@ -93,9 +94,9 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) | |
| ::cbmc_parse_optionst::cbmc_parse_optionst( | ||
| int argc, | ||
| const char **argv, | ||
| const std::string &extra_options) | ||
| const cmdline_definitiont &extra_options) | ||
| : parse_options_baset( | ||
| CBMC_OPTIONS + extra_options, | ||
| (cbmc_options + extra_options).to_option_string(), | ||
| argc, | ||
| argv, | ||
| ui_message_handler), | ||
|
|
@@ -915,121 +916,35 @@ bool cbmc_parse_optionst::process_goto_program( | |
| /// display command line help | ||
| void cbmc_parse_optionst::help() | ||
| { | ||
| // clang-format off | ||
| std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n' | ||
| << align_center_with_border("Copyright (C) 2001-2018") << '\n' | ||
| << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*) | ||
| << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*) | ||
| << align_center_with_border("[email protected]") << '\n' // NOLINT(*) | ||
| << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*) | ||
| << | ||
| "\n" | ||
| "Usage: Purpose:\n" | ||
| "\n" | ||
| " cbmc [-?] [-h] [--help] show help\n" | ||
| " cbmc file.c ... source file names\n" | ||
| "\n" | ||
| "Analysis options:\n" | ||
| 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(*) | ||
| " --trace give a counterexample trace for failed properties\n" //NOLINT(*) | ||
| "\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" | ||
| " --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_ANSI_C_LANGUAGE | ||
| HELP_FUNCTIONS | ||
| "\n" | ||
| "Program representations:\n" | ||
| " --show-parse-tree show parse tree\n" | ||
| " --show-symbol-table show loaded symbol table\n" | ||
| HELP_SHOW_GOTO_FUNCTIONS | ||
| "\n" | ||
| "Program instrumentation options:\n" | ||
| HELP_GOTO_CHECK | ||
| " --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 | ||
| HELP_REACHABILITY_SLICER_FB | ||
| " --full-slice run full slicer (experimental)\n" // NOLINT(*) | ||
| " --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" | ||
| "Backend 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(*) | ||
| " --localize-faults localize faults (experimental)\n" | ||
| " --smt2 use default SMT2 solver (Z3)\n" | ||
| " --boolector use Boolector\n" | ||
| " --cprover-smt2 use CPROVER SMT2 solver\n" | ||
| " --cvc4 use CVC4\n" | ||
| " --mathsat use MathSAT\n" | ||
| " --yices use Yices\n" | ||
| " --z3 use Z3\n" | ||
| " --refine use refinement procedure (experimental)\n" | ||
| HELP_STRING_REFINEMENT_CBMC | ||
| " --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" | ||
| " --xml-interface bi-directional XML interface\n" | ||
| " --json-ui use JSON-formatted output\n" | ||
| // NOLINTNEXTLINE(whitespace/line_length) | ||
| HELP_VALIDATE | ||
| HELP_GOTO_TRACE | ||
| HELP_FLUSH | ||
| " --verbosity # verbosity level\n" | ||
| HELP_TIMESTAMP | ||
| "\n"; | ||
| // clang-format on | ||
| switch(ui_message_handler.get_ui()) | ||
| { | ||
| case ui_message_handlert::uit::PLAIN: | ||
| // clang-format off | ||
| log.result() | ||
| << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n' | ||
| << align_center_with_border("Copyright (C) 2001-2018") << '\n' | ||
| << align_center_with_border("Daniel Kroening, Edmund Clarke") | ||
| << '\n' // NOLINT(*) | ||
| << align_center_with_border( | ||
| "Carnegie Mellon University, Computer Science Department") | ||
| << '\n' // NOLINT(*) | ||
| << align_center_with_border("[email protected]") << '\n' // NOLINT(*) | ||
| << align_center_with_border("Protected in part by U.S. patent 7,225,417") | ||
| << '\n' // NOLINT(*) | ||
| << | ||
| "\n" | ||
| "Usage: Purpose:\n" | ||
| "\n" | ||
| " cbmc [-?] [-h] [--help] show help\n" | ||
| " cbmc file.c ... source file names\n" | ||
| << cbmc_options.to_help_text(30, 80) << messaget::eom; | ||
| // clang-format on | ||
| break; | ||
| case ui_message_handlert::uit::JSON_UI: | ||
| ui_message_handler.get_json_stream().push_back(cbmc_options.to_json()); | ||
| break; | ||
| case ui_message_handlert::uit::XML_UI: | ||
| log.result() << cbmc_options.to_xml(); | ||
| break; | ||
| } | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected] | |
| #include <ansi-c/ansi_c_language.h> | ||
| #include <ansi-c/c_object_factory_parameters.h> | ||
|
|
||
| #include <util/cmdline_definition.h> | ||
| #include <util/parse_options.h> | ||
| #include <util/timestamper.h> | ||
| #include <util/ui_message.h> | ||
|
|
@@ -38,49 +39,45 @@ class goto_functionst; | |
| class optionst; | ||
|
|
||
| // clang-format off | ||
| #define CBMC_OPTIONS \ | ||
| OPT_BMC \ | ||
| "(preprocess)(slice-by-trace):" \ | ||
| OPT_FUNCTIONS \ | ||
| "(no-simplify)(full-slice)" \ | ||
| OPT_REACHABILITY_SLICER \ | ||
| "(debug-level):(no-propagation)(no-simplify-if)" \ | ||
| "(document-subgoals)(outfile):(test-preprocessor)" \ | ||
| "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ | ||
| "(object-bits):" \ | ||
| OPT_GOTO_CHECK \ | ||
| "(no-assertions)(no-assumptions)" \ | ||
| "(xml-ui)(xml-interface)(json-ui)" \ | ||
| "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ | ||
| "(cprover-smt2)" \ | ||
| "(no-sat-preprocessor)" \ | ||
| "(beautify)" \ | ||
| "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ | ||
| OPT_STRING_REFINEMENT_CBMC \ | ||
| "(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)" \ | ||
| "(property):(stop-on-fail)(trace)" \ | ||
| "(error-label):(verbosity):(no-library)" \ | ||
| "(nondet-static)" \ | ||
| "(version)" \ | ||
| "(cover):(symex-coverage-report):" \ | ||
| "(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_FLUSH \ | ||
| "(localize-faults)" \ | ||
| OPT_GOTO_TRACE \ | ||
| OPT_VALIDATE \ | ||
| OPT_ANSI_C_LANGUAGE \ | ||
| "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) | ||
| const cmdline_definitiont ui_options | ||
| { | ||
| { | ||
| "json-ui", | ||
| {}, | ||
| "use JSON-formatted output", | ||
| "Other options", | ||
| {} | ||
| }, | ||
| { | ||
| "xml-ui", | ||
| {}, | ||
| "use XML-formatted output", | ||
| "Other options", | ||
| {} | ||
| } | ||
| }; | ||
|
|
||
| const cmdline_definitiont cbmc_options( | ||
| ui_options | ||
| + cmdline_definitiont{ | ||
| { | ||
| "preprocess", | ||
| {}, | ||
| "stop after preprocessing. " | ||
| "This is a veeeeeeeeeeeeeeeeery long help text. " | ||
| "This is a veeeeeeeeeeeeeeeeery long help text.", | ||
| "C/C++ frontend options", | ||
| {} | ||
| }, | ||
| { | ||
| "slice-by-trace", | ||
| cmdline_optiont::argumentt{"f", "string"}, | ||
| "", | ||
| "", | ||
| cmdline_optiont::deprecatedt("-slice-by-trace has been removed") | ||
| } | ||
| } | ||
| + ui_options); | ||
| // clang-format on | ||
|
|
||
| class cbmc_parse_optionst: | ||
|
|
@@ -96,7 +93,7 @@ class cbmc_parse_optionst: | |
| cbmc_parse_optionst( | ||
| int argc, | ||
| const char **argv, | ||
| const std::string &extra_options); | ||
| const cmdline_definitiont &extra_options); | ||
|
|
||
| /// \brief Set the options that have default values | ||
| /// | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A rather unrelated comment: does anyone know why this ever needed to go in the header file? I.e., not just the changes in this PR, but also the current
CBMC_OPTIONS?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No idea :D