cprover
java_bytecode_vtable.h File Reference
#include <util/std_types.h>
Include dependency graph for java_bytecode_vtable.h:
This graph shows which files directly or indirectly include this file:

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)
 

Function Documentation

◆ create_vtable_pointer()

void create_vtable_pointer ( class symbolt class_symbol)

◆ create_vtable_symbol()

void create_vtable_symbol ( symbol_tablet symbol_table,
const class symbolt class_symbol 
)

◆ has_vtable_info()

bool has_vtable_info ( const symbol_tablet symbol_table,
const symbolt class_symbol 
)

◆ java_bytecode_vtable()

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.

◆ make_vtable_function()

exprt make_vtable_function ( const exprt function,
const exprt this_obj 
)

◆ set_virtual_name()

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().