cprover
namespacet Class Reference

TO_BE_DOCUMENTED. More...

#include <namespace.h>

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

Public Member Functions

 namespacet (const symbol_tablet &_symbol_table)
 
 namespacet (const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2)
 
 namespacet (const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2)
 
bool lookup (const irep_idt &name, const symbolt *&symbol) const override
 See namespace_baset::lookup(). More...
 
std::size_t smallest_unused_suffix (const std::string &prefix) const override
 See documentation for namespace_baset::smallest_unused_suffix(). More...
 
const symbol_tabletget_symbol_table () const
 
const symboltlookup (const irep_idt &name) const
 
const symboltlookup (const symbol_exprt &) const
 
const symboltlookup (const symbol_typet &) const
 
const symboltlookup (const tag_typet &) const
 
virtual bool lookup (const irep_idt &name, const symbolt *&symbol) const=0
 Searches for a symbol named name. More...
 
- Public Member Functions inherited from namespace_baset
const symboltlookup (const irep_idt &name) const
 
const symboltlookup (const symbol_exprt &) const
 
const symboltlookup (const symbol_typet &) const
 
const symboltlookup (const tag_typet &) const
 
virtual ~namespace_baset ()
 
void follow_macros (exprt &) const
 
const typetfollow (const typet &) const
 
const typetfollow_tag (const union_tag_typet &) const
 
const typetfollow_tag (const struct_tag_typet &) const
 
const typetfollow_tag (const c_enum_tag_typet &) const
 

Protected Attributes

const symbol_tabletsymbol_table1
 
const symbol_tabletsymbol_table2
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 74 of file namespace.h.

Constructor & Destructor Documentation

◆ namespacet() [1/3]

namespacet::namespacet ( const symbol_tablet _symbol_table)
inlineexplicit

Definition at line 78 of file namespace.h.

References symbol_table1, and symbol_table2.

◆ namespacet() [2/3]

namespacet::namespacet ( const symbol_tablet _symbol_table1,
const symbol_tablet _symbol_table2 
)
inline

Definition at line 81 of file namespace.h.

References symbol_table1, and symbol_table2.

◆ namespacet() [3/3]

namespacet::namespacet ( const symbol_tablet _symbol_table1,
const symbol_tablet _symbol_table2 
)
inline

Definition at line 89 of file namespace.h.

References symbol_table1, and symbol_table2.

Member Function Documentation

◆ get_symbol_table()

◆ lookup() [1/6]

const symbolt& namespace_baset::lookup
inline

Definition at line 33 of file namespace.h.

◆ lookup() [2/6]

const symbolt & namespace_baset::lookup

Definition at line 50 of file namespace.cpp.

◆ lookup() [3/6]

virtual bool namespace_baset::lookup

Searches for a symbol named name.

Iff found, set symbol to point to the symbol and return false; else symbol is unmodified and true is returned. With multiple symbol tables, symbol_table1 is searched first and then symbol_table2.

Returns
False iff the requested symbol is found in at least one of the tables.

◆ lookup() [4/6]

const symbolt & namespace_baset::lookup

Definition at line 40 of file namespace.cpp.

◆ lookup() [5/6]

const symbolt & namespace_baset::lookup

Definition at line 45 of file namespace.cpp.

◆ lookup() [6/6]

bool namespacet::lookup ( const irep_idt name,
const symbolt *&  symbol 
) const
overridevirtual

See namespace_baset::lookup().

Note that namespacet has two symbol tables.

Implements namespace_baset.

Reimplemented in multi_namespacet.

Definition at line 130 of file namespace.cpp.

References symbol_table1, symbol_table2, and symbol_table_baset::symbols.

