CBMC: Member List

address_mapt typedef java_bytecode_convert_methodt

any_superclass_has_clinit_method java_bytecode_convert_methodt protected

assert_no_exceptions_thrown 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

convert(const symbolt &class_symbol, const methodt &, const std::optional< prefix_filtert > &method_context) java_bytecode_convert_methodt protected

convert_aload(const irep_idt &statement, const exprt::operandst &op) java_bytecode_convert_methodt protectedstatic

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 constant_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 source_locationt &source_location, 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 u1 bytecode, 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, method_offsett address) java_bytecode_convert_methodt protected

convert_instructions(const methodt &) java_bytecode_convert_methodt protected

convert_invoke(source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results) java_bytecode_convert_methodt protected

convert_invoke_dynamic(const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code) java_bytecode_convert_methodt protected

convert_load(const exprt &index, char type_char, size_t address) 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, 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, exprt::operandst &results) java_bytecode_convert_methodt protected

convert_parameter_annotations(const methodt &method, const java_method_typet &method_type) java_bytecode_convert_methodt protected

convert_pop(const irep_idt &statement, const exprt::operandst &op) java_bytecode_convert_methodt protected

convert_putfield(const fieldref_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< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address) java_bytecode_convert_methodt protected

convert_shl(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const java_bytecode_convert_methodt protected

convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location) java_bytecode_convert_methodt protected

convert_switch(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

do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c) java_bytecode_convert_methodt protected

draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< method_offsett > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const java_bytecode_convert_methodt protected

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, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address) java_bytecode_convert_methodt protected

get_clinit_call(const irep_idt &classname) java_bytecode_convert_methodt protected

get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett 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 &mangled_method_name) const java_bytecode_convert_methodt protected

is_parameter(const local_variablet &v) java_bytecode_convert_methodt inlineprotected

java_bytecode_convert_method_unit_testt java_bytecode_convert_methodt friend

java_bytecode_convert_methodt(symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, bool assert_no_exceptions_thrown) 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

log java_bytecode_convert_methodt protected

max_array_length java_bytecode_convert_methodt protected

method_has_this java_bytecode_convert_methodt protected

method_id java_bytecode_convert_methodt protected

method_offsett typedef java_bytecode_convert_methodt

method_return_type java_bytecode_convert_methodt protected

methodt typedef java_bytecode_convert_methodt

needed_lazy_methods java_bytecode_convert_methodt protected

NO_CAST enum value java_bytecode_convert_methodt protected

ns java_bytecode_convert_methodt protected

operator()(const symbolt &class_symbol, const methodt &method, const std::optional< prefix_filtert > &method_context) java_bytecode_convert_methodt inline

pop(std::size_t n) java_bytecode_convert_methodt protected

pop_residue(std::size_t n) java_bytecode_convert_methodt protected

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

save_stack_entries(const std::string &, code_blockt &, const bytecode_write_typet, const irep_idt &) java_bytecode_convert_methodt protected

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

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(method_offsett 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) 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