cprover
symbol_table_baset Class Referenceabstract

The symbol table base class interface. More...

#include <symbol_table_base.h>

Inheritance diagram for symbol_table_baset:
[legend]
Collaboration diagram for symbol_table_baset:
[legend]

Classes

class  iteratort
 

Public Types

typedef std::unordered_map< irep_idt, symboltsymbolst
 

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_basetoperator= (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_tabletget_symbol_table () const =0
 
bool has_symbol (const irep_idt &name) const
 Check whether a symbol exists in the symbol table. More...
 
const symboltlookup (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
const symboltlookup_ref (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
virtual symboltget_writeable (const irep_idt &name)=0
 Find a symbol in the symbol table for read-write access. More...
 
symboltget_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 symbolstsymbols
 
const symbol_base_maptsymbol_base_map
 
const symbol_module_maptsymbol_module_map
 

Detailed Description

The symbol table base class interface.

Definition at line 21 of file symbol_table_base.h.

Member Typedef Documentation

◆ symbolst

typedef std::unordered_map<irep_idt, symbolt> symbol_table_baset::symbolst

Definition at line 24 of file symbol_table_base.h.

Constructor & Destructor Documentation

◆ symbol_table_baset() [1/2]

symbol_table_baset::symbol_table_baset ( const symbolst symbols,
const symbol_base_mapt symbol_base_map,
const symbol_module_mapt symbol_module_map 
)
inline

Definition at line 32 of file symbol_table_base.h.

◆ symbol_table_baset() [2/2]

symbol_table_baset::symbol_table_baset ( const symbol_table_baset other)
delete

◆ ~symbol_table_baset()

symbol_table_baset::~symbol_table_baset ( )
virtual

Author: Diffblue Ltd.

Destructor

Definition at line 9 of file symbol_table_base.cpp.

Member Function Documentation

◆ add()

bool symbol_table_baset::add ( const symbolt symbol)

Add a new symbol to the symbol table.

Parameters
symbolThe symbol to be added to the symbol table
Returns
Returns true if 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_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(), remove_asmt::msc_asm_function_call(), 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().

◆ begin()

virtual iteratort symbol_table_baset::begin ( )
pure virtual

Implemented in symbol_tablet.

Referenced by remove_skip().

◆ clear()

virtual void symbol_table_baset::clear ( )
pure virtual

Implemented in symbol_tablet.

◆ end()

virtual iteratort symbol_table_baset::end ( )
pure virtual

Implemented in symbol_tablet.

Referenced by remove_skip().

◆ erase()

virtual void symbol_table_baset::erase ( const symbolst::const_iterator &  entry)
pure virtual

Remove a symbol from the symbol table.

Parameters
entryan iterator pointing at the symbol to remove

Implemented in symbol_tablet.

Referenced by remove(), and remove_returnst::restore_returns().

◆ get_symbol_table()

virtual const symbol_tablet& symbol_table_baset::get_symbol_table ( ) const
pure virtual

Implemented in symbol_tablet.

Referenced by operator const symbol_tablet &().

◆ get_writeable()

virtual symbolt* symbol_table_baset::get_writeable ( const irep_idt name)
pure virtual

Find a symbol in the symbol table for read-write access.

Parameters
nameThe name of the symbol to look for
Returns
a pointer to the found symbol if it exists, nullptr otherwise.

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().

◆ get_writeable_ref()

◆ has_symbol()

◆ insert()

virtual std::pair<symbolt &, bool> symbol_table_baset::insert ( symbolt  symbol)
pure virtual

Move or copy a new symbol to the symbol table.

Remarks
: This is a nicer interface than move and achieves the same result as both move and add
Parameters
symbolThe symbol to be added to the symbol table - can be moved or copied in
Returns
Returns a reference to the newly inserted symbol or to the existing symbol if a symbol with the same name already exists in the symbol table, along with a bool that is true if a new symbol was inserted.

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().

◆ lookup()

const symbolt* symbol_table_baset::lookup ( const irep_idt name) const
inline

Find a symbol in the symbol table for read-only access.

Parameters
nameThe name of the symbol to look for
Returns
a pointer to the found symbol if it exists, nullptr otherwise.

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().

◆ lookup_ref()

const symbolt& symbol_table_baset::lookup_ref ( const irep_idt name) const
inline

Find a symbol in the symbol table for read-only access.

Parameters
nameThe name of the symbol to look for
Returns
A reference to the symbol
Exceptions
<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(), 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().

◆ move()

virtual bool symbol_table_baset::move ( symbolt symbol,
symbolt *&  new_symbol 
)
pure virtual

Implemented in symbol_tablet.

Referenced by object_factory().

◆ operator const symbol_tablet &()

symbol_table_baset::operator const symbol_tablet & ( ) const
inline

Permits implicit cast to const symbol_tablet &.

Definition at line 49 of file symbol_table_base.h.

References get_symbol_table().

◆ operator=()

symbol_table_baset& symbol_table_baset::operator= ( const symbol_table_baset other)
delete

◆ remove()

bool symbol_table_baset::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 i.e. false if the symbol was removed, or true if it didn't exist.

Definition at line 27 of file symbol_table_base.cpp.

References erase(), and symbols.

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

◆ show()

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

Print the contents of the symbol table.

Parameters
outThe ostream to direct output to

Definition at line 38 of file symbol_table_base.cpp.

References dstringt::compare(), and symbols.

Referenced by operator<<().

Member Data Documentation

◆ symbol_base_map

const symbol_base_mapt& symbol_table_baset::symbol_base_map

◆ symbol_module_map

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().

◆ symbols

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_monitor_call(), 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(), 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(), c_typecheck_baset::typecheck_typedef_type(), compilet::write_bin_object_file(), and write_goto_binary_v3().


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