cprover
|
#include <cbmc_parse_options.h>
Public Member Functions | |
virtual int | doit () override |
invoke main modules More... | |
virtual void | help () override |
display command line help More... | |
cbmc_parse_optionst (int argc, const char **argv) | |
cbmc_parse_optionst (int argc, const char **argv, const std::string &extra_options) | |
![]() | |
parse_options_baset (const std::string &optstring, int argc, const char **argv) | |
virtual void | usage_error () |
virtual int | main () |
virtual | ~parse_options_baset () |
![]() | |
xml_interfacet (cmdlinet &_cmdline) | |
Static Public Member Functions | |
static void | set_default_options (optionst &) |
Set the options that have default values. More... | |
static bool | process_goto_program (goto_modelt &, const optionst &, messaget &) |
static int | get_goto_program (goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &) |
Protected Member Functions | |
void | register_languages () |
void | get_command_line_options (optionst &) |
void | preprocessing () |
bool | set_properties () |
![]() | |
void | get_xml_options (cmdlinet &cmdline) |
XML User Interface. More... | |
void | get_xml_options (const class xmlt &xml, cmdlinet &cmdline) |
Protected Attributes | |
goto_modelt | goto_model |
ui_message_handlert | ui_message_handler |
const path_strategy_choosert | path_strategy_chooser |
Additional Inherited Members | |
![]() | |
cmdlinet | cmdline |
Definition at line 79 of file cbmc_parse_options.h.
cbmc_parse_optionst::cbmc_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 68 of file cbmc_parse_options.cpp.
cbmc_parse_optionst::cbmc_parse_optionst | ( | int | argc, |
const char ** | argv, | ||
const std::string & | extra_options | ||
) |
Definition at line 77 of file cbmc_parse_options.cpp.
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 400 of file cbmc_parse_options.cpp.
References cmdlinet::args, CBMC_VERSION, parse_options_baset::cmdline, config, CPROVER_EXIT_EXCEPTION, CPROVER_EXIT_INCORRECT_TASK, CPROVER_EXIT_PREPROCESSOR_TEST_FAILED, CPROVER_EXIT_SET_PROPERTIES_FAILED, CPROVER_EXIT_SUCCESS, CPROVER_EXIT_USAGE_ERROR, bmct::do_language_agnostic_bmc(), messaget::eom(), messaget::error(), messaget::eval_verbosity(), get_command_line_options(), get_goto_program(), get_language_from_filename(), languaget::get_language_options(), messaget::get_message_handler(), ui_message_handlert::get_ui(), cmdlinet::get_value(), goto_model, is_goto_binary(), cmdlinet::isset(), messaget::M_STATISTICS, languaget::parse(), path_strategy_chooser, preprocessing(), register_languages(), messaget::set_message_handler(), set_properties(), languaget::show_parse(), show_properties(), messaget::status(), test_c_preprocessor(), configt::this_architecture(), configt::this_operating_system(), ui_message_handler, and widen().
|
protected |
Definition at line 105 of file cbmc_parse_options.cpp.
References configt::ansi_c, parse_options_baset::cmdline, config, configt::cpp, CPROVER_EXIT_SUCCESS, CPROVER_EXIT_USAGE_ERROR, messaget::eom(), messaget::error(), cmdlinet::get_value(), cmdlinet::get_values(), cmdlinet::isset(), parse_cover_options(), PARSE_OPTIONS_GOTO_CHECK, PARSE_OPTIONS_GOTO_TRACE, path_strategy_chooser, configt::set(), configt::ansi_ct::set_c11(), configt::ansi_ct::set_c89(), configt::ansi_ct::set_c99(), configt::cppt::set_cpp03(), configt::cppt::set_cpp11(), configt::cppt::set_cpp98(), set_default_options(), optionst::set_option(), path_strategy_choosert::set_path_strategy_options(), path_strategy_choosert::show_strategies(), and parse_options_baset::usage_error().
Referenced by doit().
|
static |
Definition at line 571 of file cbmc_parse_options.cpp.
References cmdlinet::args, parse_options_baset::cmdline, config, CPROVER_EXIT_EXCEPTION, CPROVER_EXIT_INCORRECT_TASK, CPROVER_EXIT_INTERNAL_ERROR, CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY, CPROVER_EXIT_SUCCESS, messaget::eom(), messaget::error(), ui_message_handlert::get_ui(), goto_model, initialize_goto_model(), cmdlinet::isset(), configt::object_bits_info(), process_goto_program(), show_goto_functions(), show_loop_ids(), show_symbol_table(), messaget::status(), and ui_message_handler.
Referenced by doit().
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 866 of file cbmc_parse_options.cpp.
References banner_string(), configt::ansi_ct::C11, configt::ansi_ct::C89, configt::ansi_ct::C99, CBMC_VERSION, configt::cppt::CPP03, configt::cppt::CPP11, configt::cppt::CPP98, configt::ansi_ct::default_c_standard(), configt::cppt::default_cpp_standard(), HELP_BMC, HELP_FLUSH, HELP_FUNCTIONS, HELP_GOTO_CHECK, HELP_GOTO_TRACE, HELP_REACHABILITY_SLICER, HELP_SHOW_GOTO_FUNCTIONS, HELP_SHOW_PROPERTIES, HELP_TIMESTAMP, configt::this_architecture(), and configt::this_operating_system().
|
protected |
Definition at line 647 of file cbmc_parse_options.cpp.
References cmdlinet::args, parse_options_baset::cmdline, CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY, messaget::eom(), messaget::error(), get_language_from_filename(), languaget::get_language_options(), messaget::get_message_handler(), languaget::preprocess(), and messaget::set_message_handler().
Referenced by doit().
|
static |
Definition at line 704 of file cbmc_parse_options.cpp.
References add_failed_symbols(), adjust_float_expressions(), configt::ansi_c, configt::ansi_ct::arch, goto_functionst::compute_loop_numbers(), config, cprover_c_library_factory(), cprover_cpp_library_factory(), CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY, messaget::eom(), messaget::error(), full_slicer(), optionst::get_bool_option(), optionst::get_list_option(), messaget::get_message_handler(), goto_check(), goto_modelt::goto_functions, goto_model, instrument_cover_goals(), instrument_preconditions(), optionst::is_set(), label_properties(), link_to_library(), mm_io(), nondet_static(), property_slicer(), reachability_slicer(), remove_asm(), remove_complex(), remove_function_pointers(), remove_returns(), remove_skip(), remove_unused_functions(), remove_vector(), rewrite_union(), messaget::status(), string_abstraction(), string_instrumentation(), goto_modelt::symbol_table, and goto_functionst::update().
Referenced by get_goto_program().
|
protected |
Definition at line 23 of file cbmc_languages.cpp.
References new_ansi_c_language(), new_cpp_language(), new_jsil_language(), and register_language().
Referenced by doit().
|
static |
Set the options that have default values.
This function can be called from clients that wish to emulate CBMC's default behaviour, for example unit tests.
Definition at line 89 of file cbmc_parse_options.cpp.
References optionst::set_option().
Referenced by get_command_line_options().
|
protected |
Definition at line 539 of file cbmc_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), messaget::error(), cmdlinet::get_values(), goto_model, and cmdlinet::isset().
Referenced by doit().
|
protected |
Definition at line 110 of file cbmc_parse_options.h.
Referenced by doit(), get_goto_program(), process_goto_program(), and set_properties().
|
protected |
Definition at line 112 of file cbmc_parse_options.h.
Referenced by doit(), and get_command_line_options().
|
protected |
Definition at line 111 of file cbmc_parse_options.h.
Referenced by doit(), and get_goto_program().