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 () |
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 () |
virtual int | perform_analysis (const optionst &options) |
Depending on the command line mode, run one of the analysis tasks. More... | |
ai_baset * | build_analyzer (const optionst &, const namespacet &ns) |
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of options. More... | |
ui_message_handlert::uit | get_ui () |
Protected Attributes | |
ui_message_handlert | ui_message_handler |
goto_modelt | goto_model |
Additional Inherited Members | |
![]() | |
cmdlinet | cmdline |
Definition at line 153 of file goto_analyzer_parse_options.h.
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 65 of file goto_analyzer_parse_options.cpp.
|
protected |
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of options.
However at the moment some domains require the goto_model
Definition at line 298 of file goto_analyzer_parse_options.cpp.
References optionst::get_bool_option(), goto_modelt::goto_functions, and goto_model.
Referenced by perform_analysis().
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 357 of file goto_analyzer_parse_options.cpp.
References parse_options_baset::cmdline, config, CPROVER_EXIT_EXCEPTION, CPROVER_EXIT_INTERNAL_ERROR, CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY, CPROVER_EXIT_SUCCESS, messaget::eom(), messaget::error(), messaget::eval_verbosity(), get_command_line_options(), messaget::get_message_handler(), get_ui(), cmdlinet::get_value(), goto_model, initialize_goto_model(), cmdlinet::isset(), messaget::M_STATISTICS, perform_analysis(), process_goto_program(), register_languages(), show_goto_functions(), show_symbol_table(), messaget::status(), goto_modelt::symbol_table, configt::this_architecture(), configt::this_operating_system(), and ui_message_handler.
|
protectedvirtual |
Definition at line 81 of file goto_analyzer_parse_options.cpp.
References configt::ansi_c, parse_options_baset::cmdline, config, configt::cpp, CPROVER_EXIT_USAGE_ERROR, messaget::eom(), optionst::get_bool_option(), cmdlinet::get_value(), 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(), messaget::status(), and parse_options_baset::usage_error().
Referenced by doit().
|
inlineprotected |
Definition at line 178 of file goto_analyzer_parse_options.h.
References ui_message_handlert::get_ui(), and ui_message_handler.
Referenced by doit(), and perform_analysis().
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 790 of file goto_analyzer_parse_options.cpp.
References banner_string(), configt::ansi_ct::C11, configt::ansi_ct::C89, configt::ansi_ct::C99, configt::cppt::CPP03, configt::cppt::CPP11, configt::cppt::CPP98, configt::ansi_ct::default_c_standard(), configt::cppt::default_cpp_standard(), HELP_FLUSH, HELP_FUNCTIONS, HELP_GOTO_CHECK, HELP_SHOW_GOTO_FUNCTIONS, HELP_SHOW_PROPERTIES, HELP_TIMESTAMP, configt::this_architecture(), and configt::this_operating_system().
|
protectedvirtual |
Depending on the command line mode, run one of the analysis tasks.
Definition at line 462 of file goto_analyzer_parse_options.cpp.
References adjust_float_expressions(), build_analyzer(), parse_options_baset::cmdline, CPROVER_EXIT_INTERNAL_ERROR, CPROVER_EXIT_SET_PROPERTIES_FAILED, CPROVER_EXIT_SUCCESS, CPROVER_EXIT_USAGE_ERROR, CPROVER_EXIT_VERIFICATION_SAFE, CPROVER_EXIT_VERIFICATION_UNSAFE, messaget::eom(), messaget::error(), forall_goto_functions, optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), get_ui(), cmdlinet::get_value(), goto_modelt::goto_functions, goto_model, cmdlinet::isset(), label_properties(), local_may_aliast::output(), reachable_functions(), messaget::result(), set_properties(), show_properties(), static_reachable_functions(), static_show_domain(), static_simplifier(), static_unreachable_functions(), static_unreachable_instructions(), static_verifier(), messaget::status(), goto_modelt::symbol_table, taint_analysis(), unreachable_functions(), and unreachable_instructions().
Referenced by doit().
|
protectedvirtual |
Definition at line 719 of file goto_analyzer_parse_options.cpp.
References configt::ansi_c, configt::ansi_ct::arch, parse_options_baset::cmdline, goto_functionst::compute_loop_numbers(), config, cprover_c_library_factory(), cprover_cpp_library_factory(), messaget::eom(), messaget::error(), messaget::get_message_handler(), goto_check(), goto_modelt::goto_functions, goto_model, goto_partial_inline(), cmdlinet::isset(), link_to_library(), remove_asm(), remove_complex(), remove_function_pointers(), remove_returns(), remove_vector(), messaget::status(), ui_message_handler, and goto_functionst::update().
Referenced by doit().
|
protectedvirtual |
Definition at line 74 of file goto_analyzer_parse_options.cpp.
References new_ansi_c_language(), new_cpp_language(), new_jsil_language(), and register_language().
Referenced by doit().
|
protected |
Definition at line 691 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 perform_analysis().
|
protected |
Definition at line 165 of file goto_analyzer_parse_options.h.
Referenced by build_analyzer(), doit(), perform_analysis(), process_goto_program(), and set_properties().
|
protected |
Definition at line 164 of file goto_analyzer_parse_options.h.
Referenced by doit(), get_ui(), and process_goto_program().