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
 
irept to_irep () const
 
void from_irep (const irept &src)
 
class symbol_exprt symbol_expr () const
 produces a symbol_exprt for a symbol More...
 
bool is_shared () const
 
bool is_procedure_local () 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 33 of file symbol.h.

Constructor & Destructor Documentation

◆ symbolt()

symbolt::symbolt ( )
inline

Definition at line 74 of file symbol.h.

References clear().

Member Function Documentation

◆ clear()

◆ display_name()

◆ from_irep()

◆ is_procedure_local()

bool symbolt::is_procedure_local ( ) const
inline

Definition at line 108 of file symbol.h.

References is_static_lifetime.

◆ 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 191 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(), string_abstractiont::add_dummy_symbol_and_value(), java_object_factoryt::allocate_nondet_length_array(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), ansi_c_entry_point(), acceleration_utilst::assign_array(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), goto_convertt::clean_expr(), java_bytecode_convert_methodt::convert(), dump_ct::convert_global_variable(), dead_object(), deallocated(), cpp_typecheckt::default_cpctor(), value_set_dereferencet::dereference(), acceleration_utilst::do_arrays(), parameter_assignmentst::do_function_calls(), goto_convertt::do_java_new_array(), goto_convertt::do_scanf(), string_instrumentationt::do_strerror(), cpp_typecheckt::dtor(), 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(), path_symext::function_call_rec(), java_object_factoryt::gen_nondet_array_init(), w_guardst::get_guard_symbol_expr(), remove_virtual_functionst::get_method(), invariant_propagationt::get_objects(), goto_checkt::goto_check(), symex_dereference_statet::has_failed_symbol(), acceleratet::insert_automaton(), path_symex_statet::instantiate_rec(), taint_analysist::instrument(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), remove_exceptionst::instrument_throw(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_entry_point(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), remove_instanceoft::lower_instanceof(), goto_convertt::make_compound_literal(), string_abstractiont::make_decl_and_def(), acceleratet::make_overflow_loc(), goto_convertt::make_temp_symbol(), string_abstractiont::make_val_or_dummy_rec(), malloc_object(), mm_io(), goto_convertt::new_tmp_symbol(), 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(), acceleratet::set_dirty_vars(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), static_lifetime_init(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_start_thread(), c_typecheck_baset::typecheck_decl(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_symbol(), and cpp_typecheckt::typecheck_template_parameters().

◆ to_irep()

Member Data Documentation

◆ base_name

irep_idt symbolt::base_name

Base (non-scoped) name.

Definition at line 52 of file symbol.h.

Referenced by symbol_tablet::add(), const_function_pointer_propagationt::add(), shared_bufferst::add(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), const_function_pointer_propagationt::arg_stackt::add_args(), string_abstractiont::add_argument(), java_bytecode_convert_classt::add_array_types(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_stack_depth_symbol(), java_bytecode_convert_classt::add_string_type(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), array_name(), auxiliary_symbolt::auxiliary_symbolt(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), c_nondet_symbol_factory(), shared_bufferst::choice(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), clear(), convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), expr2ct::convert_rec(), create_initialize(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_dtor(), value_set_dereferencet::dereference(), goto_convertt::do_function_call_symbol(), cpp_typecheckt::do_not_typechecked(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), cpp_typecheckt::dtor(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), goto_convertt::exception_flag(), cpp_typecheckt::find_dtor(), acceleration_utilst::fresh_symbol(), from_irep(), cpp_typecheckt::full_member_initialization(), path_symext::function_call_rec(), function_to_call(), remove_asmt::gcc_asm_function_call(), java_object_factoryt::gen_nondet_array_init(), java_bytecode_convert_classt::generate_class_stub(), get_fresh_aux_symbol(), w_guardst::get_guard_symbol(), get_module(), get_virtual_method_targets(), expr2ct::id_shorthand(), path_symex_statet::instantiate_rec(), cpp_typecheckt::instantiate_template(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), java_entry_point(), java_internal_additions(), java_record_outputs(), jsil_internal_additions(), list_functions(), goto_symext::make_auto_object(), acceleratet::make_symbol(), symbol_tablet::move(), object_factory(), dump_ct::operator()(), shared_bufferst::operator()(), goto_symext::parameter_assignments(), const_function_pointer_propagationt::propagate(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), record_function_outputs(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), goto_convertt::remove_malloc(), remove_returnst::replace_returns(), java_bytecode_convert_methodt::setup_local_variables(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), swap(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), java_bytecode_convert_methodt::tmp_variable(), to_irep(), 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_java_string_literal(), 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(), c_typecheck_baset::typecheck_symbol_type(), jsil_typecheckt::typecheck_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 70 of file symbol.h.

Referenced by shared_bufferst::add(), c_typecheck_baset::add_argc_argv(), uninitializedt::add_assertions(), remove_exceptionst::add_exceptional_returns(), add_stack_depth_symbol(), ansi_c_entry_point(), 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(), convert(), java_bytecode_convert_classt::convert(), expr2ct::convert_code_decl(), goto_convertt::convert_decl(), dump_ct::convert_global_variable(), cpp_declarator_convertert::convert_new_symbol(), java_bytecode_vtable_factoryt::create_vtable_symbol(), c_typecheck_baset::do_initializer(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), from_irep(), w_guardst::get_guard_symbol(), var_mapt::init(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), shared_bufferst::is_buffered(), is_procedure_local(), goto_program_dereferencet::is_valid_object(), java_entry_point(), instrumentert::local(), goto_convertt::make_compound_literal(), object_factory(), dump_ct::operator()(), read_bin_goto_object_v3(), remove_returnst::replace_returns(), should_init_symbol(), 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(), java_bytecode_convert_methodt::tmp_variable(), to_irep(), ansi_c_declarationt::to_symbol(), uninitialized_domaint::transform(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_decl(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), 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 66 of file symbol.h.

Referenced by java_bytecode_convert_classt::add_array_types(), java_bytecode_convert_classt::add_string_type(), c_typecheck_baset::apply_asm_label(), base_type_eqt::base_type_eq_rec(), base_type_rec(), clear(), convert(), java_bytecode_convert_classt::convert(), 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_vtable_type(), c_typecheck_baset::do_initializer(), linkingt::duplicate_type_symbol(), cpp_typecheck_resolvet::filter_for_named_scopes(), namespace_baset::follow(), namespace_baset::follow_symbol(), namespace_baset::follow_tag(), from_irep(), dump_ct::gather_global_typedefs(), java_bytecode_convert_classt::generate_class_stub(), get_module_by_name(), java_bytecode_vtable_factoryt::is_class_with_vt(), jsil_internal_additions(), linkingt::needs_renaming(), linkingt::needs_renaming_type(), dump_ct::operator()(), read_bin_goto_object_v3(), read_goto_object(), remove_internal_symbols(), linkingt::rename_symbols(), java_bytecode_convert_methodt::setup_local_variables(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), to_irep(), ansi_c_declarationt::to_symbol(), type2name_symbol(), type_eq(), type_symbolt::type_symbolt(), 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_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(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), 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(), and write_goto_binary_v3().

◆ is_volatile

◆ is_weak

◆ location

source_locationt symbolt::location

Source code location of definition of symbol.

Definition at line 43 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(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), clear(), convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), dump_ct::convert_compound_declaration(), dump_ct::convert_function_declaration(), 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(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::default_dtor(), goto_convertt::do_function_call_symbol(), cpp_typecheckt::do_not_typechecked(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_non_type_symbol(), linkingt::duplicate_object_symbol(), linkingt::duplicate_type_symbol(), from_irep(), dump_ct::gather_global_typedefs(), get_fresh_aux_symbol(), expr2ct::get_shorthands(), dump_ct::ignore(), java_bytecode_convert_method_lazy(), java_entry_point(), jsil_entry_point(), linkingt::link_error(), linkingt::link_warning(), list_functions(), cpp_declarator_convertert::main_function_rules(), c_typecheck_baset::move_symbol(), object_factory(), dump_ct::operator()(), 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(), 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(), to_irep(), 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 55 of file symbol.h.

Referenced by string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_stack_depth_symbol(), java_bytecode_convert_classt::add_string_type(), 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(), clear(), convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_function(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), create_initialize(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), from_irep(), java_bytecode_convert_classt::generate_class_stub(), get_fresh_aux_symbol(), get_language(), get_virtual_method_targets(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), java_entry_point(), java_internal_additions(), jsil_internal_additions(), goto_symext::make_auto_object(), model_argc_argv(), c_typecheck_baset::move_symbol(), object_factory(), read_bin_goto_object_v3(), goto_convertt::remove_function_call(), remove_internal_symbols(), goto_convertt::remove_temporary_object(), remove_returnst::replace_returns(), bmct::run(), string_refinementt::set_mode(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), swap(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), java_bytecode_convert_methodt::tmp_variable(), to_irep(), jsil_declarationt::to_symbol(), 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_java_string_literal(), 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(), remove_static_init_loopst::unwind_enum_static(), and write_goto_binary_v3().

◆ module

◆ name

irep_idt symbolt::name

The unique identifier.

Definition at line 46 of file symbol.h.

Referenced by symbol_tablet::add(), shared_bufferst::add(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_argument(), java_bytecode_convert_classt::add_array_types(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_stack_depth_symbol(), java_bytecode_convert_classt::add_string_type(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), cpp_typecheck_resolvet::apply_template_args(), 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(), cpp_typecheckt::class_template_symbol(), goto_program2codet::cleanup_expr(), clear(), convert(), 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(), 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(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), cpp_symbol_expr(), create_initialize(), create_vtable_pointer(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), value_set_dereferencet::dereference(), 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(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), goto_convertt::exception_flag(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), remove_function_pointerst::fix_return_type(), acceleration_utilst::fresh_symbol(), from_irep(), cpp_typecheckt::full_member_initialization(), path_symext::function_call_rec(), function_to_call(), remove_asmt::gcc_asm_function_call(), java_bytecode_convert_classt::generate_class_stub(), 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_language(), get_new_name(), get_symbols_rec(), get_virtual_method_targets(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), has_vtable_info(), dump_ct::ignore(), path_symex_statet::instantiate_rec(), cpp_typecheckt::instantiate_template(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), goto_program_dereferencet::is_valid_object(), java_bytecode_convert_method_lazy(), java_entry_point(), java_internal_additions(), jsil_entry_point(), jsil_internal_additions(), link_functions(), cpp_declarator_convertert::main_function_rules(), goto_symext::make_auto_object(), acceleratet::make_symbol(), symbol_tablet::move(), c_typecheck_baset::move_symbol(), object_factory(), jsil_convertt::operator()(), dump_ct::operator()(), goto_functions_templatet< goto_programt >::output(), value_sett::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), goto_symext::parameter_assignments(), goto_symext::phi_function(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), read_goto_object(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), remove_internal_symbols(), goto_convertt::remove_malloc(), goto_convertt::remove_statement_expression(), linkingt::rename_symbols(), remove_returnst::replace_returns(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), symbol_expr(), goto_symext::symex_cpp_new(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_malloc(), goto_symext::symex_malloc(), java_bytecode_convert_methodt::tmp_variable(), to_irep(), 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_java_string_literal(), 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(), and write_goto_binary_v3().

◆ pretty_name

irep_idt symbolt::pretty_name

Language-specific display name.

Definition at line 58 of file symbol.h.

Referenced by string_abstractiont::add_argument(), string_abstractiont::add_dummy_symbol_and_value(), add_stack_depth_symbol(), java_bytecode_convert_classt::add_string_type(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), cpp_typecheckt::class_template_symbol(), clear(), convert(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), expr2cppt::convert_rec(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), display_name(), string_instrumentationt::do_strerror(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), acceleration_utilst::fresh_symbol(), from_irep(), java_bytecode_convert_classt::generate_class_stub(), get_module(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_method_lazy(), acceleratet::make_symbol(), read_bin_goto_object_v3(), java_bytecode_convert_methodt::setup_local_variables(), show(), cpp_typecheckt::show_instantiation_stack(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), 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_java_string_literal(), 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 37 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(), java_bytecode_convert_classt::add_array_types(), uninitializedt::add_assertions(), cpp_typecheckt::add_base_components(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), add_stack_depth_symbol(), java_bytecode_convert_classt::add_string_type(), add_vtable_pointer_member(), linkingt::adjust_object_type(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), 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(), cpp_typecheckt::class_template_symbol(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), clear(), concurrency_instrumentationt::collect(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), fence_volatilet::compute(), convert(), 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(), expr2ct::convert_code_decl(), dump_ct::convert_compound(), 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(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), expr2cppt::convert_rec(), cpp_typecheckt::cpp_is_pod(), cpp_symbol_expr(), create_initialize(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_dtor(), value_set_dereferencet::dereference(), cpp_typecheck_resolvet::disambiguate_template_classes(), value_sett::do_function_call(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::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(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), cpp_typecheck_resolvet::filter_for_named_scopes(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), cpp_typecheckt::find_dtor(), cpp_typecheckt::find_parent(), remove_function_pointerst::fix_return_type(), namespace_baset::follow(), namespace_baset::follow_symbol(), namespace_baset::follow_tag(), c_typecastt::follow_with_qualifiers(), acceleration_utilst::fresh_symbol(), from_irep(), cpp_typecheckt::full_member_initialization(), path_symext::function_call_rec(), function_to_call(), dump_ct::gather_global_typedefs(), remove_asmt::gcc_asm_function_call(), java_bytecode_convert_classt::generate_class_stub(), value_set_analysis_fit::get_entries(), value_set_analysis_fivrt::get_entries(), value_set_analysis_fivrnst::get_entries(), get_failed_symbol(), get_fresh_aux_symbol(), w_guardst::get_guard_symbol(), get_main_symbol(), get_module(), get_module_by_name(), get_symbols_rec(), get_virtual_method_targets(), goto_checkt::goto_check(), cpp_declarator_convertert::handle_initializer(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), has_vtable_info(), dump_ct::ignore(), path_symex_statet::instantiate_rec(), cpp_typecheckt::instantiate_template(), introduce_temporaries(), string_instrumentationt::invalidate_buffer(), java_bytecode_vtable_factoryt::is_class_with_vt(), goto_program_dereferencet::is_valid_object(), java_bytecode_convert_method_lazy(), java_entry_point(), java_internal_additions(), java_record_outputs(), java_root_class(), java_static_lifetime_init(), jsil_entry_point(), jsil_internal_additions(), link_functions(), cpp_declarator_convertert::main_function_rules(), goto_symext::make_auto_object(), string_abstractiont::make_decl_and_def(), acceleratet::make_symbol(), string_abstractiont::make_val_or_dummy_rec(), model_argc_argv(), linkingt::needs_renaming_type(), object_factory(), dump_ct::operator()(), goto_symex_statet::level0t::operator()(), shared_bufferst::operator()(), java_bytecode_vtable_factoryt::operator()(), goto_symext::parameter_assignments(), cpp_scopest::put_into_scope(), read_bin_goto_object_v3(), read_goto_object(), record_function_outputs(), remove_complex(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), remove_internal_symbols(), goto_convertt::remove_malloc(), 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(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), swap(), symbol_expr(), goto_symext::symex_cpp_new(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_start_thread(), java_bytecode_convert_methodt::tmp_variable(), to_irep(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), 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(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), java_bytecode_typecheckt::typecheck_expr_member(), 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(), java_bytecode_typecheckt::typecheck_non_type_symbol(), 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(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_args(), jsil_typecheckt::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), remove_returnst::undo_function_calls(), remove_static_init_loopst::unwind_enum_static(), 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 40 of file symbol.h.

Referenced by shared_bufferst::add(), string_abstractiont::add_argument(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_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(), goto_program2codet::cleanup_expr(), clear(), cpp_declarator_convertert::combine_types(), convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), 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_instructions(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), create_initialize(), java_bytecode_languaget::do_ci_lazy_method_conversion(), c_typecheck_baset::do_initializer(), cpp_typecheckt::do_not_typechecked(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), find_macros(), namespace_baset::follow_macros(), namespace_baset::follow_symbol(), from_irep(), remove_asmt::gcc_asm_function_call(), goto_convertt::get_constant(), w_guardst::get_guard_symbol(), get_main_symbol(), get_symbols_rec(), get_virtual_method_targets(), goto_convert(), cpp_declarator_convertert::handle_initializer(), cpp_typecheckt::instantiate_template(), introduce_temporaries(), java_entry_point(), java_static_lifetime_init(), jsil_entry_point(), link_functions(), goto_convertt::make_compound_literal(), string_abstractiont::make_decl_and_def(), jsil_convertt::operator()(), read_bin_goto_object_v3(), remove_complex(), remove_function(), remove_internal_symbols(), remove_vector(), remove_const_function_pointerst::replace_const_symbols(), remove_const_function_pointerst::resolve_symbol(), java_bytecode_vtable_factoryt::set_vtable_value(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), string_from_ns(), swap(), goto_symext::symex_start_thread(), to_irep(), 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(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), 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: