cprover
java_bytecode_vtable.cpp File Reference
#include "java_bytecode_vtable.h"
#include <algorithm>
#include <iterator>
#include <util/symbol.h>
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/vtable.h>
Include dependency graph for java_bytecode_vtable.cpp:

Go to the source code of this file.

Classes

class  is_virtual_name_equalt
 
class  is_name_equalt
 
class  java_bytecode_vtable_factoryt
 

Macros

#define ID_vtable_pointer   "@vtable_pointer"
 

Functions

bool java_bytecode_vtable (symbol_tablet &symbol_table, const std::string &module)
 
static void create_vtable_type (const irep_idt &vt_name, symbol_tablet &symbol_table, const symbolt &class_symbol)
 
static void add_vtable_pointer_member (const irep_idt &vt_name, symbolt &class_symbol)
 
void create_vtable_symbol (symbol_tablet &symbol_table, const symbolt &class_symbol)
 
bool has_vtable_info (const symbol_tablet &symbol_table, const symbolt &class_symbol)
 
void create_vtable_pointer (symbolt &class_symbol)
 
void set_virtual_name (class_typet::methodt &method)
 
static exprt get_ref (const exprt &this_obj, const symbol_typet &target_type)
 
static std::string get_full_class_name (const std::string &name)
 
exprt make_vtable_function (const exprt &func, const exprt &this_obj)
 

Variables

const char ID_virtual_name [] ="virtual_name"
 

Macro Definition Documentation

§ ID_vtable_pointer

#define ID_vtable_pointer   "@vtable_pointer"

Function Documentation

§ add_vtable_pointer_member()

§ create_vtable_pointer()

void create_vtable_pointer ( symbolt class_symbol)

§ create_vtable_symbol()

void create_vtable_symbol ( symbol_tablet symbol_table,
const symbolt class_symbol 
)

§ create_vtable_type()

static void create_vtable_type ( const irep_idt vt_name,
symbol_tablet symbol_table,
const symbolt class_symbol 
)
static

§ get_full_class_name()

static std::string get_full_class_name ( const std::string &  name)
static

Definition at line 398 of file java_bytecode_vtable.cpp.

References has_prefix(), and size_type().

Referenced by make_vtable_function().

§ get_ref()

static exprt get_ref ( const exprt this_obj,
const symbol_typet target_type 
)
static

Definition at line 385 of file java_bytecode_vtable.cpp.

References pointer_type(), and exprt::type().

Referenced by make_vtable_function().

§ 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 func,
const exprt this_obj 
)

§ set_virtual_name()

void set_virtual_name ( class_typet::methodt method)

Variable Documentation

§ ID_virtual_name

const char ID_virtual_name[] ="virtual_name"