cprover
|
The symbol table base class interface. More...
#include <symbol_table_base.h>
Classes | |
class | iteratort |
Public Types | |
typedef std::unordered_map< irep_idt, symbolt > | symbolst |
Public Member Functions | |
symbol_table_baset (const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map) | |
symbol_table_baset (const symbol_table_baset &other)=delete | |
symbol_table_baset & | operator= (const symbol_table_baset &other)=delete |
virtual | ~symbol_table_baset () |
Author: Diffblue Ltd. More... | |
operator const symbol_tablet & () const | |
Permits implicit cast to const symbol_tablet &. More... | |
virtual const symbol_tablet & | get_symbol_table () const =0 |
bool | has_symbol (const irep_idt &name) const |
Check whether a symbol exists in the symbol table. More... | |
const symbolt * | lookup (const irep_idt &name) const |
Find a symbol in the symbol table for read-only access. More... | |
const symbolt & | lookup_ref (const irep_idt &name) const |
Find a symbol in the symbol table for read-only access. More... | |
virtual symbolt * | get_writeable (const irep_idt &name)=0 |
Find a symbol in the symbol table for read-write access. More... | |
symbolt & | get_writeable_ref (const irep_idt &name) |
Find a symbol in the symbol table for read-write access. More... | |
bool | add (const symbolt &symbol) |
Add a new symbol to the symbol table. More... | |
virtual std::pair< symbolt &, bool > | insert (symbolt symbol)=0 |
Move or copy a new symbol to the symbol table. More... | |
virtual bool | move (symbolt &symbol, symbolt *&new_symbol)=0 |
bool | remove (const irep_idt &name) |
Remove a symbol from the symbol table. More... | |
virtual void | erase (const symbolst::const_iterator &entry)=0 |
Remove a symbol from the symbol table. More... | |
virtual void | clear ()=0 |
void | show (std::ostream &out) const |
Print the contents of the symbol table. More... | |
virtual iteratort | begin ()=0 |
virtual iteratort | end ()=0 |
Public Attributes | |
const symbolst & | symbols |
const symbol_base_mapt & | symbol_base_map |
const symbol_module_mapt & | symbol_module_map |
The symbol table base class interface.
Definition at line 21 of file symbol_table_base.h.
typedef std::unordered_map<irep_idt, symbolt> symbol_table_baset::symbolst |
Definition at line 24 of file symbol_table_base.h.
|
inline |
Definition at line 32 of file symbol_table_base.h.
|
delete |
|
virtual |
bool symbol_table_baset::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_base.cpp.
References insert().
Referenced by add_new_variable_symbol(), add_or_get_symbol(), assign_parameter_names(), convert(), java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), linkingt::copy_symbols(), create_clinit_wrapper_symbols(), create_initialize(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbol(), declare_function(), goto_convertt::do_function_call_symbol(), acceleration_utilst::fresh_symbol(), ci_lazy_methodst::gather_needed_globals(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_java_start_function(), languaget::generate_opaque_parameter_symbols(), generate_function_bodiest::generate_parameter_names(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), java_bytecode_convert_method_lazy(), java_internal_additions(), jsil_internal_additions(), linker_script_merget::ls_data2instructions(), goto_symext::make_auto_object(), acceleratet::make_symbol(), model_argc_argv(), jsil_convertt::operator()(), dump_ct::operator()(), ci_lazy_methodst::operator()(), read_bin_goto_object_v3(), java_bytecode_convert_methodt::setup_local_variables(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), java_bytecode_convert_methodt::tmp_variable(), c_typecheck_baset::typecheck_array_type(), java_bytecode_typecheckt::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), jsil_typecheckt::typecheck_symbol_expr(), and jsil_typecheckt::typecheck_type().
|
pure virtual |
Implemented in symbol_tablet.
Referenced by remove_skip().
|
pure virtual |
Implemented in symbol_tablet.
|
pure virtual |
Implemented in symbol_tablet.
Referenced by remove_skip().
|
pure virtual |
Remove a symbol from the symbol table.
entry | an iterator pointing at the symbol to remove |
Implemented in symbol_tablet.
Referenced by remove(), and remove_returnst::restore_returns().
|
pure virtual |
Implemented in symbol_tablet.
Referenced by operator const symbol_tablet &().
Find a symbol in the symbol table for read-write access.
name | The name of the symbol to look for |
Implemented in symbol_tablet.
Referenced by add_failed_symbol_if_needed(), java_simple_method_stubst::check_method_stub(), java_bytecode_convert_methodt::convert(), get_writeable_ref(), java_static_lifetime_init(), remove_returnst::replace_returns(), remove_returnst::restore_returns(), and java_bytecode_typecheckt::typecheck().
Find a symbol in the symbol table for read-write access.
name | The name of the symbol to look for |
<tt>std::out_of_range</tt> | if no such symbol exists |
Definition at line 90 of file symbol_table_base.h.
References get_writeable().
Referenced by cpp_typecheckt::clean_up(), cpp_typecheckt::convert_anonymous_union(), java_bytecode_languaget::convert_single_method(), compilet::convert_symbols(), linkingt::copy_symbols(), cpp_typecheckt::do_not_typechecked(), generate_function_bodiest::generate_parameter_names(), infer_opaque_type_fields(), java_bytecode_instrument(), dump_ct::operator()(), linker_script_merget::pointerize_linker_defined_symbols(), remove_function(), goto_program2codet::scan_for_varargs(), cpp_typecheckt::static_and_dynamic_initialization(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_side_effect_function_call(), and c_typecheck_baset::typecheck_type().
|
inline |
Check whether a symbol exists in the symbol table.
name | The name of the symbol to look for |
Definition at line 58 of file symbol_table_base.h.
References symbols.
Referenced by java_bytecode_convert_classt::convert(), ci_lazy_methodst::convert_and_analyze_method(), dump_ct::convert_compound_enum(), java_bytecode_convert_methodt::convert_instructions(), language_filest::convert_lazy_method(), linkingt::copy_symbols(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), goto_convertt::do_function_call_symbol(), jbmc_parse_optionst::doit(), remove_asmt::gcc_asm_function_call(), get_or_create_class_literal_symbol(), lazy_goto_modelt::initialize(), initialize_goto_model(), load_java_class(), model_argc_argv(), needs_clinit_wrapper(), resolve_inherited_componentt::operator()(), ci_lazy_methodst::resolve_method_names(), java_bytecode_instrumentt::throw_exception(), and cpp_typecheckt::typecheck_compound_declarator().
Move or copy a new symbol to the symbol table.
symbol | The symbol to be added to the symbol table - can be moved or copied in |
Implemented in symbol_tablet.
Referenced by add(), add_failed_symbol(), goto_convertt::exception_flag(), generate_class_stub(), generate_java_start_function(), get_fresh_aux_symbol(), and java_bytecode_initialize_parameter_names().
Find a symbol in the symbol table for read-only access.
name | The name of the symbol to look for |
Definition at line 66 of file symbol_table_base.h.
References symbols.
Referenced by java_simple_method_stubst::check_method_stub(), shared_bufferst::choice(), java_string_library_preprocesst::code_assign_components_to_java_string(), java_object_factoryt::gen_nondet_struct_init(), get_class_literal_initializer(), get_data_type(), remove_exceptionst::get_inflight_exception_global(), get_inherited_component(), get_length_type(), get_main_symbol(), remove_returnst::get_or_create_return_value_symbol(), java_string_library_preprocesst::get_primitive_value_of_object(), infer_opaque_type_fields(), instrument_cover_goals(), acceleratet::is_underapproximate(), java_record_outputs(), java_static_lifetime_init(), load_java_class(), mm_io(), java_syntactic_difft::operator()(), syntactic_difft::operator()(), jsil_convertt::operator()(), record_function_outputs(), remove_const_function_pointerst::replace_const_symbols(), require_goto_statements::require_entry_point_statements(), require_symbol::require_symbol_exists(), remove_const_function_pointerst::resolve_symbol(), configt::set_object_bits_from_symbol_table(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), cpp_typecheckt::static_and_dynamic_initialization(), string_data_type(), goto_symext::symex_allocate(), cpp_typecheckt::typecheck_compound_type(), jsil_typecheckt::typecheck_function_call(), and java_bytecode_typecheckt::typecheck_type().
Find a symbol in the symbol table for read-only access.
name | The name of the symbol to look for |
<tt>std::out_of_range</tt> | if no such symbol exists |
Definition at line 76 of file symbol_table_base.h.
References symbols.
Referenced by clinit_wrapper_do_recursive_calls(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), ci_lazy_methodst::convert_and_analyze_method(), java_bytecode_languaget::convert_lazy_method(), java_bytecode_languaget::convert_single_method(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), lazy_goto_functions_mapt::ensure_entry_converted(), lazy_goto_modelt::finalize(), jbmc_parse_optionst::generate_function_body(), assume_false_generate_function_bodiest::generate_function_body_impl(), assert_false_generate_function_bodiest::generate_function_body_impl(), assert_false_then_assume_false_generate_function_bodiest::generate_function_body_impl(), havoc_generate_function_bodiest::generate_function_body_impl(), generate_function_bodiest::generate_parameter_names(), get_any_incomplete_ancestor_for_stub_static_field(), remove_virtual_functionst::get_child_functions_rec(), get_clinit_wrapper_body(), remove_virtual_functionst::get_functions(), java_bytecode_convert_methodt::get_lambda_method_symbol(), remove_returnst::get_or_create_return_value_symbol(), java_bytecode_convert_methodt::get_static_field(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), interpretert::get_type(), interpretert::get_value(), remove_exceptionst::instrument_function_call(), java_enum_static_init_unwind_handler(), java_static_lifetime_init(), java_string_library_preprocesst::make_object_get_class_code(), needs_clinit_wrapper(), ci_lazy_methodst::operator()(), and original_return_type().
Implemented in symbol_tablet.
Referenced by object_factory().
|
inline |
Permits implicit cast to const symbol_tablet &.
Definition at line 49 of file symbol_table_base.h.
References get_symbol_table().
|
delete |
bool symbol_table_baset::remove | ( | const irep_idt & | name | ) |
Remove a symbol from the symbol table.
name | The name of the symbol to remove |
Definition at line 27 of file symbol_table_base.cpp.
References erase(), and symbols.
Referenced by create_initialize(), compilet::link(), and jsil_convertt::operator()().
void symbol_table_baset::show | ( | std::ostream & | out | ) | const |
Print the contents of the symbol table.
out | The ostream to direct output to |
Definition at line 38 of file symbol_table_base.cpp.
References dstringt::compare(), and symbols.
Referenced by operator<<().
const symbol_base_mapt& symbol_table_baset::symbol_base_map |
Definition at line 28 of file symbol_table_base.h.
Referenced by ansi_c_entry_point(), symbol_tablet::erase(), get_isr(), get_module_by_name(), and jsil_entry_point().
const symbol_module_mapt& symbol_table_baset::symbol_module_map |
Definition at line 29 of file symbol_table_base.h.
Referenced by symbol_tablet::erase().
const symbolst& symbol_table_baset::symbols |
Definition at line 27 of file symbol_table_base.h.
Referenced by add_failed_symbols(), ci_lazy_methods_neededt::add_needed_class(), compilet::add_written_cprover_symbols(), 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(), clinit_wrapper_do_recursive_calls(), remove_function_pointerst::compute_address_taken_in_symbols(), convert(), cpp_typecheckt::convert(), cpp_typecheckt::convert_class_template_specialization(), java_bytecode_convert_methodt::convert_invoke(), compilet::convert_symbols(), linkingt::copy_symbols(), 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(), ci_lazy_methodst::gather_needed_globals(), generate_ansi_c_start_function(), generate_function_bodies_factory(), generate_java_start_function(), languaget::generate_opaque_method_stubs(), java_bytecode_convert_methodt::get_clinit_call(), 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(), w_guardst::get_guard_symbol(), get_isr(), linker_script_merget::get_linker_script_data(), get_module(), get_module_by_name(), get_or_create_string_literal_symbol(), goto_convert(), goto_convert_functionst::goto_convert(), has_symbol(), string_instrumentationt::invalidate_buffer(), is_volatile(), java_bytecode_instrument(), java_entry_point(), java_generate_simple_method_stubs(), java_static_lifetime_init(), jsil_entry_point(), link_functions(), link_goto_model(), link_to_library(), lazy_goto_modelt::load_all_functions(), lookup(), namespacet::lookup(), lookup_ref(), model_argc_argv(), mutex_init_instrumentation(), dump_ct::operator()(), class_hierarchyt::operator()(), ci_lazy_methodst::operator()(), original_return_type(), linker_script_merget::pointerize_linker_defined_symbols(), class_hierarchy_grapht::populate(), print_global_state_size(), print_struct_alignment_problems(), remove(), remove_complex(), remove_internal_symbols(), remove_vector(), linkingt::rename(), resolve_friendly_method_name(), ci_lazy_methodst::resolve_method_names(), remove_returnst::restore_returns(), configt::set_from_symbol_table(), show(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), namespacet::smallest_unused_suffix(), static_lifetime_init(), goto_symext::symex_start_thread(), jsil_languaget::to_expr(), linkingt::typecheck(), jsil_typecheckt::typecheck(), java_bytecode_typecheckt::typecheck(), java_bytecode_languaget::typecheck(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_operands(), java_bytecode_typecheckt::typecheck_expr_symbol(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), compilet::write_bin_object_file(), and write_goto_binary_v3().