cprover
symbol_tablet Class Reference

The symbol table. More...

#include <symbol_table.h>

Collaboration diagram for symbol_tablet:
[legend]

Public Types

typedef std::unordered_map< irep_idt, symbolt, irep_id_hashsymbolst
 

Public Member Functions

bool add (const symbolt &symbol)
 Add a new symbol to the symbol table. More...
 
bool move (symbolt &symbol, symbolt *&new_symbol)
 Move a symbol into the symbol table. More...
 
bool move (symbolt &symbol)
 
void clear ()
 
bool remove (const irep_idt &name)
 Remove a symbol from the symbol table. More...
 
void show (std::ostream &out) const
 Print the contents of the symbol table. More...
 
void swap (symbol_tablet &other)
 
bool has_symbol (const irep_idt &name) const
 
symboltlookup (const irep_idt &identifier)
 Find a symbol in the symbol table. More...
 
const symboltlookup (const irep_idt &identifier) const
 Find a symbol in the symbol table. More...
 

Public Attributes

symbolst symbols
 
symbol_base_mapt symbol_base_map
 
symbol_module_mapt symbol_module_map
 

Detailed Description

The symbol table.

Definition at line 52 of file symbol_table.h.

Member Typedef Documentation

◆ symbolst

typedef std::unordered_map<irep_idt, symbolt, irep_id_hash> symbol_tablet::symbolst

Definition at line 55 of file symbol_table.h.

Member Function Documentation

◆ add()

bool symbol_tablet::add ( const symbolt symbol)

Add a new symbol to the symbol table.

Parameters
symbolThe symbol to be added to the symbol table
Returns
Returns a boolean indicating whether the process failed, which should only happen if there is a symbol with the same name already in the symbol table

Definition at line 18 of file symbol_table.cpp.

References symbolt::base_name, symbolt::module, symbolt::name, symbol_base_map, symbol_module_map, and symbols.

Referenced by java_bytecode_convert_classt::add_array_types(), remove_exceptionst::add_exceptional_returns(), java_bytecode_convert_classt::add_string_type(), ansi_c_entry_point(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_instructions(), linkingt::copy_symbols(), create_initialize(), create_vtable_type(), java_bytecode_languaget::do_ci_lazy_method_conversion(), goto_convertt::do_function_call_symbol(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), acceleration_utilst::fresh_symbol(), gather_needed_globals(), remove_asmt::gcc_asm_function_call(), get_virtual_method_targets(), path_symex_statet::instantiate_rec(), java_bytecode_convert_method_lazy(), java_entry_point(), java_internal_additions(), jsil_internal_additions(), goto_symext::make_auto_object(), acceleratet::make_symbol(), model_argc_argv(), goto_convertt::new_name(), goto_symext::new_name(), jsil_convertt::operator()(), dump_ct::operator()(), java_bytecode_vtable_factoryt::operator()(), read_bin_goto_object_v3(), read_goto_object(), remove_returnst::replace_returns(), java_bytecode_convert_methodt::setup_local_variables(), goto_symext::symex_cpp_new(), goto_symext::symex_malloc(), java_bytecode_convert_methodt::tmp_variable(), c_typecheck_baset::typecheck_array_type(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), java_bytecode_typecheckt::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), jsil_typecheckt::typecheck_symbol_expr(), and jsil_typecheckt::typecheck_type().

◆ clear()

void symbol_tablet::clear ( void  )
inline

Definition at line 69 of file symbol_table.h.

References symbol_base_map, symbol_module_map, and symbols.

Referenced by goto_modelt::clear(), and compilet::compile().

◆ has_symbol()

◆ lookup() [1/2]

◆ lookup() [2/2]

const symbolt & symbol_tablet::lookup ( const irep_idt identifier) const

Find a symbol in the symbol table.

Throws a string if no such symbol is found.

Parameters
identifierThe name of the symbol to look for
Returns
The symbol in the symbol table with the correct name

Definition at line 121 of file symbol_table.cpp.

References id2string(), and symbols.

◆ move() [1/2]

bool symbol_tablet::move ( symbolt symbol,
symbolt *&  new_symbol 
)

Move a symbol into the symbol table.

If there is already a symbol with the same name then symbol is unchanged, new_symbol points to the symbol with the same name and true is returned. Otherwise, the symbol is moved into the symbol table, symbol is set to be empty, new_symbol points to its new location in the symbol table and false is returned

Parameters
symbolThe symbol to be added to the symbol table
new_symbolPointer which the function will set to either point to the symbol in the symbol table with the same name or to the symbol that has been successfully moved into the symbol table
Returns
Returns a boolean indicating whether the process failed, which should only happen if there is a symbol with the same name already in the symbol table. If the process failed then symbol is unchanged and new_symbol points to the symbol with the same name. If the process succeeded symbol is set to be empty and new_symbol points to its new location in the symbol table

