cprover
java_bytecode_vtable.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H
12 
13 #include <util/std_types.h>
14 
16  class symbolt &class_symbol);
17 
19  symbol_tablet &symbol_table,
20  const class symbolt &class_symbol);
21 
22 bool has_vtable_info(
23  const symbol_tablet &symbol_table,
24  const symbolt &class_symbol);
25 
27  const exprt &function,
28  const exprt &this_obj);
29 
30 void set_virtual_name(
31  class_typet::methodt &method);
32 
34  symbol_tablet &symbol_table,
35  const std::string &module);
36 
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...
Definition: symbol.h:33
void create_vtable_symbol(symbol_tablet &symbol_table, const class symbolt &class_symbol)
exprt make_vtable_function(const exprt &function, const exprt &this_obj)
The symbol table.
Definition: symbol_table.h:52
bool java_bytecode_vtable(symbol_tablet &symbol_table, const std::string &module)
componentt methodt
Definition: std_types.h:342
API to type classes.
Base class for all expressions.
Definition: expr.h:46