cprover
|
JAVA Bytecode Language Conversion. More...
#include "java_bytecode_convert_method.h"
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_types.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <linking/zero_initializer.h>
#include <goto-programs/cfg.h>
#include <analyses/cfg_dominators.h>
#include <limits>
#include <algorithm>
#include <functional>
#include <unordered_set>
Go to the source code of this file.
Classes | |
class | patternt |
Functions | |
static bool | operator== (const irep_idt &what, const patternt &pattern) |
const size_t | SLOTS_PER_INTEGER (1u) |
const size_t | INTEGER_WIDTH (64u) |
static size_t | count_slots (const size_t value, const code_typet::parametert ¶m) |
static size_t | get_variable_slots (const code_typet::parametert ¶m) |
static irep_idt | strip_java_namespace_prefix (const irep_idt to_strip) |
void | java_bytecode_convert_method_lazy (const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table) |
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More... | |
static irep_idt | get_if_cmp_operator (const irep_idt &stmt) |
static member_exprt | to_member (const exprt &pointer, const exprt &fieldref) |
static void | gather_symbol_live_ranges (unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result) |
static unsigned | get_bytecode_type_width (const typet &ty) |
void | java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, 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_refine) |
JAVA Bytecode Language Conversion.
Definition in file java_bytecode_convert_method.cpp.
|
static |
Definition at line 71 of file java_bytecode_convert_method.cpp.
References irept::get_unsigned_int(), INTEGER_WIDTH(), SLOTS_PER_INTEGER(), and exprt::type().
Referenced by get_variable_slots().
|
static |
Definition at line 733 of file java_bytecode_convert_method.cpp.
References forall_operands, irept::id(), and to_symbol_expr().
Referenced by java_bytecode_convert_methodt::convert_instructions().
|
static |
Definition at line 772 of file java_bytecode_convert_method.cpp.
References irept::get_unsigned_int(), and irept::id().
Referenced by java_bytecode_convert_methodt::convert_instructions().
Definition at line 421 of file java_bytecode_convert_method.cpp.
References patternt::patternt().
Referenced by java_bytecode_convert_methodt::convert_instructions().
|
static |
Definition at line 79 of file java_bytecode_convert_method.cpp.
References count_slots().
Referenced by java_bytecode_convert_methodt::convert().
const size_t INTEGER_WIDTH | ( | 64u | ) |
Referenced by count_slots(), and operator==().
void java_bytecode_convert_method | ( | const symbolt & | class_symbol, |
const java_bytecode_parse_treet::methodt & | method, | ||
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_refine | ||
) |
Definition at line 2435 of file java_bytecode_convert_method.cpp.
References java_bytecode_convert_method().
Referenced by java_bytecode_convert_classt::convert(), java_bytecode_languaget::convert_lazy_method(), java_bytecode_languaget::do_ci_lazy_method_conversion(), and java_bytecode_convert_method().
void java_bytecode_convert_method_lazy | ( | const symbolt & | class_symbol, |
const irep_idt & | method_identifier, | ||
const java_bytecode_parse_treet::methodt & | m, | ||
symbol_tablet & | symbol_table | ||
) |
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.
The caller should call java_bytecode_convert_method later to give the symbol/method a body.
method_identifier
: fully qualified method name, including type signature (e.g. "x.y.z.f:(I)") m
: parsed method object to convert symbol_table
: global symbol table (will be modified) Definition at line 207 of file java_bytecode_convert_method.cpp.
References symbol_tablet::add(), symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, id2string(), java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_reference_type(), java_type_from_string(), symbolt::location, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, irept::set(), source_locationt::set_function(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, to_code_type(), symbolt::type, and exprt::type().
Referenced by java_bytecode_convert_classt::convert(), and java_bytecode_convert_method().
Definition at line 64 of file java_bytecode_convert_method.cpp.
References INTEGER_WIDTH(), and SLOTS_PER_INTEGER().
const size_t SLOTS_PER_INTEGER | ( | 1u | ) |
Referenced by count_slots(), and operator==().
Definition at line 84 of file java_bytecode_convert_method.cpp.
References has_prefix(), and id2string().
Referenced by java_bytecode_convert_methodt::convert_instructions().
|
static |
Definition at line 439 of file java_bytecode_convert_method.cpp.
References irept::get(), java_reference_type(), and exprt::type().
Referenced by java_bytecode_convert_methodt::convert_instructions().