- Generated by
1.9.1
|
CBMC
|
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 |
| 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 class | 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 |
1.9.1