cprover
|
#include "java_bytecode_vtable.h"
#include <algorithm>
#include <iterator>
#include <util/symbol.h>
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/vtable.h>
Go to the source code of this file.
Classes | |
class | is_virtual_name_equalt |
class | is_name_equalt |
class | java_bytecode_vtable_factoryt |
Macros | |
#define | ID_vtable_pointer "@vtable_pointer" |
Functions | |
bool | java_bytecode_vtable (symbol_tablet &symbol_table, const std::string &module) |
static void | create_vtable_type (const irep_idt &vt_name, symbol_tablet &symbol_table, const symbolt &class_symbol) |
static void | add_vtable_pointer_member (const irep_idt &vt_name, symbolt &class_symbol) |
void | create_vtable_symbol (symbol_tablet &symbol_table, const symbolt &class_symbol) |
bool | has_vtable_info (const symbol_tablet &symbol_table, const symbolt &class_symbol) |
void | create_vtable_pointer (symbolt &class_symbol) |
void | set_virtual_name (class_typet::methodt &method) |
static exprt | get_ref (const exprt &this_obj, const symbol_typet &target_type) |
static std::string | get_full_class_name (const std::string &name) |
exprt | make_vtable_function (const exprt &func, const exprt &this_obj) |
Variables | |
const char | ID_virtual_name [] ="virtual_name" |
#define ID_vtable_pointer "@vtable_pointer" |
Definition at line 283 of file java_bytecode_vtable.cpp.
Referenced by add_vtable_pointer_member(), has_vtable_info(), and make_vtable_function().
Definition at line 285 of file java_bytecode_vtable.cpp.
References struct_union_typet::components(), ID_vtable_pointer, pointer_type(), irept::set(), struct_union_typet::componentt::set_base_name(), struct_union_typet::componentt::set_name(), struct_union_typet::componentt::set_pretty_name(), to_struct_type(), symbolt::type, and exprt::type().
Referenced by create_vtable_pointer().
void create_vtable_pointer | ( | symbolt & | class_symbol | ) |
Definition at line 357 of file java_bytecode_vtable.cpp.
References add_vtable_pointer_member(), get_type(), id2string(), and symbolt::name.
void create_vtable_symbol | ( | symbol_tablet & | symbol_table, |
const symbolt & | class_symbol | ||
) |
Definition at line 313 of file java_bytecode_vtable.cpp.
References create_vtable_type(), get_type(), symbol_tablet::has_symbol(), id2string(), and symbolt::name.
|
static |
Definition at line 264 of file java_bytecode_vtable.cpp.
References symbol_tablet::add(), symbolt::base_name, id2string(), symbolt::is_type, symbolt::location, symbolt::mode, symbolt::module, symbolt::name, symbolt::pretty_name, irept::set(), and symbolt::type.
Referenced by create_vtable_symbol().
|
static |
Definition at line 398 of file java_bytecode_vtable.cpp.
References has_prefix(), and size_type().
Referenced by make_vtable_function().
|
static |
Definition at line 385 of file java_bytecode_vtable.cpp.
References pointer_type(), and exprt::type().
Referenced by make_vtable_function().
bool has_vtable_info | ( | const symbol_tablet & | symbol_table, |
const symbolt & | class_symbol | ||
) |
Definition at line 336 of file java_bytecode_vtable.cpp.
References get_type(), struct_union_typet::has_component(), symbol_tablet::has_symbol(), id2string(), ID_vtable_pointer, symbolt::name, to_struct_union_type(), and symbolt::type.
bool java_bytecode_vtable | ( | symbol_tablet & | symbol_table, |
const std::string & | module | ||
) |
Definition at line 249 of file java_bytecode_vtable.cpp.
References symbol_tablet::symbols.
Definition at line 420 of file java_bytecode_vtable.cpp.
References irept::get(), get_full_class_name(), get_ref(), get_type(), id2string(), ID_vtable_pointer, pointer_type(), and exprt::type().
void set_virtual_name | ( | class_typet::methodt & | method | ) |
Definition at line 377 of file java_bytecode_vtable.cpp.
References id2string(), ID_virtual_name, irept::set(), and size_type().
const char ID_virtual_name[] ="virtual_name" |
Definition at line 21 of file java_bytecode_vtable.cpp.
Referenced by is_virtual_name_equalt::operator()(), and set_virtual_name().