cprover
namespace_baset Class Referenceabstract

#include <namespace.h>

Inheritance diagram for namespace_baset:
[legend]

Public Member Functions

const symboltlookup (const irep_idt &name) const
 
const symboltlookup (const irept &irep) const
 
virtual ~namespace_baset ()
 
void follow_symbol (irept &irep) const
 
void follow_macros (exprt &expr) const
 
const typetfollow (const typet &src) const
 
const typetfollow_tag (const union_tag_typet &src) const
 
const typetfollow_tag (const struct_tag_typet &src) const
 
const typetfollow_tag (const c_enum_tag_typet &src) const
 
virtual unsigned get_max (const std::string &prefix) const =0
 
virtual bool lookup (const irep_idt &name, const symbolt *&symbol) const =0
 

Detailed Description

Definition at line 26 of file namespace.h.

Constructor & Destructor Documentation

§ ~namespace_baset()

namespace_baset::~namespace_baset ( )
virtual

Definition at line 39 of file namespace.cpp.

Referenced by lookup().

Member Function Documentation

§ follow()

const typet & namespace_baset::follow ( const typet src) const

Definition at line 66 of file namespace.cpp.

References irept::id(), symbolt::is_type, lookup(), and symbolt::type.

Referenced by string_abstractiont::abstract_assign(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraints(), arrayst::add_array_constraints_array_of(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), goto_program2codet::add_local_types(), add_padding(), goto_symext::address_arithmetic(), adjust_float_expressions(), c_typecheck_baset::adjust_float_rel(), alignment(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), value_sett::apply_code(), as_vcd_binary(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), smt1_convt::binary2struct(), smt1_convt::binary2union(), string_refinementt::boolbv_set_equality_to_true(), boolbvt::boolbv_set_equality_to_true(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), string_abstractiont::build_abstraction_type(), string_abstractiont::build_abstraction_type_rec(), endianness_mapt::build_big_endian(), build_class_identifier(), value_set_dereferencet::build_reference_to(), boolbvt::bv_get_rec(), c_sizeoft::c_offsetof(), smt1_convt::ce_value(), bv_refinementt::check_SAT(), value_set_analysis_fit::check_type(), value_set_analysis_fivrt::check_type(), value_set_analysis_fivrnst::check_type(), invariant_propagationt::check_type(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), arrayst::collect_arrays(), arrayst::collect_indices(), compute_pointer_offset(), goto_checkt::conversion_check(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), expr2ct::convert_array(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), boolbvt::convert_bv_typecast(), expr2ct::convert_complex(), dump_ct::convert_compound(), expr2ct::convert_constant(), smt1_convt::convert_expr(), bv_refinementt::convert_floatbv_op(), boolbvt::convert_floatbv_op(), boolbvt::convert_floatbv_typecast(), cpp_typecheck_resolvet::convert_identifier(), boolbvt::convert_index(), smt2_convt::convert_index(), expr2ct::convert_member(), smt1_convt::convert_member(), boolbvt::convert_member(), smt2_convt::convert_member(), bv_refinementt::convert_mult(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_pmop(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_rec(), expr2javat::convert_struct(), expr2cppt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), smt1_convt::convert_type(), smt2_convt::convert_type(), expr2ct::convert_typecast(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), boolbvt::convert_unary_minus(), boolbvt::convert_update_rec(), expr2ct::convert_vector(), smt1_convt::convert_with(), expr2ct::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with(), expr2ct::convert_with_precedence(), cpp_exception_list_rec(), smt2_convt::define_object_size(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_set_dereferencet::dereference_type_compare(), dereferencet::dereference_typecast(), c_typecheck_baset::designator_enter(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_array_equal(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_java_new_array(), bv_pointerst::do_postponed(), c_typecheck_baset::do_special_functions(), c_typecastt::do_typecast(), dynamic_object_upper_bound(), cpp_typecheckt::dynamic_typecast(), interpretert::evaluate_address(), path_symex_statet::expand_structs_and_arrays(), value_sett::field_sensitive(), find_superclass_with_type(), smt1_convt::find_symbols_rec(), smt2_convt::find_symbols_rec(), remove_function_pointerst::fix_argument_types(), remove_function_pointerst::fix_return_type(), smt2_convt::flatten2bv(), smt2_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), goto_checkt::float_overflow_check(), follow_tags_symbols(), gather_field_types(), c_typecheck_baset::gcc_types_compatible_p(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), goto_convertt::get_array_argument(), c_typecastt::get_c_type(), cpp_typecheckt::get_component(), get_component_rec(), remove_const_function_pointerst::get_component_value(), get_destructor(), value_set_analysis_fit::get_entries_rec(), value_set_analysis_fivrt::get_entries_rec(), value_set_analysis_fivrnst::get_entries_rec(), boolbv_widtht::get_entry(), boolbv_mapt::get_map_entry(), invariant_propagationt::get_objects_rec(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), interpretert::get_size(), get_subexpression_at_offset(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), good_pointer_def(), cpp_typecheck_resolvet::guess_template_args(), has_component_rec(), have_to_adjust_float_expressions(), have_to_rewrite_union(), cpp_typecheckt::implicit_typecast(), c_typecastt::implicit_typecast_arithmetic(), c_typecastt::implicit_typecast_followed(), c_typecheck_baset::increment_designator(), goto_symext::initialize_auto_object(), path_symex_statet::instantiate_rec(), goto_checkt::integer_overflow_check(), string_abstractiont::is_char_type(), c_typecheck_baset::is_complete_type(), is_not_zero(), path_symex_statet::is_symbol_member_index(), boolbvt::is_unbounded_array(), json(), lookup(), make_clean_pointer_cast(), cpp_typecheck_resolvet::make_constructors(), string_abstractiont::make_decl_and_def(), c_typecheck_baset::make_designator(), value_sett::make_member(), make_member_expr(), cpp_typecheckt::make_ptr_typecast(), string_abstractiont::make_type(), string_instrumentationt::make_type(), string_abstractiont::make_val_or_dummy_rec(), member_offset_expr(), value_set_dereferencet::memory_model_bytes(), object_lower_bound(), object_upper_bound(), cpp_typecheckt::operator_is_overloaded(), overflow_instrumentert::overflow_expr(), cpp_typecheckt::overloadable(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), smt2_convt::parse_rec(), pointer_offset_bits(), goto_checkt::pointer_validity_check(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), arrayst::record_array_equality(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_related(), goto_convertt::remove_assignment(), goto_convertt::remove_post(), goto_convertt::remove_pre(), cpp_typecheck_resolvet::remove_templates(), goto_symex_statet::rename(), goto_symext::replace_array_equal(), cpp_typecheck_resolvet::resolve_with_arguments(), rewrite_union(), set_class_identifier(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_member(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_offset(), size_of_expr(), c_sizeoft::sizeof_rec(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_sequence(), static_lifetime_init(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), goto_symext::symex_assign_array(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_other(), cpp_typecheckt::this_struct_type(), trace_value_binary(), boolbvt::type_conversion(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), c_typecheck_baset::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), c_typecheck_baset::typecheck_function_call_arguments(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_return(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_symbol(), goto_checkt::undefined_shift_check(), smt2_convt::unflatten(), unpack_rec(), smt2_convt::use_array_theory(), cpp_typecheckt::user_defined_conversion_sequence(), xml(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

§ follow_macros()

void namespace_baset::follow_macros ( exprt expr) const

§ follow_symbol()

§ follow_tag() [1/3]

§ follow_tag() [2/3]

const typet & namespace_baset::follow_tag ( const struct_tag_typet src) const

§ follow_tag() [3/3]

const typet & namespace_baset::follow_tag ( const c_enum_tag_typet src) const

§ get_max()

virtual unsigned namespace_baset::get_max ( const std::string &  prefix) const
pure virtual

§ lookup() [1/3]

const symbolt& namespace_baset::lookup ( const irep_idt name) const
inline

§ lookup() [2/3]

const symbolt& namespace_baset::lookup ( const irept irep) const
inline

§ lookup() [3/3]

virtual bool namespace_baset::lookup ( const irep_idt name,
const symbolt *&  symbol 
) const
pure virtual

Implemented in multi_namespacet, and namespacet.


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