cprover
|
Public Member Functions | |
java_bytecode_vtable_factoryt (symbol_tablet &symbol_table, const std::string &module) | |
symbolt & | get_vt_type_symbol (const class_typet &class_type) |
void | create_vtable_symbol (symbolt &result, const class_typet &class_type) |
bool | has_component (const class_typet &vtable_type, const irep_idt &ifc_name) |
void | add_vtable_entry (struct_exprt &vtable_value, const class_typet &interface, const class_typet &implementor, const class_typet::methodt &implementation) |
const class_typet & | get_class_type (const irept &base) |
bool | has_method (const irept &base, const class_typet::methodt &method) |
void | extract_types (std::vector< class_typet > &result, const irept::subt &types, const class_typet::methodt &method) |
bool | is_virtual (const class_typet::methodt &method) |
void | create_base_vtable_entries (struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method) |
void | create_vtable_entry (struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method) |
void | set_vtable_value (symbolt &vtable_symbol, const class_typet &class_type, struct_exprt &vtable_value) |
bool | is_class_with_vt (const symbolt &symbol) |
void | operator() (const irep_idt &symbol_name) |
Public Attributes | |
bool | has_error |
Private Attributes | |
symbol_tablet & | symbol_table |
const std::string & | module |
const namespacet | ns |
Definition at line 54 of file java_bytecode_vtable.cpp.
|
inline |
Definition at line 63 of file java_bytecode_vtable.cpp.
|
inline |
Definition at line 103 of file java_bytecode_vtable.cpp.
References struct_union_typet::components(), exprt::copy_to_operands(), struct_union_typet::componentt::get_name(), get_vt_type_symbol(), has_component(), class_typet::methods(), pointer_type(), struct_union_typet::componentt::set_base_name(), struct_union_typet::componentt::set_name(), to_class_type(), and exprt::type().
Referenced by create_base_vtable_entries(), and create_vtable_entry().
|
inline |
Definition at line 174 of file java_bytecode_vtable.cpp.
References add_vtable_entry(), class_typet::bases(), extract_types(), and is_virtual().
Referenced by operator()().
|
inline |
Definition at line 188 of file java_bytecode_vtable.cpp.
References add_vtable_entry(), and is_virtual().
Referenced by operator()().
|
inline |
Definition at line 79 of file java_bytecode_vtable.cpp.
References symbolt::base_name, irept::get(), get_vt_type_symbol(), id2string(), symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::location, symbolt::mode, symbolt::module, module, symbolt::name, symbolt::pretty_name, and symbolt::type.
Referenced by operator()().
|
inline |
Definition at line 154 of file java_bytecode_vtable.cpp.
References get_class_type(), and has_method().
Referenced by create_base_vtable_entries().
|
inline |
Definition at line 130 of file java_bytecode_vtable.cpp.
References irept::find(), symbol_typet::get_identifier(), symbol_tablet::has_symbol(), namespacet::lookup(), ns, symbol_table, to_class_type(), and to_symbol_type().
Referenced by extract_types().
|
inline |
Definition at line 73 of file java_bytecode_vtable.cpp.
References irept::get(), get_type(), id2string(), symbol_tablet::lookup(), and symbol_table.
Referenced by add_vtable_entry(), and create_vtable_symbol().
|
inline |
Definition at line 96 of file java_bytecode_vtable.cpp.
References struct_union_typet::components().
Referenced by add_vtable_entry().
|
inline |
Definition at line 140 of file java_bytecode_vtable.cpp.
References irept::find(), symbol_typet::get_identifier(), symbol_tablet::has_symbol(), namespacet::lookup(), ns, symbol_table, to_class_type(), and to_symbol_type().
Referenced by extract_types().
|
inline |
Definition at line 205 of file java_bytecode_vtable.cpp.
References irept::get(), get_type(), symbol_tablet::has_symbol(), irept::id(), id2string(), symbolt::is_type, symbol_table, to_class_type(), and symbolt::type.
Referenced by operator()().
|
inline |
Definition at line 168 of file java_bytecode_vtable.cpp.
References irept::get_bool().
Referenced by create_base_vtable_entries(), and create_vtable_entry().
|
inline |
Definition at line 214 of file java_bytecode_vtable.cpp.
References symbol_tablet::add(), create_base_vtable_entries(), create_vtable_entry(), create_vtable_symbol(), symbol_tablet::has_symbol(), id2string(), is_class_with_vt(), symbol_tablet::lookup(), class_typet::methods(), set_vtable_value(), symbol_table, to_class_type(), and symbolt::type.
|
inline |
Definition at line 196 of file java_bytecode_vtable.cpp.
References irept::get(), get_type(), id2string(), exprt::type(), and symbolt::value.
Referenced by operator()().
bool java_bytecode_vtable_factoryt::has_error |
Definition at line 61 of file java_bytecode_vtable.cpp.
|
private |
Definition at line 57 of file java_bytecode_vtable.cpp.
Referenced by create_vtable_symbol().
|
private |
Definition at line 58 of file java_bytecode_vtable.cpp.
Referenced by get_class_type(), and has_method().
|
private |
Definition at line 56 of file java_bytecode_vtable.cpp.
Referenced by get_class_type(), get_vt_type_symbol(), has_method(), is_class_with_vt(), and operator()().