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) | |
![]() | |
language_uit (const cmdlinet &cmdline, ui_message_handlert &ui_message_handler) | |
Constructor. More... | |
virtual | ~language_uit () |
Destructor. More... | |
virtual bool | parse () |
virtual bool | parse (const std::string &filename) |
virtual bool | typecheck () |
virtual bool | final () |
virtual void | clear_parse () |
virtual void | show_symbol_table (bool brief=false) |
virtual void | show_symbol_table_plain (std::ostream &out, bool brief) |
virtual void | show_symbol_table_xml_ui (bool brief) |
uit | get_ui () |
Protected Member Functions | |
virtual void | register_languages () |
virtual void | get_command_line_options (optionst &options) |
virtual int | do_bmc (bmct &bmc, const goto_functionst &goto_functions) |
invoke main modules More... | |
virtual int | get_goto_program (const optionst &options, expr_listt &bmc_constraints, goto_functionst &goto_functions) |
virtual bool | process_goto_program (const optionst &options, goto_functionst &goto_functions) |
bool | set_properties (goto_functionst &goto_functions) |
void | eval_verbosity () |
virtual int | get_modules (expr_listt &bmc_constraints) |
void | preprocessing () |
![]() | |
void | get_xml_options (cmdlinet &cmdline) |
XML User Interface. More... | |
void | get_xml_options (const class xmlt &xml, cmdlinet &cmdline) |
Protected Attributes | |
ui_message_handlert | ui_message_handler |
![]() | |
const cmdlinet & | _cmdline |
ui_message_handlert & | ui_message_handler |
Additional Inherited Members | |
![]() | |
typedef ui_message_handlert::uit | uit |
![]() | |
cmdlinet | cmdline |
![]() | |
language_filest | language_files |
symbol_tablet | symbol_table |
Definition at line 68 of file cbmc_parse_options.h.
cbmc_parse_optionst::cbmc_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 67 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 75 of file cbmc_parse_options.cpp.
|
protectedvirtual |
invoke main modules
Definition at line 902 of file cbmc_parse_options.cpp.
References messaget::debug(), messaget::endl(), messaget::eom(), safety_checkert::ERROR, language_uit::get_ui(), memory_info(), messaget::result(), bmct::run(), safety_checkert::SAFE, bmct::set_ui(), and safety_checkert::UNSAFE.
Referenced by doit().
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 404 of file cbmc_parse_options.cpp.
References CBMC_VERSION, parse_options_baset::cmdline, config, do_bmc(), messaget::eom(), messaget::error(), eval_verbosity(), optionst::get_bool_option(), get_command_line_options(), get_goto_program(), cbmc_solverst::get_solver(), language_uit::get_ui(), cmdlinet::isset(), preprocessing(), cbmc_solverst::solvert::prop_conv(), register_languages(), remove_static_init_loops(), set_properties(), cbmc_solverst::set_ui(), show_properties(), messaget::status(), language_uit::symbol_table, test_c_preprocessor(), configt::this_architecture(), configt::this_operating_system(), and ui_message_handler.
|
protected |
Definition at line 86 of file cbmc_parse_options.cpp.
References parse_options_baset::cmdline, cmdlinet::get_value(), cmdlinet::isset(), messaget::M_STATISTICS, message_handlert::set_verbosity(), ui_message_handler, and unsafe_string2unsigned().
Referenced by doit().
|
protectedvirtual |
Definition at line 101 of file cbmc_parse_options.cpp.
References configt::ansi_c, parse_options_baset::cmdline, config, configt::cpp, messaget::eom(), messaget::error(), optionst::get_bool_option(), cmdlinet::get_value(), cmdlinet::get_values(), cmdlinet::isset(), PARSE_OPTIONS_GOTO_CHECK, 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(), optionst::set_option(), and parse_options_baset::usage_error().
Referenced by doit().
|
protectedvirtual |
Definition at line 533 of file cbmc_parse_options.cpp.
References cmdlinet::args, language_uit::clear_parse(), parse_options_baset::cmdline, config, messaget::eom(), messaget::error(), get_language_from_filename(), messaget::get_message_handler(), get_modules(), language_uit::get_ui(), goto_convert(), is_goto_binary(), cmdlinet::isset(), language_uit::parse(), languaget::parse(), process_goto_program(), read_object_and_link(), configt::set_from_symbol_table(), messaget::set_message_handler(), show_goto_functions(), show_loop_ids(), languaget::show_parse(), language_uit::show_symbol_table(), messaget::status(), language_uit::symbol_table, language_uit::typecheck(), ui_message_handler, and widen().
Referenced by doit().
|
inlineprotectedvirtual |
Definition at line 107 of file cbmc_parse_options.h.
References preprocessing().
Referenced by get_goto_program().
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 933 of file cbmc_parse_options.cpp.
References 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_GOTO_CHECK, HELP_SHOW_GOTO_FUNCTIONS, configt::this_architecture(), and configt::this_operating_system().
|
protected |
Definition at line 699 of file cbmc_parse_options.cpp.
References cmdlinet::args, parse_options_baset::cmdline, messaget::eom(), messaget::error(), get_language_from_filename(), messaget::get_message_handler(), languaget::preprocess(), and messaget::set_message_handler().
Referenced by doit(), and get_modules().
|
protectedvirtual |
Definition at line 755 of file cbmc_parse_options.cpp.
References add_failed_symbols(), adjust_float_expressions(), parse_options_baset::cmdline, goto_functions_templatet< bodyT >::compute_loop_numbers(), messaget::eom(), messaget::error(), full_slicer(), messaget::get_message_handler(), cmdlinet::get_values(), goto_check(), goto_partial_inline(), instrument_cover_goals(), cmdlinet::isset(), label_properties(), link_to_library(), mm_io(), nondet_static(), property_slicer(), remove_asm(), remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_returns(), remove_skip(), remove_unused_functions(), remove_vector(), remove_virtual_functions(), rewrite_union(), messaget::status(), string_abstraction(), string_instrumentation(), language_uit::symbol_table, ui_message_handler, and goto_functions_templatet< bodyT >::update().
Referenced by get_goto_program().
|
protectedvirtual |
Definition at line 24 of file cbmc_languages.cpp.
References new_ansi_c_language(), new_cpp_language(), new_java_bytecode_language(), new_jsil_language(), and register_language().
Referenced by doit().
|
protected |
Definition at line 502 of file cbmc_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), messaget::error(), cmdlinet::get_values(), and cmdlinet::isset().
Referenced by doit().
|
protected |
Definition at line 84 of file cbmc_parse_options.h.
Referenced by doit(), eval_verbosity(), get_goto_program(), and process_goto_program().