cprover
|
The symbol table. More...
#include <symbol_table.h>
Public Types | |
typedef std::unordered_map< irep_idt, symbolt, irep_id_hash > | symbolst |
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 |
symbolt & | lookup (const irep_idt &identifier) |
Find a symbol in the symbol table. More... | |
const symbolt & | lookup (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 |
The symbol table.
Definition at line 52 of file symbol_table.h.
typedef std::unordered_map<irep_idt, symbolt, irep_id_hash> symbol_tablet::symbolst |
Definition at line 55 of file symbol_table.h.
bool symbol_tablet::add | ( | const symbolt & | symbol | ) |
Add a new symbol to the symbol table.
symbol | The symbol to be added to 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(), 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(), has_and_or(), 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(), goto_symext::symex_cpp_new(), goto_symext::symex_malloc(), 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().
|
inline |
Definition at line 69 of file symbol_table.h.
References show().
Referenced by goto_modelt::clear(), and compilet::compile().
|
inline |
Definition at line 87 of file symbol_table.h.
References lookup(), and operator<<().
Referenced by remove_exceptionst::add_exceptional_returns(), shared_bufferst::choice(), java_bytecode_convert_classt::convert(), dump_ct::convert_compound_enum(), create_vtable_symbol(), goto_convertt::do_function_call_symbol(), remove_asmt::gcc_asm_function_call(), java_bytecode_vtable_factoryt::get_class_type(), get_virtual_method_target(), java_bytecode_vtable_factoryt::has_method(), has_vtable_info(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), java_bytecode_vtable_factoryt::is_class_with_vt(), java_record_outputs(), mm_io(), jsil_convertt::operator()(), java_bytecode_vtable_factoryt::operator()(), jsil_typecheckt::typecheck_function_call(), and jsil_typecheckt::update_expr_type().
Find a symbol in the symbol table.
Throws a string if no such symbol is found.
identifier | The name of the symbol to look for |
Definition at line 135 of file symbol_table.cpp.
References id2string(), and symbols.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), remove_exceptionst::add_exceptional_returns(), shared_bufferst::choice(), java_bytecode_languaget::do_ci_lazy_method_conversion(), java_bytecode_vtable_factoryt::get_vt_type_symbol(), has_symbol(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), remove_exceptionst::instrument_throw(), acceleratet::is_underapproximate(), java_record_outputs(), java_static_lifetime_init(), mm_io(), jsil_convertt::operator()(), java_bytecode_vtable_factoryt::operator()(), const_function_pointer_propagationt::propagate(), record_function_outputs(), remove_function(), remove_const_function_pointerst::replace_const_symbols(), remove_const_function_pointerst::resolve_symbol(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), java_bytecode_typecheckt::typecheck_expr_member(), jsil_typecheckt::typecheck_function_call(), remove_static_init_loopst::unwind_enum_static(), and jsil_typecheckt::update_expr_type().
Find a symbol in the symbol table.
Throws a string if no such symbol is found.
identifier | The name of the symbol to look for |
Definition at line 121 of file symbol_table.cpp.
References id2string(), and symbols.
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
symbol | The symbol to be added to the symbol table |
new_symbol | Pointer 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 |
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(), has_and_or(), 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().
|
inline |
Definition at line 66 of file symbol_table.h.
References move().
bool symbol_tablet::remove | ( | const irep_idt & | name | ) |
Remove a symbol from the symbol table.
name | The name of the symbol to remove |
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()().
void symbol_tablet::show | ( | std::ostream & | out | ) | const |
Print the contents of the symbol table.
out | The ostream to direct output to |
Definition at line 109 of file symbol_table.cpp.
References forall_symbols, and symbols.
Referenced by clear(), and operator<<().
|
inline |
Definition at line 80 of file symbol_table.h.
References symbol_base_map, symbol_module_map, and symbols.
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion(), and goto_convert().
symbol_base_mapt symbol_tablet::symbol_base_map |
Definition at line 58 of file symbol_table.h.
Referenced by add(), ansi_c_entry_point(), get_isr(), get_module_by_name(), jsil_entry_point(), move(), remove(), and swap().
symbol_module_mapt symbol_tablet::symbol_module_map |
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(), remove_function_pointerst::compute_address_taken_in_symbols(), cpp_declarator_convertert::convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_class_template_specialization(), 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(), get_module(), get_module_by_name(), goto_convert(), goto_convert_functionst::goto_convert(), 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(), 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().