Definition at line 46 of file symbol_table.cpp.

References symbolt::base_name, symbolt::module, symbolt::name, symbol_base_map, symbol_module_map, and symbols.

Referenced by shared_bufferst::add(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_stack_depth_symbol(), ansi_c_entry_point(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), c_nondet_symbol_factory(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), value_set_dereferencet::dereference(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), goto_convertt::exception_flag(), function_to_call(), java_bytecode_convert_classt::generate_class_stub(), get_fresh_aux_symbol(), w_guardst::get_guard_symbol(), symex_dereference_statet::has_failed_symbol(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_entry_point(), jsil_entry_point(), move(), c_typecheck_baset::move_symbol(), object_factory(), goto_symext::parameter_assignments(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_function_template(), and cpp_typecheckt::typecheck_member_function().

◆ move() [2/2]

bool symbol_tablet::move ( symbolt symbol)
inline

Definition at line 66 of file symbol_table.h.

References move().

◆ remove()

bool symbol_tablet::remove ( const irep_idt name)

Remove a symbol from the symbol table.

Parameters
nameThe name of the symbol to remove
Returns
Returns a boolean indicating whether the process failed

Definition at line 73 of file symbol_table.cpp.

References symbol_base_map, symbol_module_map, and symbols.

Referenced by compilet::link(), and jsil_convertt::operator()().

◆ show()

void symbol_tablet::show ( std::ostream &  out) const

Print the contents of the symbol table.

Parameters
outThe ostream to direct output to

Definition at line 109 of file symbol_table.cpp.

References forall_symbols, and symbols.

Referenced by operator<<().

◆ swap()

void symbol_tablet::swap ( symbol_tablet other)
inline

Member Data Documentation

◆ symbol_base_map

symbol_base_mapt symbol_tablet::symbol_base_map

◆ symbol_module_map

symbol_module_mapt symbol_tablet::symbol_module_map

Definition at line 59 of file symbol_table.h.

Referenced by add(), clear(), move(), remove(), and swap().

◆ symbols

symbolst symbol_tablet::symbols

Definition at line 57 of file symbol_table.h.

Referenced by add(), remove_exceptionst::add_exceptional_returns(), add_failed_symbols(), ci_lazy_methodst::add_needed_class(), string_abstractiont::add_str_arguments(), ansi_c_entry_point(), interpretert::build_memory_map(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), cpp_typecheckt::class_template_symbol(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_expr(), clear(), remove_function_pointerst::compute_address_taken_in_symbols(), cpp_declarator_convertert::convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_class_template_specialization(), java_bytecode_convert_methodt::convert_instructions(), compilet::convert_symbols(), linkingt::copy_symbols(), java_bytecode_languaget::do_ci_lazy_method_conversion(), cpp_typecheckt::do_not_typechecked(), string_instrumentationt::do_strerror(), linkingt::do_type_dependencies(), goto_convertt::exception_flag(), function_to_call(), dump_ct::gather_global_typedefs(), gather_needed_globals(), get_cprover_library_text(), cpp_declarator_convertert::get_final_identifier(), value_set_analysis_fit::get_globals(), value_set_analysis_fivrt::get_globals(), value_set_analysis_fivrnst::get_globals(), invariant_propagationt::get_globals(), clobber_parse_optionst::get_goto_program(), w_guardst::get_guard_symbol(), get_isr(), get_main_symbol(), namespacet::get_max(), get_module(), get_module_by_name(), goto_convert(), goto_convert_functionst::goto_convert(), has_symbol(), cpp_typecheckt::instantiate_template(), string_instrumentationt::invalidate_buffer(), is_volatile(), fence_volatilet::is_volatile(), java_bytecode_vtable(), java_entry_point(), java_static_lifetime_init(), jsil_entry_point(), link_functions(), link_to_library(), namespacet::lookup(), lookup(), model_argc_argv(), move(), mutex_init_instrumentation(), class_hierarchyt::operator()(), dump_ct::operator()(), original_return_type(), print_struct_alignment_problems(), read_object_and_link(), remove(), remove_complex(), goto_program2codet::remove_const(), remove_internal_symbols(), remove_vector(), linkingt::rename(), linkingt::rename_symbols(), remove_returnst::replace_returns(), remove_returnst::restore_returns(), goto_program2codet::scan_for_varargs(), configt::set_from_symbol_table(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), goto_symext::symex_start_thread(), jsil_languaget::to_expr(), linkingt::typecheck(), jsil_typecheckt::typecheck(), java_bytecode_typecheckt::typecheck(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_function_identifier(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_operands(), java_bytecode_typecheckt::typecheck_expr_symbol(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), java_bytecode_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), compilet::write_bin_object_file(), and write_goto_binary_v3().


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