cprover
|
#include <janalyzer_parse_options.h>
Public Member Functions | |
virtual int | doit () override |
invoke main modules More... | |
virtual void | help () override |
display command line help More... | |
janalyzer_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 janalyzer_parse_options.h.
janalyzer_parse_optionst::janalyzer_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 59 of file janalyzer_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 265 of file janalyzer_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 324 of file janalyzer_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 71 of file janalyzer_parse_options.cpp.
References parse_options_baset::cmdline, config, CPROVER_EXIT_USAGE_ERROR, messaget::eom(), optionst::get_bool_option(), cmdlinet::get_value(), cmdlinet::get_values(), cmdlinet::isset(), configt::set(), optionst::set_option(), messaget::status(), and parse_options_baset::usage_error().
Referenced by doit().
|
inlineprotected |
Definition at line 176 of file janalyzer_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 722 of file janalyzer_parse_options.cpp.
References banner_string(), HELP_FUNCTIONS, HELP_GOTO_CHECK, HELP_SHOW_GOTO_FUNCTIONS, HELP_SHOW_PROPERTIES, HELP_TIMESTAMP, and JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP.
|
protectedvirtual |
Depending on the command line mode, run one of the analysis tasks.
Definition at line 427 of file janalyzer_parse_options.cpp.
References 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 659 of file janalyzer_parse_options.cpp.
References parse_options_baset::cmdline, goto_functionst::compute_loop_numbers(), messaget::eom(), messaget::error(), messaget::get_message_handler(), goto_check(), goto_modelt::goto_functions, goto_model, goto_partial_inline(), cmdlinet::isset(), remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_returns(), remove_vector(), remove_virtual_functions(), messaget::status(), ui_message_handler, and goto_functionst::update().
Referenced by doit().
|
protectedvirtual |
Definition at line 66 of file janalyzer_parse_options.cpp.
References new_java_bytecode_language(), and register_language().
Referenced by doit().
|
protected |
Definition at line 631 of file janalyzer_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 163 of file janalyzer_parse_options.h.
Referenced by build_analyzer(), doit(), perform_analysis(), process_goto_program(), and set_properties().
|
protected |
Definition at line 162 of file janalyzer_parse_options.h.
Referenced by doit(), get_ui(), and process_goto_program().