Referenced by string_abstractiont::abstract_function_call(), actuals_replace_map(), cpp_typecheckt::add_anonymous_members_to_scope(), uninitializedt::add_assertions(), cpp_typecheckt::add_base_components(), code_contractst::add_contract_check(), acceleratet::add_dirty_checks(), w_guardst::add_initialization(), goto_program2codet::add_local_types(), invariant_propagationt::add_objects(), add_or_get_symbol(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), adjust_float_expressions(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), array_name(), shared_bufferst::assignment(), goto_symex_statet::assignment(), base_type_eqt::base_type_eq_rec(), base_type_rec(), value_set_dereferencet::build_reference_to(), string_abstractiont::build_symbol(), string_abstractiont::build_unknown(), cpp_typecheckt::check_component_access(), cpp_typecheckt::check_member_initializers(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), dump_ct::cleanup_harness(), concurrency_instrumentationt::collect(), dump_ct::collect_typedefs_rec(), convert(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert_class_template_specialization(), expr2ct::convert_code_decl(), dump_ct::convert_compound(), goto_convertt::convert_cpp_delete(), convert_decl(), goto_convertt::convert_decl(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), goto_difft::convert_function_json(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), convert_input(), convert_nondet(), convert_output(), cpp_typecheckt::convert_parameter(), expr2ct::convert_rec(), expr2cppt::convert_rec(), convert_return(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheckt::cpp_is_pod(), create_initialize(), create_static_function_call(), dead_object(), deallocated(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheck_resolvet::disambiguate_template_classes(), goto_convertt::do_cpp_new(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), value_sett::do_function_call(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), cpp_typecheckt::do_not_typechecked(), string_instrumentationt::do_strerror(), cpp_typecheckt::do_virtual_table(), goto_instrument_parse_optionst::doit(), cpp_typecheckt::dtor(), dynamic_size(), cpp_typecheckt::elaborate_class_template(), interpretert::execute_function_call(), cpp_typecheck_resolvet::filter_for_named_scopes(), find_macros(), cpp_typecheckt::find_parent(), remove_function_pointerst::fix_return_type(), c_typecastt::follow_with_qualifiers(), cpp_typecheckt::full_member_initialization(), generate_ansi_c_start_function(), cpp_typecheckt::get_bases(), interpretert::get_component(), goto_convertt::get_constant(), get_failed_symbol(), remove_virtual_functionst::get_method(), get_mode_from_identifier(), get_new_name(), expr2ct::get_shorthands(), get_symbols_rec(), symex_bmct::get_unwind_recursion(), cpp_typecheckt::get_virtual_bases(), goto_check(), goto_checkt::goto_check(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), expr2ct::id_shorthand(), ci_lazy_methodst::initialize_instantiated_classes(), escape_analysist::insert_cleanup(), dump_ct::insert_local_type_decls(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), string_instrumentationt::invalidate_buffer(), shared_bufferst::is_buffered(), is_fence(), is_lwfence(), is_shared(), goto_program_dereferencet::is_valid_object(), goto_symex_statet::l2_thread_read_encoding(), goto_symex_statet::l2_thread_write_encoding(), link_functions(), list_functions(), list_undefined_functions(), instrumentert::local(), goto_symext::locality(), cpp_typecheck_resolvet::make_constructors(), string_abstractiont::make_decl_and_def(), malloc_object(), rd_range_domaint::merge_shared(), model_argc_argv(), nondet_static(), taint_analysist::operator()(), dump_ct::operator()(), goto_symex_statet::level0t::operator()(), goto_functionst::output(), value_set_fit::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), goto_difft::output_function(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), goto_symext::phi_function(), goto_convertt::remove_function_call(), goto_symex_statet::rename(), cpp_typecheck_resolvet::resolve(), goto_program2codet::scan_for_varargs(), constant_propagator_domaint::valuest::set_dirty_to_top(), set_internal_dynamic_object(), bmct::setup(), show_goto_functions(), cpp_typecheck_resolvet::show_identifiers(), cpp_typecheckt::show_instantiation_stack(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), splice_call(), static_lifetime_init(), string_from_ns(), goto_symext::symex_assign_symbol(), goto_symext::symex_decl(), goto_symext::symex_gcc_builtin_va_arg_next(), to_expr(), shared_bufferst::track(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), uninitialized_domaint::transform(), rd_range_domaint::transform(), rd_range_domaint::transform_assign(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), rd_range_domaint::transform_start_thread(), goto_symext::trigger_auto_object(), type2name_symbol(), type_eq(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_method_application(), remove_returnst::undo_function_calls(), unreachable_instructions(), unsigned_from_ns(), cpp_typecheckt::user_defined_conversion_sequence(), and value_set_dereferencet::valid_check().

◆ smallest_unused_suffix()

std::size_t namespacet::smallest_unused_suffix ( const std::string &  prefix) const
overridevirtual

See documentation for namespace_baset::smallest_unused_suffix().

Implements namespace_baset.

Reimplemented in multi_namespacet.

Definition at line 117 of file namespace.cpp.

References symbol_table1, symbol_table2, and symbol_table_baset::symbols.

Referenced by get_new_name().

Member Data Documentation

◆ symbol_table1

const symbol_tablet* namespacet::symbol_table1
protected

Definition at line 112 of file namespace.h.

Referenced by get_symbol_table(), lookup(), namespacet(), and smallest_unused_suffix().

◆ symbol_table2

const symbol_tablet * namespacet::symbol_table2
protected

Definition at line 112 of file namespace.h.

Referenced by lookup(), namespacet(), and smallest_unused_suffix().


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