cprover
|
dstringt has one field, an unsigned integer no which is an index into a static table of strings. More...
#include <dstring.h>
Public Member Functions | |
dstringt () | |
dstringt (const char *s) | |
dstringt (const std::string &s) | |
bool | empty () const |
char | operator[] (size_t i) const |
const char * | c_str () const |
size_t | size () const |
bool | operator< (const dstringt &b) const |
bool | operator== (const dstringt &b) const |
bool | operator!= (const dstringt &b) const |
bool | operator== (const char *b) const |
bool | operator!= (const char *b) const |
bool | operator== (const std::string &b) const |
bool | operator!= (const std::string &b) const |
bool | operator< (const std::string &b) const |
bool | operator> (const std::string &b) const |
bool | operator<= (const std::string &b) const |
bool | operator>= (const std::string &b) const |
int | compare (const dstringt &b) const |
void | clear () |
void | swap (dstringt &b) |
dstringt & | operator= (const dstringt &b) |
std::ostream & | operator<< (std::ostream &out) const |
unsigned | get_no () const |
size_t | hash () const |
Static Public Member Functions | |
static dstringt | make_from_table_index (unsigned no) |
Private Member Functions | |
dstringt (unsigned _no) | |
const std::string & | as_string () const |
Private Attributes | |
unsigned | no |
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
This makes it expensive to create a new string(because you have to look through the whole table to see if it is already there, and add it if it isn't) but very cheap to compare strings (just compare the two integers). It also means that when you have lots of copies of the same string you only have to store the whole string once, which saves space.
irep_idt
and irep_namet
are typedef-ed to dstringt in irep.h unless USE_STD_STRING
is set.
Note: Marked final to disable inheritance. No virtual destructor, so runtime-polymorphic use would be unsafe.
|
inline |
Definition at line 40 of file dstring.h.
Referenced by make_from_table_index().
|
inlineprivate |
Definition at line 163 of file dstring.h.
References string_containert::get_string(), get_string_container(), and no.
Referenced by c_str(), compare(), operator!=(), operator<(), operator<<(), operator<=(), operator==(), operator>(), operator>=(), operator[](), and size().
|
inline |
Definition at line 84 of file dstring.h.
References as_string().
Referenced by string_constraint_generatort::add_axioms_for_constrain_characters(), cpp_typecheckt::convert_anon_struct_union_member(), expr2ct::convert_overflow(), acceleration_utilst::extract_polynomial(), goto_inlinet::goto_inline_logt::output_inline_log_json(), cpp_typecheckt::put_compound_into_scope(), cpp_scopest::put_into_scope(), remove_internal_symbols(), require_goto_statements::require_declaration_of_name(), cpp_typecheck_resolvet::resolve(), java_bytecode_parsert::rinner_classes_attribute(), java_string_library_preprocesst::string_expr_of_function(), and cpp_typecheckt::typecheck_class_template().
|
inline |
Definition at line 127 of file dstring.h.
References no.
Referenced by c_storage_spect::clear(), mm_parsert::clear(), goto_tracet::clear(), and Parser::rFunctionBody().
|
inline |
Definition at line 118 of file dstring.h.
References as_string(), and no.
Referenced by irept::compare(), remove_virtual_functionst::get_functions(), remove_instanceoft::lower_instanceof(), and symbol_table_baset::show().
|
inline |
Definition at line 73 of file dstring.h.
References no.
Referenced by ansi_c_parsert::add_declarator(), string_abstractiont::add_dummy_symbol_and_value(), goto_program2codet::add_local_types(), c_typecheck_baset::apply_asm_label(), source_locationt::as_string(), ansi_c_declaratort::build(), build_function_environment(), string_abstractiont::build_new_symbol(), build_ssa_identifier_rec(), custom_bitvector_analysist::check(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), dump_ct::cleanup_type(), dump_ct::collect_typedefs_rec(), java_bytecode_convert_classt::convert(), convert(), java_bytecode_convert_methodt::convert(), expr2ct::convert_code(), expr2ct::convert_code_fence(), dump_ct::convert_compound(), dump_ct::convert_compound_declaration(), dump_ct::convert_global_variable(), expr2ct::convert_member(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), cpp_typecheckt::convert_parameter(), convert_properties_json(), expr2ct::convert_rec(), expr2cppt::convert_rec(), boolbvt::convert_symbol(), expr2ct::convert_with(), cover_basic_blockst::cover_basic_blockst(), cpp_exception_list_rec(), cpp_type2name(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbols(), goto_symext::dereference_rec(), symbolt::display_name(), value_set_fit::do_function_call(), parameter_assignmentst::do_function_calls(), linkingt::duplicate_code_symbol(), ci_lazy_methodst::entry_point_methods(), filter_out(), find_symbols(), dump_ct::gather_global_typedefs(), java_object_factoryt::gen_nondet_struct_init(), get_clinit_wrapper_body(), floatbv_typet::get_f(), get_failed_symbol(), remove_virtual_functionst::get_functions(), get_inherited_component(), fixedbv_typet::get_integer_bits(), java_bytecode_convert_methodt::get_lambda_method_symbol(), get_main_symbol(), get_mode_from_identifier(), get_nil_irep(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), value_sett::get_value_set_rec(), ci_lazy_methodst::get_virtual_method_targets(), goto_inlinet::goto_inline(), goto_program_coverage_recordt::goto_program_coverage_recordt(), ci_lazy_methodst::handle_virtual_methods_with_no_callees(), goto_program_dereferencet::has_failed_symbol(), expr2ct::id_shorthand(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), irept::is_comment(), java_build_arguments(), java_enum_static_init_unwind_handler(), json(), ui_message_handlert::json_ui_msg(), list_functions(), Parser::make_subtype(), jsil_typecheckt::make_type_compatible(), cpp_declaratort::merge_type(), move_label_ifthenelse(), cpp_scopest::new_scope(), goto_convertt::new_tmp_symbol(), custom_bitvector_domaint::object2id(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), graphml_witnesst::operator()(), dump_ct::operator()(), class_hierarchyt::operator()(), resolve_inherited_componentt::operator()(), goto_symex_statet::level0t::operator()(), goto_symex_statet::level1t::operator()(), internal_goals_filtert::operator()(), cpp_typecheckt::operator_is_overloaded(), c_storage_spect::operator|=(), Parser::optIntegralTypeOrClassSpec(), java_bytecode_parse_treet::classt::output(), change_impactt::output_instruction(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), java_bytecode_languaget::parse(), class_hierarchy_grapht::populate(), message_handlert::print(), gcc_message_handlert::print(), cpp_typecheckt::put_compound_into_scope(), cpp_scopest::put_into_scope(), cpp_convert_typet::read_function_type(), ansi_c_convert_typet::read_rec(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), goto_symex_statet::rename(), replace_location(), cpp_typecheck_resolvet::resolve_scope(), java_bytecode_parsert::rmethod_attribute(), Parser::rOperatorName(), Parser::rTypeName(), Parser::set_location(), goto_symex_statet::set_ssa_indices(), symbolt::show(), simplify_exprt::simplify_rec(), sort_and_join(), goto_symext::symex_assign_symbol(), symex_bmct::symex_step(), to_reference_type(), custom_bitvector_domaint::transform(), escape_domaint::transform(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), type2name(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_member_function(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), goto_unwindt::unwind(), jsil_typecheckt::update_expr_type(), validate_type(), value_sets_to_xml(), java_bytecode_convert_methodt::variable(), xml(), and ui_message_handlert::xml_ui_msg().
|
inline |
|
inline |
Definition at line 147 of file dstring.h.
References no.
Referenced by hash_string(), dstring_hash::operator()(), and std::hash< dstringt >::operator()().
|
inlinestatic |
Definition at line 48 of file dstring.h.
References dstringt(), and no.
|
inline |
|
inline |
Definition at line 109 of file dstring.h.
References as_string().
|
inline |
Definition at line 112 of file dstring.h.
References as_string().
|
inline |
|
inline |
Definition at line 113 of file dstring.h.
References as_string().
std::ostream & dstringt::operator<< | ( | std::ostream & | out | ) | const |
Definition at line 16 of file dstring.cpp.
References as_string().
|
inline |
Definition at line 115 of file dstring.h.
References as_string().
|
inline |
|
inline |
Definition at line 108 of file dstring.h.
References as_string().
|
inline |
Definition at line 111 of file dstring.h.
References as_string().
|
inline |
Definition at line 114 of file dstring.h.
References as_string().
|
inline |
Definition at line 116 of file dstring.h.
References as_string().
|
inline |
Definition at line 78 of file dstring.h.
References as_string().
|
inline |
Definition at line 89 of file dstring.h.
References as_string().
Referenced by actuals_replace_map(), expr2ct::convert_constant(), smt2_convt::convert_identifier(), java_bytecode_convert_methodt::convert_instructions(), cpp_typecheck_resolvet::do_builtin(), get_fresh_aux_symbol(), instantiate(), taint_analysist::instrument(), is_java_main(), patternt::operator==(), smt2_convt::parse_struct(), cpp_typecheck_resolvet::resolve(), string_constantt::set_value(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_index(), simplify_json_expr(), simplify_exprt::simplify_object_size(), and mm2cppt::text2c().
|
inline |
Definition at line 130 of file dstring.h.
References no.
Referenced by interrupt(), cpp_tokent::swap(), ansi_c_scopet::swap(), goto_tracet::swap(), irept::dt::swap(), and cpp_typecheckt::typecheck_compound_bases().
|
private |
Definition at line 160 of file dstring.h.
Referenced by as_string(), clear(), compare(), empty(), get_no(), hash(), make_from_table_index(), operator!=(), operator<(), operator=(), operator==(), and swap().