cprover
|
#include <jbmc_parse_options.h>
Static Public Member Functions | |
static void | set_default_options (optionst &) |
Set the options that have default values. | |
Protected Member Functions | |
void | get_command_line_options (optionst &) |
int | get_goto_program (std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &) |
bool | show_loaded_functions (const abstract_goto_modelt &goto_model) |
bool | show_loaded_symbols (const abstract_goto_modelt &goto_model) |
![]() | |
virtual void | register_languages () |
Protected Attributes | |
java_object_factory_parameterst | object_factory_params |
bool | stub_objects_are_not_null |
std::unique_ptr< class_hierarchyt > | class_hierarchy |
optionalt< prefix_filtert > | method_context |
See java_bytecode_languaget::method_context. | |
![]() | |
ui_message_handlert | ui_message_handler |
messaget | log |
Additional Inherited Members | |
![]() | |
cmdlinet | cmdline |
Definition at line 90 of file jbmc_parse_options.h.
Definition at line 67 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 76 of file jbmc_parse_options.cpp.
Definition at line 912 of file jbmc_parse_options.cpp.
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 376 of file jbmc_parse_options.cpp.
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 919 of file jbmc_parse_options.cpp.
Definition at line 109 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 595 of file jbmc_parse_options.cpp.
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 957 of file jbmc_parse_options.cpp.
void jbmc_parse_optionst::process_goto_function | ( | goto_model_functiont & | function, |
const abstract_goto_modelt & | model, | ||
const optionst & | options | ||
) |
Definition at line 673 of file jbmc_parse_options.cpp.
bool jbmc_parse_optionst::process_goto_functions | ( | goto_modelt & | goto_model, |
const optionst & | options | ||
) |
Definition at line 808 of file jbmc_parse_options.cpp.
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 92 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 776 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 759 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 126 of file jbmc_parse_options.h.
|
protected |
See java_bytecode_languaget::method_context.
The two fields are initialized in exactly the same way. TODO Refactor this so it only needs to be computed once, in one place.
Definition at line 138 of file jbmc_parse_options.h.
|
protected |
Definition at line 123 of file jbmc_parse_options.h.
|
protected |
Definition at line 124 of file jbmc_parse_options.h.