cprover
|
#include <symex_parse_options.h>
Public Member Functions | |
virtual int | doit () |
invoke main modules More... | |
virtual void | help () |
display command line help More... | |
symex_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 | |
void | get_command_line_options (optionst &options) |
bool | process_goto_program (const optionst &options) |
bool | set_properties () |
void | report_success () |
void | report_failure () |
void | report_properties (const path_searcht::property_mapt &) |
void | report_cover (const path_searcht::property_mapt &) |
void | show_counterexample (const class goto_tracet &) |
void | eval_verbosity () |
std::string | get_test (const goto_tracet &goto_trace) |
Protected Attributes | |
ui_message_handlert | ui_message_handler |
goto_modelt | goto_model |
![]() | |
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 53 of file symex_parse_options.h.
symex_parse_optionst::symex_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 59 of file symex_parse_options.cpp.
|
virtual |
invoke main modules
Implements parse_options_baset.
Definition at line 118 of file symex_parse_options.cpp.
References locst::build(), CBMC_VERSION, parse_options_baset::cmdline, messaget::debug(), path_searcht::eager_infeasibility, messaget::endl(), messaget::eom(), messaget::error(), eval_verbosity(), 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(), memory_info(), new_ansi_c_language(), new_cpp_language(), new_java_bytecode_language(), locst::output(), process_goto_program(), path_searcht::property_map, register_language(), report_cover(), report_failure(), report_properties(), report_success(), safety_checkert::SAFE, safe_string2unsigned(), path_searcht::set_bfs(), path_searcht::set_branch_bound(), path_searcht::set_context_bound(), path_searcht::set_depth_limit(), path_searcht::set_dfs(), path_searcht::set_locs(), messaget::set_message_handler(), set_properties(), path_searcht::set_time_limit(), path_searcht::set_unwind_limit(), show_properties(), path_searcht::show_vcc, goto_modelt::symbol_table, safety_checkert::UNSAFE, and unsafe_string2unsigned().
|
protected |
Definition at line 66 of file symex_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 83 of file symex_parse_options.cpp.
References parse_options_baset::cmdline, config, cmdlinet::get_value(), cmdlinet::get_values(), cmdlinet::isset(), PARSE_OPTIONS_GOTO_CHECK, configt::set(), optionst::set_option(), and parse_options_baset::usage_error().
Referenced by doit().
|
protected |
Definition at line 22 of file symex_cover.cpp.
References from_expr(), goto_model, id2string(), goto_tracet::steps, and goto_modelt::symbol_table.
Referenced by report_cover().
|
virtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 549 of file symex_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 290 of file symex_parse_options.cpp.
References adjust_float_expressions(), ASSERTION, BRANCH, parse_options_baset::cmdline, goto_functions_templatet< bodyT >::compute_loop_numbers(), CONDITION, COVER, DECISION, messaget::eom(), messaget::error(), messaget::get_message_handler(), language_uit::get_ui(), cmdlinet::get_value(), goto_check(), goto_modelt::goto_functions, goto_model, goto_partial_inline(), instrument_cover_goals(), cmdlinet::isset(), link_to_library(), LOCATION, MCDC, PATH, remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_unused_functions(), remove_vector(), remove_virtual_functions(), rewrite_union(), show_goto_functions(), show_loop_ids(), messaget::status(), language_uit::symbol_table, ui_message_handler, and goto_functions_templatet< bodyT >::update().
Referenced by doit().
|
protected |
Definition at line 46 of file symex_cover.cpp.
References parse_options_baset::cmdline, convert(), messaget::eom(), get_test(), language_uit::get_ui(), goto_model, id2string(), cmdlinet::isset(), json(), ui_message_handlert::JSON_UI, jsont::make_array(), jsont::make_object(), xmlt::new_element(), ui_message_handlert::PLAIN, json_arrayt::push_back(), messaget::result(), xmlt::set_attribute(), messaget::mstreamt::source_location, messaget::status(), goto_modelt::symbol_table, xml(), and ui_message_handlert::XML_UI.
Referenced by doit().
|
protected |
Definition at line 525 of file symex_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.
Referenced by doit().
|
protected |
Definition at line 410 of file symex_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), path_searcht::FAILURE, language_uit::get_ui(), id2string(), cmdlinet::isset(), path_searcht::NOT_REACHED, ui_message_handlert::PLAIN, xmlt::set_attribute(), show_counterexample(), messaget::status(), path_searcht::SUCCESS, and ui_message_handlert::XML_UI.
Referenced by doit().
|
protected |
Definition at line 477 of file symex_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.
Referenced by doit().
|
protected |
Definition at line 261 of file symex_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), messaget::error(), cmdlinet::get_values(), goto_modelt::goto_functions, goto_model, and cmdlinet::isset().
Referenced by doit().
|
protected |
Definition at line 500 of file symex_parse_options.cpp.
References convert(), language_uit::get_ui(), goto_model, ui_message_handlert::PLAIN, show_goto_trace(), goto_modelt::symbol_table, xml(), and ui_message_handlert::XML_UI.
Referenced by report_properties().
|
protected |
Definition at line 65 of file symex_parse_options.h.
Referenced by doit(), get_test(), process_goto_program(), report_cover(), set_properties(), and show_counterexample().
|
protected |
Definition at line 64 of file symex_parse_options.h.
Referenced by eval_verbosity(), and process_goto_program().