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 () |
Static Public Member Functions | |
static void | set_default_options (optionst &) |
Set the options that have default values. More... | |
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 86 of file jbmc_parse_options.h.
jbmc_parse_optionst::jbmc_parse_optionst | ( | int | argc, |
const char ** | argv | ||
) |
Definition at line 64 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 72 of file jbmc_parse_options.cpp.
bool jbmc_parse_optionst::can_generate_function_body | ( | const irep_idt & | name | ) |
Definition at line 999 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 385 of file jbmc_parse_options.cpp.
References add_failed_symbols(), bmct::add_loop_unwind_handler(), cmdlinet::args, CBMC_VERSION, 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 1006 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 100 of file jbmc_parse_options.cpp.
References parse_options_baset::cmdline, config, CPROVER_EXIT_SUCCESS, CPROVER_EXIT_USAGE_ERROR, messaget::eom(), messaget::error(), optionst::get_bool_option(), cmdlinet::get_value(), cmdlinet::isset(), parse_cover_options(), PARSE_OPTIONS_GOTO_CHECK, PARSE_OPTIONS_GOTO_TRACE, path_strategy_chooser, configt::set(), set_default_options(), optionst::set_option(), path_strategy_choosert::set_path_strategy_options(), path_strategy_choosert::show_strategies(), parse_options_baset::usage_error(), and messaget::warning().
Referenced by doit().
|
protected |
Definition at line 614 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 1042 of file jbmc_parse_options.cpp.
References banner_string(), CBMC_VERSION, HELP_BMC, HELP_FLUSH, HELP_FUNCTIONS, 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 712 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 870 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().
|
static |
Set the options that have default values.
This function can be called from clients that wish to emulate JBMC's default behaviour, for example unit tests.
Definition at line 83 of file jbmc_parse_options.cpp.
References optionst::set_option().
Referenced by get_command_line_options().
|
protected |
Definition at line 586 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 826 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 122 of file jbmc_parse_options.h.
Referenced by doit(), and process_goto_function().
|
protected |
Definition at line 124 of file jbmc_parse_options.h.
Referenced by doit(), generate_function_body(), and process_goto_function().
|
protected |
Definition at line 123 of file jbmc_parse_options.h.
Referenced by doit(), and get_command_line_options().
|
protected |
Definition at line 125 of file jbmc_parse_options.h.
Referenced by doit(), and generate_function_body().
|
protected |
Definition at line 121 of file jbmc_parse_options.h.
Referenced by doit(), get_goto_program(), and show_loaded_functions().