cprover
symbolt Class Reference

Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet. More...

#include <symbol.h>

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

Public Member Functions

const irep_idtdisplay_name () const
 
 symbolt ()
 
void clear ()
 
void swap (symbolt &b)
 
void show (std::ostream &out) const
 
class symbol_exprt symbol_expr () const
 produces a symbol_exprt for a symbol More...
 
bool is_shared () const
 
bool is_procedure_local () const
 
bool is_function () const
 

Public Attributes

typet type
 Type of symbol. More...
 
exprt value
 Initial value of symbol. More...
 
source_locationt location
 Source code location of definition of symbol. More...
 
irep_idt name
 The unique identifier. More...
 
irep_idt module
 Name of module the symbol belongs to. More...
 
irep_idt base_name
 Base (non-scoped) name. More...
 
irep_idt mode
 Language mode. More...
 
irep_idt pretty_name
 Language-specific display name. More...
 
bool is_type
 
bool is_macro
 
bool is_exported
 
bool is_input
 
bool is_output
 
bool is_state_var
 
bool is_property
 
bool is_static_lifetime
 
bool is_thread_local
 
bool is_lvalue
 
bool is_file_local
 
bool is_extern
 
bool is_volatile
 
bool is_parameter
 
bool is_auxiliary
 
bool is_weak
 

Detailed Description

Symbol table entry.

This is a symbol in the symbol table, stored in an object of type symbol_tablet.

Definition at line 30 of file symbol.h.

Constructor & Destructor Documentation

◆ symbolt()

symbolt::symbolt ( )
inline

Definition at line 71 of file symbol.h.

References clear().

Member Function Documentation

◆ clear()

◆ display_name()

◆ is_function()

bool symbolt::is_function ( ) const
inline

Definition at line 106 of file symbol.h.

References irept::id(), is_macro, is_type, and type.

Referenced by lazy_goto_modelt::finalize().

◆ is_procedure_local()

bool symbolt::is_procedure_local ( ) const
inline

Definition at line 101 of file symbol.h.

References is_static_lifetime.

Referenced by constant_propagator_domaint::valuest::set_dirty_to_top().

◆ is_shared()

◆ show()

◆ swap()

◆ symbol_expr()

symbol_exprt symbolt::symbol_expr ( ) const

produces a symbol_exprt for a symbol

Returns
symbol_exprt

Definition at line 111 of file symbol.cpp.

References name, and type.

