cprover
java_bytecode_convert_methodt Member List

This is the complete list of members for java_bytecode_convert_methodt, including all inherited members.

address_mapt typedefjava_bytecode_convert_methodt
bytecode_write_typet enum namejava_bytecode_convert_methodtprotected
CAST_AS_NEEDED enum valuejava_bytecode_convert_methodtprotected
character_preprocessjava_bytecode_convert_methodtprotected
convert(const symbolt &class_symbol, const methodt &)java_bytecode_convert_methodtprotected
convert_instructions(const methodt &, const code_typet &)java_bytecode_convert_methodtprotected
create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)java_bytecode_convert_methodtprotected
current_methodjava_bytecode_convert_methodtprotected
debug()messagetinline
endl(mstreamt &m)messagetinlinestatic
eom(mstreamt &m)messagetinlinestatic
error()messagetinline
find_initialisers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)java_bytecode_convert_methodtprotected
find_initialisers_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_methodtprotected
find_variable_for_slot(size_t address, variablest &var_list)java_bytecode_convert_methodtprotected
get_array_bounds_check(const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc)java_bytecode_convert_methodtprotected
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_methodtprotected
get_bytecode_info(const irep_idt &statement)java_bytecode_convert_methodtprotected
get_message_handler()messagetinline
get_mstream(unsigned message_level)messagetinline
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_methodtprotected
INST_INDEX enum valuejava_bytecode_convert_methodtprotected
INST_INDEX_CONST enum valuejava_bytecode_convert_methodtprotected
instruction_sizet enum namejava_bytecode_convert_methodtprotected
instructionst typedefjava_bytecode_convert_methodt
instructiont typedefjava_bytecode_convert_methodt
is_constructor(const class_typet::methodt &method)java_bytecode_convert_methodtprotected
java_bytecode_convert_methodt(symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, safe_pointer< ci_lazy_methodst > _lazy_methods, const character_refine_preprocesst &_character_preprocess)java_bytecode_convert_methodtinline
java_cfg_dominatorst typedefjava_bytecode_convert_methodt
label(const irep_idt &address)java_bytecode_convert_methodtprotected
lazy_methodsjava_bytecode_convert_methodtprotected
local_variable_table_with_holest typedefjava_bytecode_convert_methodt
local_variable_tablet typedefjava_bytecode_convert_methodt
local_variablet typedefjava_bytecode_convert_methodt
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
max_array_lengthjava_bytecode_convert_methodtprotected
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
method_has_thisjava_bytecode_convert_methodtprotected
method_idjava_bytecode_convert_methodtprotected
method_return_typejava_bytecode_convert_methodtprotected
method_with_amapt typedefjava_bytecode_convert_methodt
methodt typedefjava_bytecode_convert_methodt
mstreammessagetprotected
NO_CAST enum valuejava_bytecode_convert_methodtprotected
operator()(const symbolt &class_symbol, const methodt &method)java_bytecode_convert_methodtinline
pop(std::size_t n)java_bytecode_convert_methodtprotected
pop_residue(std::size_t n)java_bytecode_convert_methodtprotected
progress()messagetinline
push(const exprt::operandst &o)java_bytecode_convert_methodtprotected
replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)java_bytecode_convert_methodtprotectedstatic
result()messagetinline
save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)java_bytecode_convert_methodtprotected
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
setup_local_variables(const methodt &m, const address_mapt &amap)java_bytecode_convert_methodtprotected
stackjava_bytecode_convert_methodtprotected
stackt typedefjava_bytecode_convert_methodtprotected
statistics()messagetinline
status()messagetinline
symbol_tablejava_bytecode_convert_methodtprotected
tmp_variable(const std::string &prefix, const typet &type)java_bytecode_convert_methodtprotected
tmp_varsjava_bytecode_convert_methodtprotected
used_local_namesjava_bytecode_convert_methodtprotected
variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)java_bytecode_convert_methodtprotected
variable_cast_argumentt enum namejava_bytecode_convert_methodtprotected
variablesjava_bytecode_convert_methodtprotected
variablest typedefjava_bytecode_convert_methodtprotected
warning()messagetinline
~messaget()messagetvirtual