cprover
|
This is the complete list of members for java_bytecode_convert_methodt, including all inherited members.
address_mapt typedef | java_bytecode_convert_methodt | |
any_superclass_has_clinit_method | java_bytecode_convert_methodt | protected |
bytecode_write_typet enum name | java_bytecode_convert_methodt | protected |
CAST_AS_NEEDED enum value | java_bytecode_convert_methodt | protected |
class_has_clinit_method | java_bytecode_convert_methodt | protected |
class_hierarchy | java_bytecode_convert_methodt | protected |
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const | messaget | |
convert(const symbolt &class_symbol, const methodt &) | java_bytecode_convert_methodt | protected |
convert_aload(const irep_idt &statement, const exprt::operandst &op) const | java_bytecode_convert_methodt | protected |
convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location) | java_bytecode_convert_methodt | protected |
convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
convert_cmp(const exprt::operandst &op, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
convert_const(const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
convert_dup2(exprt::operandst &op, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_dup2_x1(exprt::operandst &op, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_dup2_x2(exprt::operandst &op, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const | java_bytecode_convert_methodt | protected |
convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const | java_bytecode_convert_methodt | protected |
convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const | java_bytecode_convert_methodt | protected |
convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const | java_bytecode_convert_methodt | protected |
convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address) | java_bytecode_convert_methodt | protected |
convert_instructions(const methodt &, const java_class_typet::java_lambda_method_handlest &) | java_bytecode_convert_methodt | protected |
convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_invoke_dynamic(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0) | java_bytecode_convert_methodt | protected |
convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location) | java_bytecode_convert_methodt | protected |
convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) | java_bytecode_convert_methodt | protected |
convert_pop(const irep_idt &statement, const exprt::operandst &op) | java_bytecode_convert_methodt | protected |
convert_putfield(const exprt &arg0, const exprt::operandst &op) | java_bytecode_convert_methodt | protected |
convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr) | java_bytecode_convert_methodt | protected |
convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address) | java_bytecode_convert_methodt | protected |
convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location) | java_bytecode_convert_methodt | protected |
convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location) | java_bytecode_convert_methodt | protected |
convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const | java_bytecode_convert_methodt | protected |
create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &) | java_bytecode_convert_methodt | protected |
current_method | java_bytecode_convert_methodt | protected |
debug() const | messaget | inline |
do_exception_handling(const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c) | java_bytecode_convert_methodt | protected |
draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const | java_bytecode_convert_methodt | protected |
endl(mstreamt &m) | messaget | inlinestatic |
eom(mstreamt &m) | messaget | inlinestatic |
error() const | messaget | inline |
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) | messaget | static |
find_initializers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms) | java_bytecode_convert_methodt | protected |
find_initializers_for_slot(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms) | java_bytecode_convert_methodt | protected |
find_variable_for_slot(size_t address, variablest &var_list) | java_bytecode_convert_methodt | protected |
get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address) | java_bytecode_convert_methodt | protected |
get_bytecode_info(const irep_idt &statement) | java_bytecode_convert_methodt | protected |
get_clinit_call(const irep_idt &classname) | java_bytecode_convert_methodt | protected |
get_lambda_method_symbol(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index) | java_bytecode_convert_methodt | protected |
get_message_handler() | messaget | inline |
get_mstream(unsigned message_level) const | messaget | inline |
get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address, const address_mapt &amap, bool allow_merge=true) | java_bytecode_convert_methodt | protected |
get_static_field(const irep_idt &class_identifier, const irep_idt &component_name) const | java_bytecode_convert_methodt | protected |
INST_INDEX enum value | java_bytecode_convert_methodt | protected |
INST_INDEX_CONST enum value | java_bytecode_convert_methodt | protected |
instruction_sizet enum name | java_bytecode_convert_methodt | protected |
instructionst typedef | java_bytecode_convert_methodt | |
instructiont typedef | java_bytecode_convert_methodt | |
is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const | java_bytecode_convert_methodt | protected |
is_parameter(const local_variablet &v) | java_bytecode_convert_methodt | inlineprotected |
java_bytecode_convert_methodt(symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support) | java_bytecode_convert_methodt | inline |
java_cfg_dominatorst typedef | java_bytecode_convert_methodt | |
label(const irep_idt &address) | java_bytecode_convert_methodt | protectedstatic |
local_variable_table_with_holest typedef | java_bytecode_convert_methodt | |
local_variable_tablet typedef | java_bytecode_convert_methodt | |
local_variablet typedef | java_bytecode_convert_methodt | |
M_DEBUG enum value | messaget | |
M_ERROR enum value | messaget | |
M_PROGRESS enum value | messaget | |
M_RESULT enum value | messaget | |
M_STATISTICS enum value | messaget | |
M_STATUS enum value | messaget | |
M_WARNING enum value | messaget | |
max_array_length | java_bytecode_convert_methodt | protected |
message_handler | messaget | protected |
message_levelt enum name | messaget | |
messaget() | messaget | inline |
messaget(const messaget &other) | messaget | inline |
messaget(message_handlert &_message_handler) | messaget | inlineexplicit |
method_has_this | java_bytecode_convert_methodt | protected |
method_id | java_bytecode_convert_methodt | protected |
method_return_type | java_bytecode_convert_methodt | protected |
method_with_amapt typedef | java_bytecode_convert_methodt | |
methodt typedef | java_bytecode_convert_methodt | |
mstream | messaget | mutableprotected |
needed_lazy_methods | java_bytecode_convert_methodt | protected |
NO_CAST enum value | java_bytecode_convert_methodt | protected |
operator()(const symbolt &class_symbol, const methodt &method) | java_bytecode_convert_methodt | inline |
operator=(const messaget &other) | messaget | inline |
pop(std::size_t n) | java_bytecode_convert_methodt | protected |
pop_residue(std::size_t n) | java_bytecode_convert_methodt | protected |
progress() const | messaget | inline |
push(const exprt::operandst &o) | java_bytecode_convert_methodt | protected |
replace_call_to_cprover_assume(source_locationt location, codet &c) | java_bytecode_convert_methodt | protected |
replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label) | java_bytecode_convert_methodt | protectedstatic |
result() const | messaget | inline |
save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &) | java_bytecode_convert_methodt | protected |
set_message_handler(message_handlert &_message_handler) | messaget | inlinevirtual |
setup_local_variables(const methodt &m, const address_mapt &amap) | java_bytecode_convert_methodt | protected |
slots_for_parameters | java_bytecode_convert_methodt | protected |
stack | java_bytecode_convert_methodt | protected |
stackt typedef | java_bytecode_convert_methodt | protected |
statistics() const | messaget | inline |
status() const | messaget | inline |
string_preprocess | java_bytecode_convert_methodt | protected |
symbol_table | java_bytecode_convert_methodt | protected |
threading_support | java_bytecode_convert_methodt | protected |
throw_assertion_error | java_bytecode_convert_methodt | protected |
tmp_variable(const std::string &prefix, const typet &type) | java_bytecode_convert_methodt | protected |
tmp_vars | java_bytecode_convert_methodt | protected |
try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const | java_bytecode_convert_methodt | protected |
used_local_names | java_bytecode_convert_methodt | protected |
variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast) | java_bytecode_convert_methodt | protected |
variable_cast_argumentt enum name | java_bytecode_convert_methodt | protected |
variables | java_bytecode_convert_methodt | protected |
variablest typedef | java_bytecode_convert_methodt | protected |
warning() const | messaget | inline |
~messaget() | messaget | virtual |