cprover
|
#include <clobber_parse_options.h>
Public Member Functions | |
virtual int | doit () |
invoke main modules More... | |
virtual void | help () |
display command line help More... | |
clobber_parse_optionst (int argc, const char **argv) | |
clobber_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 () |
![]() | |
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 | |
void | get_command_line_options (optionst &options) |
bool | get_goto_program (const optionst &options, goto_functionst &goto_functions) |
bool | process_goto_program (const optionst &options, goto_functionst &goto_functions) |
bool | set_properties (goto_functionst &goto_functions) |
void | report_success () |
void | report_failure () |
void | show_counterexample (const class goto_tracet &) |
void | eval_verbosity () |
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 37 of file clobber_parse_options.h.
clobber_parse_optionst::clobber_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 44 of file clobber_parse_options.cpp.
clobber_parse_optionst::clobber_parse_optionst | ( | int | argc, |
const char ** | argv, | ||
const std::string & | extra_options | ||
) |
|
virtual |
invoke main modules
Implements parse_options_baset.
Definition at line 103 of file clobber_parse_options.cpp.
References CBMC_VERSION, parse_options_baset::cmdline, messaget::debug(), dump_c(), messaget::endl(), messaget::eom(), messaget::error(), eval_verbosity(), get_command_line_options(), get_goto_program(), language_uit::get_ui(), cmdlinet::isset(), label_properties(), memory_info(), new_ansi_c_language(), new_cpp_language(), register_language(), set_properties(), show_properties(), messaget::status(), and language_uit::symbol_table.
|
protected |
Definition at line 51 of file clobber_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_string2int().
Referenced by doit().
|
protected |
Definition at line 68 of file clobber_parse_options.cpp.
References parse_options_baset::cmdline, config, cmdlinet::get_value(), cmdlinet::isset(), PARSE_OPTIONS_GOTO_CHECK, configt::set(), optionst::set_option(), and parse_options_baset::usage_error().
Referenced by doit().
|
protected |
Definition at line 192 of file clobber_parse_options.cpp.
References cmdlinet::args, language_uit::clear_parse(), parse_options_baset::cmdline, config, goto_functions_templatet< bodyT >::entry_point(), messaget::eom(), messaget::error(), get_language_from_filename(), messaget::get_message_handler(), goto_convert(), is_goto_binary(), cmdlinet::isset(), link_to_library(), language_uit::parse(), languaget::parse(), process_goto_program(), read_goto_binary(), configt::set_from_symbol_table(), messaget::set_message_handler(), languaget::show_parse(), language_uit::show_symbol_table(), messaget::status(), language_uit::symbol_table, symbol_tablet::symbols, language_uit::typecheck(), ui_message_handler, and widen().
Referenced by doit().
|
virtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 490 of file clobber_parse_options.cpp.
References CBMC_VERSION, HELP_GOTO_CHECK, HELP_SHOW_GOTO_FUNCTIONS, configt::this_architecture(), and configt::this_operating_system().
|
protected |
Definition at line 314 of file clobber_parse_options.cpp.
References parse_options_baset::cmdline, goto_functions_templatet< bodyT >::compute_loop_numbers(), messaget::eom(), language_uit::get_ui(), goto_check(), goto_partial_inline(), cmdlinet::isset(), make_assertions_false(), show_goto_functions(), show_loop_ids(), messaget::status(), language_uit::symbol_table, ui_message_handler, and goto_functions_templatet< bodyT >::update().
Referenced by get_goto_program().
|
protected |
Definition at line 466 of file clobber_parse_options.cpp.
References xmlt::data, messaget::eom(), language_uit::get_ui(), ui_message_handlert::PLAIN, messaget::result(), xml(), and ui_message_handlert::XML_UI.
|
protected |
Definition at line 418 of file clobber_parse_options.cpp.
References xmlt::data, messaget::eom(), language_uit::get_ui(), ui_message_handlert::PLAIN, messaget::result(), xml(), and ui_message_handlert::XML_UI.
|
protected |
Definition at line 184 of file clobber_parse_options.cpp.
References parse_options_baset::cmdline, cmdlinet::get_values(), and cmdlinet::isset().
Referenced by doit().
|
protected |
Definition at line 441 of file clobber_parse_options.cpp.
References convert(), language_uit::get_ui(), ui_message_handlert::PLAIN, show_goto_trace(), language_uit::symbol_table, xml(), and ui_message_handlert::XML_UI.
|
protected |
Definition at line 52 of file clobber_parse_options.h.
Referenced by eval_verbosity(), get_goto_program(), and process_goto_program().