Referenced by acceleration_utilst::abstract_arrays(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), c_typecheck_baset::add_argc_argv(), add_array_to_length_association(), string_abstractiont::add_dummy_symbol_and_value(), allocate_dynamic_object(), java_object_factoryt::allocate_nondet_length_array(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), acceleration_utilst::assign_array(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), c_nondet_symbol_factory(), goto_convertt::clean_expr(), java_bytecode_convert_methodt::convert(), dump_ct::convert_global_variable(), convert_synchronized_methods(), java_simple_method_stubst::create_method_stub(), dead_object(), deallocated(), java_string_library_preprocesst::decl_string_expr(), value_set_dereferencet::dereference(), acceleration_utilst::do_arrays(), parameter_assignmentst::do_function_calls(), goto_convertt::do_scanf(), string_instrumentationt::do_strerror(), linkingt::duplicate_object_symbol(), acceleration_utilst::ensure_no_overflows(), sat_path_enumeratort::find_distinguishing_points(), disjunctive_polynomial_accelerationt::find_distinguishing_points(), disjunctive_polynomial_accelerationt::fit_polynomial(), polynomial_acceleratort::fit_polynomial_sliced(), remove_function_pointerst::fix_return_type(), java_string_library_preprocesst::fresh_array(), java_string_library_preprocesst::fresh_string(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_subtype_pointer_init(), generate_ansi_c_start_function(), generate_java_start_function(), remove_virtual_functionst::get_child_functions_rec(), remove_virtual_functionst::get_functions(), w_guardst::get_guard_symbol_expr(), remove_exceptionst::get_inflight_exception_global(), remove_virtual_functionst::get_method(), invariant_propagationt::get_objects(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), java_string_library_preprocesst::get_primitive_value_of_object(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), goto_checkt::goto_check(), symex_dereference_statet::has_failed_symbol(), initialize_nondet_string_fields(), acceleratet::insert_automaton(), taint_analysist::instrument(), instrument_start_thread(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_bytecode_instrument_uncaught_exceptions(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), java_string_library_preprocesst::make_argument_for_format(), goto_convertt::make_compound_literal(), string_abstractiont::make_decl_and_def(), java_string_library_preprocesst::make_equals_function_code(), make_nondet_infinite_char_array(), acceleratet::make_overflow_loc(), goto_convertt::make_temp_symbol(), string_abstractiont::make_val_or_dummy_rec(), malloc_object(), mm_io(), object_factory(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), record_function_outputs(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), goto_convertt::remove_malloc(), goto_convertt::remove_temporary_object(), java_string_library_preprocesst::replace_char_array(), acceleratet::set_dirty_vars(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), static_lifetime_init(), java_string_library_preprocesst::string_expr_of_function(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_start_thread(), java_bytecode_instrumentt::throw_exception(), c_typecheck_baset::typecheck_decl(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_symbol(), and cpp_typecheckt::typecheck_template_parameters().

Member Data Documentation

◆ base_name

irep_idt symbolt::base_name

Base (non-scoped) name.

Definition at line 49 of file symbol.h.

Referenced by shared_bufferst::add(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), java_string_library_preprocesst::add_string_type(), c_typecheck_baset::apply_asm_label(), array_name(), assign_parameter_names(), auxiliary_symbolt::auxiliary_symbolt(), 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(), clear(), convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anonymous_union(), convert_decl(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), expr2ct::convert_rec(), create_clinit_wrapper_symbols(), create_initialize(), create_stub_global_symbol(), declare_function(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_dtor(), goto_convertt::do_function_call_symbol(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), cpp_typecheckt::dtor(), symbol_tablet::erase(), goto_convertt::exception_flag(), cpp_typecheckt::find_dtor(), remove_function_pointerst::fix_return_type(), acceleration_utilst::fresh_symbol(), cpp_typecheckt::full_member_initialization(), remove_asmt::gcc_asm_function_call(), java_object_factoryt::gen_nondet_array_init(), generate_ansi_c_start_function(), generate_class_stub(), generate_java_start_function(), languaget::generate_opaque_parameter_symbols(), generate_function_bodiest::generate_parameter_names(), w_guardst::get_guard_symbol(), get_module(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), expr2ct::id_shorthand(), symbol_tablet::insert(), cpp_typecheckt::instantiate_template(), instrument_synchronized_code(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_internal_additions(), java_record_outputs(), jsil_internal_additions(), list_functions(), goto_symext::make_auto_object(), acceleratet::make_symbol(), symbol_tablet::move(), remove_asmt::msc_asm_function_call(), object_factory(), dump_ct::operator()(), shared_bufferst::operator()(), goto_symext::parameter_assignments(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), record_function_outputs(), goto_convertt::remove_function_call(), java_bytecode_convert_methodt::setup_local_variables(), show(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), swap(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), java_bytecode_convert_methodt::tmp_variable(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), goto_symext::trigger_auto_object(), 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_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_function_body(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typedef_type(), unreachable_instructions(), and write_goto_binary_v3().

◆ is_auxiliary

◆ is_exported

◆ is_extern

◆ is_file_local

◆ is_input

◆ is_lvalue

bool symbolt::is_lvalue

◆ is_macro

◆ is_output

◆ is_parameter

◆ is_property

◆ is_state_var

◆ is_static_lifetime

bool symbolt::is_static_lifetime

Definition at line 67 of file symbol.h.

Referenced by shared_bufferst::add(), c_typecheck_baset::add_argc_argv(), uninitializedt::add_assertions(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), java_object_factoryt::allocate_object(), c_typecheck_baset::apply_asm_label(), interpretert::build_memory_map(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), c_new_tmp_symbol(), c_nondet_symbol_factory(), goto_program2codet::cleanup_expr(), clear(), expr2ct::convert_code_decl(), goto_convertt::convert_decl(), dump_ct::convert_global_variable(), cpp_declarator_convertert::convert_new_symbol(), create_stub_global_symbol(), declare_function(), c_typecheck_baset::do_initializer(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), java_string_library_preprocesst::fresh_array(), java_string_library_preprocesst::fresh_string(), generate_ansi_c_start_function(), generate_java_start_function(), w_guardst::get_guard_symbol(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), shared_bufferst::is_buffered(), is_procedure_local(), goto_program_dereferencet::is_valid_object(), java_internal_additions(), instrumentert::local(), linker_script_merget::ls_data2instructions(), goto_convertt::make_compound_literal(), object_factory(), dump_ct::operator()(), read_bin_goto_object_v3(), should_init_symbol(), show(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), goto_symext::symex_start_thread(), java_bytecode_convert_methodt::tmp_variable(), ansi_c_declarationt::to_symbol(), uninitialized_domaint::transform(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_decl(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_symbol(), and write_goto_binary_v3().

◆ is_thread_local

◆ is_type

bool symbolt::is_type

Definition at line 63 of file symbol.h.

Referenced by java_string_library_preprocesst::add_string_type(), c_typecheck_baset::apply_asm_label(), base_type_eqt::base_type_eq_rec(), base_type_rec(), java_simple_method_stubst::check_method_stub(), clear(), dump_ct::convert_compound(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), linkingt::copy_symbols(), cpp_typecheckt::cpp_is_pod(), create_stub_global_symbol(), c_typecheck_baset::do_initializer(), linkingt::duplicate_type_symbol(), cpp_typecheck_resolvet::filter_for_named_scopes(), namespace_baset::follow(), namespace_baset::follow_tag(), dump_ct::gather_global_typedefs(), generate_class_stub(), get_module_by_name(), get_or_create_string_literal_symbol(), is_function(), languaget::is_symbol_opaque_function(), java_add_components_to_class(), jsil_internal_additions(), linkingt::needs_renaming(), linkingt::needs_renaming_type(), dump_ct::operator()(), print_global_state_size(), read_bin_goto_object_v3(), goto_program2codet::remove_const(), remove_internal_symbols(), linkingt::rename_symbols(), java_bytecode_convert_methodt::setup_local_variables(), show(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), ansi_c_declarationt::to_symbol(), type2name_symbol(), type_eq(), type_symbolt::type_symbolt(), jsil_typecheckt::typecheck(), java_bytecode_typecheckt::typecheck(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_operands(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_member_function(), jsil_typecheckt::typecheck_non_type_symbol(), java_bytecode_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), java_bytecode_typecheckt::typecheck_type_symbol(), c_typecheck_baset::typecheck_typedef_type(), and write_goto_binary_v3().

◆ is_volatile

◆ is_weak

◆ location

source_locationt symbolt::location

Source code location of definition of symbol.

Definition at line 40 of file symbol.h.

Referenced by c_typecheck_baset::add_argc_argv(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), goto_program2codet::add_local_types(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), string_abstractiont::build_new_symbol(), c_nondet_symbol_factory(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), clear(), java_string_library_preprocesst::code_for_function(), convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), dump_ct::convert_compound_declaration(), dump_ct::convert_function_declaration(), goto_difft::convert_function_json(), dump_ct::convert_global_variable(), cpp_typecheckt::convert_initializer(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), convert_return(), cpp_typecheckt::default_dtor(), goto_convertt::do_function_call_symbol(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_non_type_symbol(), linkingt::duplicate_object_symbol(), linkingt::duplicate_type_symbol(), dump_ct::gather_global_typedefs(), generate_ansi_c_start_function(), generate_java_start_function(), generate_function_bodiest::generate_parameter_names(), get_fresh_aux_symbol(), expr2ct::get_shorthands(), system_library_symbolst::is_symbol_internal_symbol(), java_bytecode_convert_method_lazy(), java_entry_point(), java_static_lifetime_init(), jsil_entry_point(), linkingt::link_error(), linkingt::link_warning(), list_functions(), linker_script_merget::ls_data2instructions(), cpp_declarator_convertert::main_function_rules(), c_typecheck_baset::move_symbol(), object_factory(), dump_ct::operator()(), goto_difft::output_function(), read_bin_goto_object_v3(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), goto_convertt::remove_malloc(), show(), cpp_typecheck_resolvet::show_identifiers(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), goto_symext::symex_start_thread(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), 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_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), and write_goto_binary_v3().

◆ mode

irep_idt symbolt::mode

Language mode.

Definition at line 52 of file symbol.h.

Referenced by string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), java_string_library_preprocesst::add_string_type(), assign_parameter_names(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), c_nondet_symbol_factory(), cpp_typecheckt::class_template_symbol(), clear(), convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), convert_decl(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), convert_input(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), convert_nondet(), convert_output(), cpp_typecheckt::convert_parameter(), create_clinit_wrapper_symbols(), create_initialize(), create_stub_global_symbol(), declare_function(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), remove_function_pointerst::fix_return_type(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_class_stub(), jbmc_parse_optionst::generate_function_body(), generate_java_start_function(), generate_function_bodiest::generate_parameter_names(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::get_entry_point_mode(), get_fresh_aux_symbol(), get_mode_from_identifier(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), goto_convert(), instrument_cover_goals(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_internal_additions(), jsil_internal_additions(), goto_symext::make_auto_object(), model_argc_argv(), c_typecheck_baset::move_symbol(), remove_asmt::msc_asm_function_call(), object_factory(), goto_symext::parameter_assignments(), read_bin_goto_object_v3(), goto_convertt::remove_function_call(), remove_internal_symbols(), configt::set_object_bits_from_symbol_table(), bmct::setup(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), swap(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), java_bytecode_convert_methodt::tmp_variable(), jsil_declarationt::to_symbol(), c_typecheck_baset::typecheck_array_type(), 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(), java_bytecode_typecheckt::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), jsil_typecheckt::typecheck_symbol_expr(), jsil_typecheckt::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), and write_goto_binary_v3().

◆ module

◆ name

irep_idt symbolt::name

The unique identifier.

Definition at line 43 of file symbol.h.

Referenced by shared_bufferst::add(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_failed_symbol_if_needed(), cpp_typecheckt::add_method_body(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), java_string_library_preprocesst::add_string_type(), c_typecheck_baset::apply_asm_label(), cpp_typecheck_resolvet::apply_template_args(), assign_parameter_names(), auxiliary_symbolt::auxiliary_symbolt(), interpretert::build_memory_map(), string_abstractiont::build_new_symbol(), value_set_dereferencet::build_reference_to(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), c_nondet_symbol_factory(), cpp_typecheckt::check_member_initializers(), java_simple_method_stubst::check_method_stub(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_harness(), clear(), java_string_library_preprocesst::code_for_function(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), dump_ct::convert_compound_declaration(), goto_convertt::convert_decl(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_function_declaration(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), convert_synchronized_methods(), cpp_symbol_expr(), create_clinit_wrapper_symbols(), create_initialize(), java_simple_method_stubst::create_method_stub(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbol(), create_void_function_symbol(), declare_function(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_template_classes(), display_name(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), goto_instrument_parse_optionst::doit(), cpp_typecheckt::dtor(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), ci_lazy_methodst::entry_point_methods(), symbol_tablet::erase(), goto_convertt::exception_flag(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), acceleration_utilst::fresh_symbol(), cpp_typecheckt::full_member_initialization(), function_to_call(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_class_stub(), generate_java_start_function(), languaget::generate_opaque_parameter_symbols(), generate_function_bodiest::generate_parameter_names(), java_bytecode_languaget::generate_support_functions(), get_class_literal_initializer(), value_set_analysis_fit::get_entries(), value_set_analysis_fivrt::get_entries(), value_set_analysis_fivrnst::get_entries(), get_fresh_aux_symbol(), w_guardst::get_guard_symbol(), get_new_name(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), get_symbols_rec(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), infer_opaque_type_fields(), symbol_tablet::insert(), cpp_typecheckt::instantiate_template(), instrument_synchronized_code(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), system_library_symbolst::is_symbol_internal_symbol(), goto_program_dereferencet::is_valid_object(), java_bytecode_convert_method(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_bytecode_instrument_symbol(), java_internal_additions(), java_static_lifetime_init(), jsil_entry_point(), jsil_internal_additions(), link_functions(), linker_script_merget::ls_data2instructions(), cpp_declarator_convertert::main_function_rules(), goto_symext::make_auto_object(), acceleratet::make_symbol(), model_argc_argv(), symbol_tablet::move(), c_typecheck_baset::move_symbol(), remove_asmt::msc_asm_function_call(), object_factory(), jsil_convertt::operator()(), dump_ct::operator()(), goto_functionst::output(), value_set_fit::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), goto_symext::parameter_assignments(), goto_symext::phi_function(), print_global_state_size(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), remove_internal_symbols(), goto_convertt::remove_statement_expression(), linkingt::rename_symbols(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_goto_functions(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), symbol_expr(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_gcc_builtin_va_arg_next(), java_bytecode_convert_methodt::tmp_variable(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), type_eq(), linkingt::type_to_string_verbose(), 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_compound_bases(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_method_bodies(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), jsil_typecheckt::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), and write_goto_binary_v3().

◆ pretty_name

irep_idt symbolt::pretty_name

Language-specific display name.

Definition at line 55 of file symbol.h.

Referenced by string_abstractiont::add_argument(), string_abstractiont::add_dummy_symbol_and_value(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), java_string_library_preprocesst::add_string_type(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), cpp_typecheckt::class_template_symbol(), clear(), java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), expr2cppt::convert_rec(), create_clinit_wrapper_symbols(), create_stub_global_symbol(), declare_function(), display_name(), string_instrumentationt::do_strerror(), acceleration_utilst::fresh_symbol(), generate_class_stub(), get_module(), get_or_create_string_literal_symbol(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), linker_script_merget::ls_data2instructions(), acceleratet::make_symbol(), read_bin_goto_object_v3(), java_bytecode_convert_methodt::setup_local_variables(), show(), cpp_typecheckt::show_instantiation_stack(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), swap(), ansi_c_declarationt::to_symbol(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_type(), java_bytecode_typecheckt::typecheck_expr_symbol(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_symbol(), and write_goto_binary_v3().

◆ type

typet symbolt::type

Type of symbol.

Definition at line 34 of file symbol.h.

Referenced by string_abstractiont::abstract_function_call(), shared_bufferst::add(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), cpp_typecheckt::add_base_components(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_failed_symbol_if_needed(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), string_abstractiont::add_str_arguments(), java_string_library_preprocesst::add_string_type(), linkingt::adjust_object_type(), c_typecheck_baset::apply_asm_label(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), assign_parameter_names(), auxiliary_symbolt::auxiliary_symbolt(), base_type_eqt::base_type_eq_rec(), base_type_rec(), interpretert::build_memory_map(), string_abstractiont::build_new_symbol(), value_set_dereferencet::build_reference_to(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), c_nondet_symbol_factory(), cpp_typecheckt::check_member_initializers(), java_simple_method_stubst::check_method_stub(), cpp_typecheckt::class_template_symbol(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), dump_ct::cleanup_harness(), clear(), clinit_wrapper_do_recursive_calls(), java_string_library_preprocesst::code_for_function(), concurrency_instrumentationt::collect(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), convert(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), expr2ct::convert_code_decl(), dump_ct::convert_compound(), dump_ct::convert_compound_declaration(), convert_decl(), goto_convertt::convert_decl(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_function_declaration(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), expr2cppt::convert_rec(), java_bytecode_languaget::convert_single_method(), convert_synchronized_methods(), linkingt::copy_symbols(), cpp_typecheckt::cpp_is_pod(), cpp_symbol_expr(), create_clinit_wrapper_symbols(), create_initialize(), java_simple_method_stubst::create_method_stub(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbol(), declare_function(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_dtor(), cpp_typecheck_resolvet::disambiguate_template_classes(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), value_sett::do_function_call(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), c_typecheck_baset::do_initializer(), cpp_typecheckt::do_not_typechecked(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), goto_instrument_parse_optionst::doit(), cpp_typecheckt::dtor(), linkingt::duplicate_code_symbol(), linkingt::duplicate_non_type_symbol(), linkingt::duplicate_object_symbol(), linkingt::duplicate_type_symbol(), cpp_typecheckt::elaborate_class_template(), goto_convertt::exception_flag(), interpretert::execute_function_call(), cpp_typecheck_resolvet::filter_for_named_scopes(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), cpp_typecheckt::find_dtor(), cpp_typecheckt::find_parent(), namespace_baset::follow(), namespace_baset::follow_tag(), acceleration_utilst::fresh_symbol(), cpp_typecheckt::full_member_initialization(), dump_ct::gather_global_typedefs(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_class_stub(), generate_java_start_function(), languaget::generate_opaque_method_stubs(), languaget::generate_opaque_parameter_symbols(), generate_function_bodiest::generate_parameter_names(), get_any_incomplete_ancestor_for_stub_static_field(), get_class_literal_initializer(), get_clinit_wrapper_body(), interpretert::get_component(), get_data_type(), value_set_analysis_fit::get_entries(), value_set_analysis_fivrt::get_entries(), value_set_analysis_fivrnst::get_entries(), get_failed_symbol(), w_guardst::get_guard_symbol(), get_inherited_component(), get_length_type(), get_module(), get_module_by_name(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_symbols_rec(), get_thread_safe_clinit_wrapper_body(), interpretert::get_type(), interpretert::get_value(), goto_checkt::goto_check(), cpp_declarator_convertert::handle_initializer(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), infer_opaque_type_fields(), cpp_typecheckt::instantiate_template(), remove_exceptionst::instrument_function_call(), instrument_synchronized_code(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), is_function(), languaget::is_symbol_opaque_function(), system_library_symbolst::is_type_internal(), goto_program_dereferencet::is_valid_object(), java_add_components_to_class(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_bytecode_instrument_uncaught_exceptions(), java_entry_point(), java_enum_static_init_unwind_handler(), java_internal_additions(), java_record_outputs(), java_root_class(), java_static_lifetime_init(), jsil_entry_point(), jsil_internal_additions(), link_functions(), linker_script_merget::ls_data2instructions(), cpp_declarator_convertert::main_function_rules(), goto_symext::make_auto_object(), string_abstractiont::make_decl_and_def(), java_string_library_preprocesst::make_object_get_class_code(), acceleratet::make_symbol(), string_abstractiont::make_val_or_dummy_rec(), model_argc_argv(), remove_asmt::msc_asm_function_call(), needs_clinit_wrapper(), linkingt::needs_renaming_type(), object_factory(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), dump_ct::operator()(), shared_bufferst::operator()(), goto_symex_statet::level0t::operator()(), original_return_type(), goto_symext::parameter_assignments(), linker_script_merget::pointerize_linker_defined_symbols(), print_global_state_size(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), record_function_outputs(), remove_complex(), goto_program2codet::remove_const(), remove_internal_symbols(), goto_convertt::remove_statement_expression(), remove_vector(), goto_symex_statet::rename(), linkingt::rename_symbols(), remove_const_function_pointerst::replace_const_symbols(), remove_returnst::replace_returns(), cpp_typecheck_resolvet::resolve(), remove_returnst::restore_returns(), goto_program2codet::scan_for_varargs(), constant_propagator_domaint::valuest::set_dirty_to_top(), set_internal_dynamic_object(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), string_data_type(), swap(), symbol_expr(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_start_thread(), java_bytecode_convert_methodt::tmp_variable(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), constant_propagator_domaint::transform(), type2name_symbol(), type_eq(), type_symbolt::type_symbolt(), linkingt::type_to_string_verbose(), 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_compound_bases(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), c_typecheck_baset::typecheck_expr_operands(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_new_symbol(), jsil_typecheckt::typecheck_non_type_symbol(), java_bytecode_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_args(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), c_typecheck_baset::typecheck_typedef_type(), remove_returnst::undo_function_calls(), jsil_typecheckt::update_expr_type(), value_set_dereferencet::valid_check(), and write_goto_binary_v3().

◆ value

exprt symbolt::value

Initial value of symbol.

Definition at line 37 of file symbol.h.

Referenced by shared_bufferst::add(), string_abstractiont::add_argument(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_new_variable_symbol(), add_or_get_symbol(), add_stack_depth_symbol(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), java_simple_method_stubst::check_method_stub(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_expr(), clear(), cpp_declarator_convertert::combine_types(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), ci_lazy_methodst::convert_and_analyze_method(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_languaget::convert_lazy_method(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), java_bytecode_languaget::convert_single_method(), compilet::convert_symbols(), convert_synchronized_methods(), convert_threadblock(), linkingt::copy_symbols(), create_initialize(), java_simple_method_stubst::create_method_stub(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbol(), c_typecheck_baset::do_initializer(), cpp_typecheckt::do_not_typechecked(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), lazy_goto_functions_mapt::ensure_entry_converted(), find_macros(), namespace_baset::follow_macros(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_java_start_function(), get_class_literal_initializer(), goto_convertt::get_constant(), w_guardst::get_guard_symbol(), get_or_create_string_literal_symbol(), get_symbols_rec(), goto_convert(), cpp_declarator_convertert::handle_initializer(), cpp_typecheckt::instantiate_template(), instrument_synchronized_code(), introduce_temporaries(), languaget::is_symbol_opaque_function(), java_bytecode_instrument(), java_bytecode_instrument_symbol(), java_internal_additions(), java_static_lifetime_init(), jsil_entry_point(), link_functions(), goto_convertt::make_compound_literal(), string_abstractiont::make_decl_and_def(), remove_asmt::msc_asm_function_call(), jsil_convertt::operator()(), linker_script_merget::pointerize_linker_defined_symbols(), read_bin_goto_object_v3(), remove_complex(), remove_function(), remove_internal_symbols(), remove_vector(), remove_const_function_pointerst::replace_const_symbols(), require_goto_statements::require_entry_point_statements(), remove_const_function_pointerst::resolve_symbol(), show(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), string_from_ns(), swap(), goto_symext::symex_allocate(), goto_symext::symex_start_thread(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_method_bodies(), c_typecheck_baset::typecheck_new_symbol(), jsil_typecheckt::typecheck_non_type_symbol(), java_bytecode_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_symbol(), unsigned_from_ns(), and write_goto_binary_v3().


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