cprover
java_bytecode_vtable_factoryt Class Reference
Collaboration diagram for java_bytecode_vtable_factoryt:
[legend]

Public Member Functions

 java_bytecode_vtable_factoryt (symbol_tablet &symbol_table, const std::string &module)
 
symboltget_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_typetget_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_tabletsymbol_table
 
const std::string & module
 
const namespacet ns
 

Detailed Description

Definition at line 54 of file java_bytecode_vtable.cpp.

Constructor & Destructor Documentation

§ java_bytecode_vtable_factoryt()

java_bytecode_vtable_factoryt::java_bytecode_vtable_factoryt ( symbol_tablet symbol_table,
const std::string &  module 
)
inline

Definition at line 63 of file java_bytecode_vtable.cpp.

Member Function Documentation

§ add_vtable_entry()

§ create_base_vtable_entries()

void java_bytecode_vtable_factoryt::create_base_vtable_entries ( struct_exprt vtable_value,
const class_typet class_type,
const class_typet::methodt method 
)
inline

Definition at line 174 of file java_bytecode_vtable.cpp.

References class_typet::bases().

§ create_vtable_entry()

void java_bytecode_vtable_factoryt::create_vtable_entry ( struct_exprt vtable_value,
const class_typet class_type,
const class_typet::methodt method 
)
inline

Definition at line 188 of file java_bytecode_vtable.cpp.

§ create_vtable_symbol()

void java_bytecode_vtable_factoryt::create_vtable_symbol ( symbolt result,
const class_typet class_type 
)
inline

§ extract_types()

void java_bytecode_vtable_factoryt::extract_types ( std::vector< class_typet > &  result,
const irept::subt types,
const class_typet::methodt method 
)
inline

Definition at line 154 of file java_bytecode_vtable.cpp.

§ get_class_type()

const class_typet& java_bytecode_vtable_factoryt::get_class_type ( const irept base)
inline

§ get_vt_type_symbol()

symbolt& java_bytecode_vtable_factoryt::get_vt_type_symbol ( const class_typet class_type)
inline

§ has_component()

bool java_bytecode_vtable_factoryt::has_component ( const class_typet vtable_type,
const irep_idt ifc_name 
)
inline

Definition at line 96 of file java_bytecode_vtable.cpp.

References struct_union_typet::components().

§ has_method()

bool java_bytecode_vtable_factoryt::has_method ( const irept base,
const class_typet::methodt method 
)
inline

§ is_class_with_vt()

bool java_bytecode_vtable_factoryt::is_class_with_vt ( const symbolt symbol)
inline

§ is_virtual()

bool java_bytecode_vtable_factoryt::is_virtual ( const class_typet::methodt method)
inline

Definition at line 168 of file java_bytecode_vtable.cpp.

References irept::get_bool().

§ operator()()

void java_bytecode_vtable_factoryt::operator() ( const irep_idt symbol_name)
inline

§ set_vtable_value()

void java_bytecode_vtable_factoryt::set_vtable_value ( symbolt vtable_symbol,
const class_typet class_type,
struct_exprt vtable_value 
)
inline

Member Data Documentation

§ has_error

bool java_bytecode_vtable_factoryt::has_error

Definition at line 61 of file java_bytecode_vtable.cpp.

§ module

const std::string& java_bytecode_vtable_factoryt::module
private

Definition at line 57 of file java_bytecode_vtable.cpp.

§ ns

const namespacet java_bytecode_vtable_factoryt::ns
private

Definition at line 58 of file java_bytecode_vtable.cpp.

§ symbol_table

symbol_tablet& java_bytecode_vtable_factoryt::symbol_table
private

Definition at line 56 of file java_bytecode_vtable.cpp.


The documentation for this class was generated from the following file: