cprover
|
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet. More...
#include <symbol.h>
Public Member Functions | |
const irep_idt & | display_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 |
Symbol table entry.
This is a symbol in the symbol table, stored in an object of type symbol_tablet.
|
inline |
Definition at line 79 of file symbol.h.
References from_irep(), irept::make_nil(), show(), swap(), and to_irep().
Referenced by cpp_typecheck_resolvet::guess_function_template_args(), symbolt(), jsil_declarationt::to_symbol(), and ansi_c_declarationt::to_symbol().
|
inline |
Definition at line 60 of file symbol.h.
References dstringt::empty(), and pretty_name.
Referenced by cpp_declarator_convertert::combine_types(), convert(), symex_bmct::get_unwind_recursion(), cpp_declarator_convertert::handle_initializer(), linkingt::link_error(), linkingt::link_warning(), taint_analysist::operator()(), goto_functions_templatet< goto_programt >::output(), value_sett::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), c_typecheck_baset::typecheck_expr_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), and c_typecheck_baset::typecheck_symbol().
void symbolt::from_irep | ( | const irept & | src | ) |
Definition at line 126 of file symbol.cpp.
References base_name, irept::find(), irept::get(), irept::get_bool(), is_auxiliary, is_exported, is_extern, is_file_local, is_input, is_lvalue, is_macro, is_output, is_parameter, is_property, is_state_var, is_static_lifetime, is_thread_local, is_type, is_volatile, is_weak, location, mode, module, name, pretty_name, type, and value.
Referenced by clear(), and xml_symbol_convertt::convert().
|
inline |
Definition at line 108 of file symbol.h.
References is_static_lifetime, and operator<<().
|
inline |
Definition at line 103 of file symbol.h.
References is_thread_local.
Referenced by fence_all_sharedt::compute(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), is_shared(), goto_symex_statet::level0t::operator()(), goto_symext::phi_function(), rd_range_domaint::transform(), rd_range_domaint::transform_assign(), and rd_range_domaint::transform_function_call().
void symbolt::show | ( | std::ostream & | out | ) | const |
Definition at line 16 of file symbol.cpp.
References base_name, dstringt::empty(), is_auxiliary, is_exported, is_extern, is_file_local, is_input, is_lvalue, is_macro, is_output, is_parameter, is_property, is_state_var, is_static_lifetime, is_thread_local, is_type, is_volatile, is_weak, location, mode, module, name, irept::pretty(), pretty_name, type, and value.
Referenced by clear(), and operator<<().
void symbolt::swap | ( | symbolt & | b | ) |
Definition at line 156 of file symbol.cpp.
References base_name, is_auxiliary, is_exported, is_extern, is_file_local, is_input, is_lvalue, is_macro, is_output, is_parameter, is_property, is_state_var, is_static_lifetime, is_thread_local, is_type, is_volatile, is_weak, location, mode, module, name, pretty_name, SYM_SWAP1, SYM_SWAP2, type, and value.
Referenced by clear().
symbol_exprt symbolt::symbol_expr | ( | ) | const |
produces a symbol_exprt for a symbol
Definition at line 191 of file symbol.cpp.
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(), has_and_or(), 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().
irept symbolt::to_irep | ( | ) | const |
Definition at line 76 of file symbol.cpp.
References irept::add(), base_name, irept::clear(), is_auxiliary, is_exported, is_extern, is_file_local, is_input, is_lvalue, is_macro, is_output, is_parameter, is_property, is_state_var, is_static_lifetime, is_thread_local, is_type, is_volatile, is_weak, location, mode, module, name, pretty_name, irept::set(), type, and value.
Referenced by clear(), and xml_symbol_convertt::convert().
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(), 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(), has_and_or(), 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().
bool symbolt::is_auxiliary |
Definition at line 71 of file symbol.h.
Referenced by auxiliary_symbolt::auxiliary_symbolt(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), goto_symext::symex_assign_symbol(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_exported |
Definition at line 66 of file symbol.h.
Referenced by from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_extern |
Definition at line 71 of file symbol.h.
Referenced by goto_program2codet::cleanup_expr(), convert(), cpp_declarator_convertert::convert(), expr2ct::convert_code_decl(), dump_ct::convert_global_variable(), cpp_declarator_convertert::convert_new_symbol(), linkingt::duplicate_non_type_symbol(), from_irep(), cpp_declarator_convertert::handle_initializer(), jsil_internal_additions(), read_bin_goto_object_v3(), remove_internal_symbols(), 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(), to_irep(), ansi_c_declarationt::to_symbol(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_decl(), c_typecheck_baset::typecheck_expr_operands(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), jsil_typecheckt::typecheck_type(), and write_goto_binary_v3().
bool symbolt::is_file_local |
Definition at line 71 of file symbol.h.
Referenced by uninitializedt::add_assertions(), auxiliary_symbolt::auxiliary_symbolt(), string_abstractiont::build_symbol_constant(), convert(), expr2ct::convert_code_decl(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), goto_convertt::exception_flag(), from_irep(), linkingt::needs_renaming_non_type(), parameter_symbolt::parameter_symbolt(), read_bin_goto_object_v3(), remove_internal_symbols(), java_bytecode_convert_methodt::setup_local_variables(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), ansi_c_declarationt::to_symbol(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_symbol(), and write_goto_binary_v3().
bool symbolt::is_input |
Definition at line 66 of file symbol.h.
Referenced by convert(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_lvalue |
Definition at line 71 of file symbol.h.
Referenced by c_typecheck_baset::add_argc_argv(), uninitializedt::add_assertions(), add_failed_symbol(), add_stack_depth_symbol(), auxiliary_symbolt::auxiliary_symbolt(), convert(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert_instructions(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), cpp_symbol_expr(), java_bytecode_vtable_factoryt::create_vtable_symbol(), value_set_dereferencet::dereference(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), goto_convertt::exception_flag(), from_irep(), string_instrumentationt::invalidate_buffer(), java_internal_additions(), jsil_internal_additions(), goto_symext::make_auto_object(), parameter_symbolt::parameter_symbolt(), read_bin_goto_object_v3(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), to_irep(), cpp_typecheckt::typecheck_compound_declarator(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), and write_goto_binary_v3().
bool symbolt::is_macro |
Definition at line 66 of file symbol.h.
Referenced by c_typecheck_baset::apply_asm_label(), convert(), cpp_typecheck_resolvet::convert_identifier(), cpp_declarator_convertert::convert_new_symbol(), c_typecheck_baset::do_initializer(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), find_macros(), namespace_baset::follow_macros(), from_irep(), dump_ct::gather_global_typedefs(), read_bin_goto_object_v3(), 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(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), 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_symbol(), cpp_typecheckt::typecheck_member_function(), c_typecheck_baset::typecheck_new_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_symbol(), c_typecheck_baset::typecheck_symbol_type(), and write_goto_binary_v3().
bool symbolt::is_output |
Definition at line 66 of file symbol.h.
Referenced by convert(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_parameter |
Definition at line 71 of file symbol.h.
Referenced by from_irep(), expr2ct::get_shorthands(), parameter_symbolt::parameter_symbolt(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), goto_symext::symex_assign_symbol(), to_irep(), ansi_c_declarationt::to_symbol(), c_typecheck_baset::typecheck_new_symbol(), and write_goto_binary_v3().
bool symbolt::is_property |
Definition at line 66 of file symbol.h.
Referenced by convert(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_state_var |
Definition at line 66 of file symbol.h.
Referenced by auxiliary_symbolt::auxiliary_symbolt(), concurrency_instrumentationt::collect(), convert(), java_bytecode_convert_classt::convert(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), java_bytecode_vtable_factoryt::create_vtable_symbol(), string_instrumentationt::do_strerror(), from_irep(), string_instrumentationt::invalidate_buffer(), java_internal_additions(), jsil_internal_additions(), parameter_symbolt::parameter_symbolt(), read_bin_goto_object_v3(), should_init_symbol(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), and write_goto_binary_v3().
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(), 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_empty(), 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().
bool symbolt::is_thread_local |
Definition at line 70 of file symbol.h.
Referenced by uninitializedt::add_assertions(), add_stack_depth_symbol(), auxiliary_symbolt::auxiliary_symbolt(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), concurrency_instrumentationt::collect(), fence_volatilet::compute(), convert(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::exception_flag(), from_irep(), var_mapt::init(), introduce_temporaries(), shared_bufferst::is_buffered(), is_shared(), java_internal_additions(), jsil_internal_additions(), instrumentert::local(), parameter_symbolt::parameter_symbolt(), read_bin_goto_object_v3(), java_bytecode_convert_methodt::setup_local_variables(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), goto_symext::symex_start_thread(), to_irep(), ansi_c_declarationt::to_symbol(), shared_bufferst::track(), and write_goto_binary_v3().
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(), 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().
bool symbolt::is_volatile |
Definition at line 71 of file symbol.h.
Referenced by fence_volatilet::compute(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), and write_goto_binary_v3().
bool symbolt::is_weak |
Definition at line 71 of file symbol.h.
Referenced by linkingt::adjust_object_type_rec(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), from_irep(), read_bin_goto_object_v3(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), swap(), to_irep(), ansi_c_declarationt::to_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), and write_goto_binary_v3().
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(), 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(), has_and_or(), 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().
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(), 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().
irep_idt symbolt::module |
Name of module the symbol belongs to.
Definition at line 49 of file symbol.h.
Referenced by symbol_tablet::add(), string_abstractiont::add_argument(), uninitializedt::add_assertions(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), string_abstractiont::build_new_symbol(), string_abstractiont::build_unknown(), convert(), cpp_typecheckt::convert(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), acceleration_utilst::fresh_symbol(), from_irep(), acceleratet::is_underapproximate(), linkingt::link_error(), linkingt::link_warning(), acceleratet::make_symbol(), symbol_tablet::move(), c_typecheck_baset::move_symbol(), read_bin_goto_object_v3(), remove_returnst::replace_returns(), show(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), cpp_typecheckt::static_and_dynamic_initialization(), swap(), to_expr(), to_irep(), 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(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), and write_goto_binary_v3().
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(), 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(), 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(), has_and_or(), 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(), is_empty(), 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().
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(), 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().
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(), 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(), has_and_or(), 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(), is_empty(), 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().
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(), 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(), has_and_or(), 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().