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 93 of file jbmc_parse_options.h.
Definition at line 73 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 82 of file jbmc_parse_options.cpp.
Definition at line 995 of file jbmc_parse_options.cpp.
|
overridevirtual |
invoke main modules
Implements parse_options_baset.
Definition at line 463 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 1002 of file jbmc_parse_options.cpp.
Definition at line 119 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 682 of file jbmc_parse_options.cpp.
|
overridevirtual |
display command line help
Reimplemented from parse_options_baset.
Definition at line 1040 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 760 of file jbmc_parse_options.cpp.
bool jbmc_parse_optionst::process_goto_functions | ( | goto_modelt & | goto_model, |
const optionst & | options | ||
) |
Definition at line 901 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 98 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 869 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 852 of file jbmc_parse_options.cpp.
|
protected |
Definition at line 129 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 141 of file jbmc_parse_options.h.
|
protected |
Definition at line 126 of file jbmc_parse_options.h.
|
protected |
Definition at line 127 of file jbmc_parse_options.h.