12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H 13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H 37 size_t _max_array_length,
82 typedef std::vector<local_variable_with_holest>
109 const exprt &arraystruct,
153 const instructionst::const_iterator &it,
178 local_variable_table_with_holest::iterator firstvar,
179 local_variable_table_with_holest::iterator varlimit,
201 block_tree_nodet &tree,
203 unsigned address_start,
204 unsigned address_limit,
205 unsigned next_block_start_address);
208 block_tree_nodet &tree,
210 unsigned address_start,
211 unsigned address_limit,
212 unsigned next_block_start_address,
214 bool allow_merge=
true);
void 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)
Given a sequence of users of the same local variable slot, this figures out which ones are related by...
The type of an expression.
java_bytecode_convert_methodt::address_mapt address_mapt
methodt::local_variable_tablet local_variable_tablet
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
void convert(const symbolt &class_symbol, const methodt &)
instructionst::const_iterator source
std::pair< const methodt &, const address_mapt & > method_with_amapt
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
methodt::instructionst instructionst
void operator()(const symbolt &class_symbol, const methodt &method)
safe_pointer< ci_lazy_methodst > lazy_methods
code_blockt & 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)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
irep_idt label(const irep_idt &address)
std::vector< holet > holes
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initialisers_for_slot above for more detail.
character_refine_preprocesst character_preprocess
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::map< unsigned, converted_instructiont > address_mapt
expanding_vectort< variablest > variables
std::set< unsigned > predecessors
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
std::vector< local_variable_with_holest > local_variable_table_with_holest
bool is_constructor(const class_typet::methodt &method)
methodt::local_variablet local_variablet
std::vector< holet > holes
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_parse_treet::methodt methodt
JAVA Bytecode Language Conversion.
API to expression classes.
Context-insensitive lazy methods container.
std::vector< instructiont > instructionst
std::list< unsigned > successors
const size_t max_array_length
java_bytecode_parse_treet::instructiont instructiont
std::list< symbol_exprt > tmp_vars
void find_initialisers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
See find_initialisers_for_slot above for more detail.
exprt::operandst pop(std::size_t n)
std::set< symbol_exprt > used_local_names
std::vector< exprt > operandst
std::vector< block_tree_nodet > branch
codet convert_instructions(const methodt &, const code_typet &)
std::vector< exprt > stackt
std::vector< variablet > variablest
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
void create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)
actually create a temporary variable to hold the value of a stack entry
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
Base class for all expressions.
symbol_tablet & symbol_table
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
std::vector< local_variablet > local_variable_tablet
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
create temporary variables if a write instruction can have undesired side- effects ...
void push(const exprt::operandst &o)
Expression to hold a symbol (variable)
A statement in a programming language.
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
Compute dominators for CFG of goto_function.
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
cfg_dominators_templatet< method_with_amapt, unsigned, false > java_cfg_dominatorst
std::vector< unsigned > branch_addresses
codet get_array_bounds_check(const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc)
static block_tree_nodet get_leaf()