cprover
|
#include <util/std_types.h>
Go to the source code of this file.
Functions | |
void | create_vtable_pointer (class symbolt &class_symbol) |
void | create_vtable_symbol (symbol_tablet &symbol_table, const class symbolt &class_symbol) |
bool | has_vtable_info (const symbol_tablet &symbol_table, const symbolt &class_symbol) |
exprt | make_vtable_function (const exprt &function, const exprt &this_obj) |
void | set_virtual_name (class_typet::methodt &method) |
bool | java_bytecode_vtable (symbol_tablet &symbol_table, const std::string &module) |
void create_vtable_pointer | ( | class 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 class symbolt & | class_symbol | ||
) |
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, size_type(), and is_virtual_name_equalt::virtual_name.