10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H 11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H 20 const class symbolt &class_symbol);
27 const exprt &
function,
28 const exprt &this_obj);
35 const std::string &module);
37 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H bool has_vtable_info(const symbol_tablet &symbol_table, const symbolt &class_symbol)
void create_vtable_pointer(class symbolt &class_symbol)
void set_virtual_name(class_typet::methodt &method)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void create_vtable_symbol(symbol_tablet &symbol_table, const class symbolt &class_symbol)
exprt make_vtable_function(const exprt &function, const exprt &this_obj)
bool java_bytecode_vtable(symbol_tablet &symbol_table, const std::string &module)
Base class for all expressions.