cprover
|
#include <goto_analyzer_parse_options.h>
Public Member Functions | |
virtual int | doit () override |
invoke main modules More... | |
virtual void | help () override |
display command line help More... | |
goto_analyzer_parse_optionst (int argc, const char **argv) | |
![]() | |
parse_options_baset (const std::string &optstring, int argc, const char **argv) | |
virtual void | usage_error () |
virtual int | main () |
virtual | ~parse_options_baset () |
![]() | |
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 bool | process_goto_program (const optionst &options) |
bool | set_properties () |
void | eval_verbosity () |
Protected Attributes | |
ui_message_handlert | ui_message_handler |
goto_modelt | goto_model |
bool | has_entry_point |
![]() | |
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 50 of file goto_analyzer_parse_options.h.
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 57 of file goto_analyzer_parse_options.cpp.
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 137 of file goto_analyzer_parse_options.cpp.
References CBMC_VERSION, parse_options_baset::cmdline, config, messaget::eom(), messaget::error(), eval_verbosity(), forall_goto_functions, get_command_line_options(), messaget::get_message_handler(), language_uit::get_ui(), cmdlinet::get_value(), goto_modelt::goto_functions, goto_model, initialize_goto_model(), cmdlinet::isset(), label_properties(), local_may_aliast::output(), process_goto_program(), reachable_functions(), register_languages(), messaget::result(), optionst::set_option(), set_properties(), show_intervals(), show_properties(), static_analyzer(), messaget::status(), goto_modelt::symbol_table, taint_analysis(), configt::this_architecture(), configt::this_operating_system(), unreachable_functions(), and unreachable_instructions().
|
protected |
Definition at line 74 of file goto_analyzer_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 89 of file goto_analyzer_parse_options.cpp.
References configt::ansi_c, parse_options_baset::cmdline, config, configt::cpp, cmdlinet::get_values(), cmdlinet::isset(), 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().
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 426 of file goto_analyzer_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().
|
protectedvirtual |
Definition at line 338 of file goto_analyzer_parse_options.cpp.
References parse_options_baset::cmdline, goto_functions_templatet< bodyT >::compute_loop_numbers(), messaget::eom(), messaget::error(), messaget::get_message_handler(), language_uit::get_ui(), goto_check(), goto_modelt::goto_functions, goto_model, goto_partial_inline(), cmdlinet::isset(), link_to_library(), remove_asm(), remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_returns(), remove_vector(), remove_virtual_functions(), show_goto_functions(), language_uit::show_symbol_table(), messaget::status(), ui_message_handler, and goto_functions_templatet< bodyT >::update().
Referenced by doit().
|
protectedvirtual |
Definition at line 66 of file goto_analyzer_parse_options.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 310 of file goto_analyzer_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 62 of file goto_analyzer_parse_options.h.
Referenced by doit(), process_goto_program(), and set_properties().
|
protected |
Definition at line 73 of file goto_analyzer_parse_options.h.
|
protected |
Definition at line 61 of file goto_analyzer_parse_options.h.
Referenced by eval_verbosity(), and process_goto_program().