cprover
|
#include <jbmc_parse_options.h>
Public Member Functions | |
virtual int | doit () override |
invoke main modules More... | |
virtual void | help () override |
display command line help More... | |
jbmc_parse_optionst (int argc, const char **argv) | |
jbmc_parse_optionst (int argc, const char **argv, const std::string &extra_options) | |
void | process_goto_function (goto_model_functiont &function, const abstract_goto_modelt &, const optionst &) |
bool | process_goto_functions (goto_modelt &goto_model, const optionst &options) |
bool | can_generate_function_body (const irep_idt &name) |
bool | generate_function_body (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) |
![]() | |
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 | |
void | get_command_line_options (optionst &) |
int | get_goto_program (std::unique_ptr< goto_modelt > &goto_model, const optionst &) |
bool | show_loaded_functions (const abstract_goto_modelt &goto_model) |
bool | set_properties (goto_modelt &goto_model) |
Protected Attributes | |
ui_message_handlert | ui_message_handler |
std::unique_ptr< cover_configt > | cover_config |
path_strategy_choosert | path_strategy_chooser |
object_factory_parameterst | object_factory_params |
bool | stub_objects_are_not_null |
Additional Inherited Members | |
![]() | |
cmdlinet | cmdline |
Definition at line 87 of file jbmc_parse_options.h.
jbmc_parse_optionst::jbmc_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 63 of file jbmc_parse_options.cpp.
jbmc_parse_optionst::jbmc_parse_optionst | ( | int | argc, |
const char ** | argv, | ||
const std::string & | extra_options | ||
) |
Definition at line 71 of file jbmc_parse_options.cpp.
bool jbmc_parse_optionst::can_generate_function_body | ( | const irep_idt & | name | ) |
Definition at line 1025 of file jbmc_parse_options.cpp.
References goto_functionst::entry_point(), and INITIALIZE_FUNCTION.
Referenced by generate_function_body().
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 411 of file jbmc_parse_options.cpp.
References add_failed_symbols(), bmct::add_loop_unwind_handler(), cmdlinet::args, parse_options_baset::cmdline, config, cover_config, bmct::do_language_agnostic_bmc(), goto_functionst::entry_point(), messaget::eom(), messaget::error(), messaget::eval_verbosity(), lazy_goto_modelt::from_handler_object(), optionst::get_bool_option(), get_command_line_options(), get_cover_config(), get_goto_program(), get_language_from_filename(), languaget::get_language_options(), messaget::get_message_handler(), ui_message_handlert::get_ui(), cmdlinet::get_value(), symbol_table_baset::has_symbol(), lazy_goto_modelt::initialize(), cmdlinet::isset(), java_enum_static_init_unwind_handler(), messaget::M_STATISTICS, object_factory_parameterst::max_nondet_array_length, MAX_NONDET_ARRAY_LENGTH_DEFAULT, MAX_NONDET_STRING_LENGTH, object_factory_parameterst::max_nondet_string_length, MAX_NONDET_TREE_DEPTH, object_factory_parameterst::max_nondet_tree_depth, new_ansi_c_language(), new_java_bytecode_language(), object_factory_params, languaget::parse(), path_strategy_chooser, register_language(), messaget::set_message_handler(), set_properties(), show_loaded_functions(), languaget::show_parse(), show_properties(), messaget::status(), stub_objects_are_not_null, lazy_goto_modelt::symbol_table, configt::this_architecture(), configt::this_operating_system(), ui_message_handler, and widen().
bool jbmc_parse_optionst::generate_function_body | ( | const irep_idt & | function_name, |
symbol_table_baset & | symbol_table, | ||
goto_functiont & | function, | ||
bool | body_available | ||
) |
Definition at line 1032 of file jbmc_parse_options.cpp.
References can_generate_function_body(), goto_convert_functionst::convert_function(), messaget::get_message_handler(), java_generate_simple_method_stub(), symbol_table_baset::lookup_ref(), symbolt::mode, object_factory_params, and stub_objects_are_not_null.
|
protected |
Definition at line 82 of file jbmc_parse_options.cpp.
References parse_options_baset::cmdline, config, CPROVER_EXIT_SUCCESS, messaget::eom(), messaget::error(), optionst::get_bool_option(), cmdlinet::get_value(), cmdlinet::get_values(), INVARIANT, cmdlinet::isset(), parse_cover_options(), PARSE_OPTIONS_GOTO_CHECK, PARSE_OPTIONS_GOTO_TRACE, path_strategy_chooser, configt::set(), optionst::set_option(), path_strategy_choosert::set_path_strategy_options(), path_strategy_choosert::show_strategies(), and parse_options_baset::usage_error().
Referenced by doit().
|
protected |
Definition at line 643 of file jbmc_parse_options.cpp.
References add_failed_symbols(), cmdlinet::args, parse_options_baset::cmdline, config, CPROVER_EXIT_SUCCESS, messaget::eom(), messaget::error(), lazy_goto_modelt::from_handler_object(), messaget::get_message_handler(), ui_message_handlert::get_ui(), lazy_goto_modelt::initialize(), cmdlinet::isset(), lazy_goto_modelt::load_all_functions(), configt::object_bits_info(), lazy_goto_modelt::process_whole_model_and_freeze(), show_class_hierarchy(), show_goto_functions(), show_loop_ids(), show_symbol_table(), messaget::status(), lazy_goto_modelt::symbol_table, and ui_message_handler.
Referenced by doit().
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 1068 of file jbmc_parse_options.cpp.
References banner_string(), HELP_BMC, HELP_FLUSH, HELP_FUNCTIONS, HELP_GOTO_CHECK, HELP_GOTO_TRACE, HELP_REACHABILITY_SLICER, HELP_SHOW_CLASS_HIERARCHY, HELP_SHOW_GOTO_FUNCTIONS, HELP_SHOW_PROPERTIES, HELP_TIMESTAMP, and JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP.
void jbmc_parse_optionst::process_goto_function | ( | goto_model_functiont & | function, |
const abstract_goto_modelt & | model, | ||
const optionst & | options | ||
) |
Definition at line 741 of file jbmc_parse_options.cpp.
References add_failed_symbol_if_needed(), adjust_float_expressions(), abstract_goto_modelt::can_produce_function(), parse_options_baset::cmdline, convert_nondet(), cover_config, messaget::eom(), messaget::error(), optionst::get_bool_option(), messaget::get_message_handler(), goto_check(), instrument_cover_goals(), INVARIANT, cmdlinet::isset(), label_properties(), object_factory_params, REMOVE_ADDED_INSTANCEOF, remove_exceptions(), remove_instanceof(), remove_java_new(), remove_returns(), remove_virtual_functions(), and replace_java_nondet().
bool jbmc_parse_optionst::process_goto_functions | ( | goto_modelt & | goto_model, |
const optionst & | options | ||
) |
Definition at line 898 of file jbmc_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), messaget::error(), full_slicer(), optionst::get_bool_option(), messaget::get_message_handler(), cmdlinet::get_values(), goto_modelt::goto_functions, instrument_cover_goals(), instrument_preconditions(), cmdlinet::isset(), label_properties(), nondet_static(), property_slicer(), reachability_slicer(), REMOVE_ADDED_INSTANCEOF, remove_exceptions(), remove_skip(), remove_unused_functions(), messaget::status(), and goto_functionst::update().
|
protected |
Definition at line 615 of file jbmc_parse_options.cpp.
References parse_options_baset::cmdline, messaget::eom(), messaget::error(), cmdlinet::get_values(), and cmdlinet::isset().
Referenced by doit().
|
protected |
Definition at line 854 of file jbmc_parse_options.cpp.
References parse_options_baset::cmdline, abstract_goto_modelt::get_goto_functions(), messaget::get_message_handler(), abstract_goto_modelt::get_symbol_table(), ui_message_handlert::get_ui(), cmdlinet::isset(), show_goto_functions(), show_loop_ids(), show_properties(), show_symbol_table(), and ui_message_handler.
Referenced by doit().
|
protected |
Definition at line 117 of file jbmc_parse_options.h.
Referenced by doit(), and process_goto_function().
|
protected |
Definition at line 119 of file jbmc_parse_options.h.
Referenced by doit(), generate_function_body(), and process_goto_function().
|
protected |
Definition at line 118 of file jbmc_parse_options.h.
Referenced by doit(), and get_command_line_options().
|
protected |
Definition at line 120 of file jbmc_parse_options.h.
Referenced by doit(), and generate_function_body().
|
protected |
Definition at line 116 of file jbmc_parse_options.h.
Referenced by doit(), get_goto_program(), and show_loaded_functions().