cprover
|
#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 |
|
inline |
Definition at line 28 of file dstring.h.
Referenced by make_from_table_index().
|
inlineprivate |
Definition at line 154 of file dstring.h.
References string_containert::get_string(), no, and string_container.
Referenced by c_str(), compare(), operator!=(), operator<(), operator<<(), operator<=(), operator==(), operator>(), operator>=(), operator[](), and size().
|
inline |
Definition at line 72 of file dstring.h.
References as_string().
Referenced by cpp_typecheckt::convert_anon_struct_union_member(), expr2ct::convert_overflow(), acceleration_utilst::extract_polynomial(), polynomialt::from_expr(), goto_inlinet::goto_inline_logt::output_inline_log_json(), cpp_typecheckt::put_compound_into_scope(), cpp_scopest::put_into_scope(), remove_internal_symbols(), cpp_typecheck_resolvet::resolve(), and cpp_typecheckt::typecheck_class_template().
|
inline |
Definition at line 115 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 106 of file dstring.h.
References as_string(), and no.
Referenced by irept::compare().
|
inline |
Definition at line 61 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(), convert(), value_set_analysist::convert(), java_bytecode_convert_classt::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(), cpp_typecheckt::convert_parameter(), expr2ct::convert_rec(), expr2cppt::convert_rec(), string_refinementt::convert_symbol(), boolbvt::convert_symbol(), expr2ct::convert_with(), cpp_exception_list_rec(), cpp_type2name(), symbolt::display_name(), java_bytecode_languaget::do_ci_lazy_method_conversion(), value_set_fit::do_function_call(), parameter_assignmentst::do_function_calls(), path_searcht::drop_state(), linkingt::duplicate_code_symbol(), filter_out(), find_symbols(), path_symext::function_call_rec(), dump_ct::gather_global_typedefs(), java_object_factoryt::gen_nondet_struct_init(), floatbv_typet::get_f(), get_failed_symbol(), remove_virtual_functionst::get_functions(), fixedbv_typet::get_integer_bits(), get_main_symbol(), get_nil_irep(), goto_inlinet::goto_inline(), goto_program_coverage_recordt::goto_program_coverage_recordt(), goto_program_dereferencet::has_failed_symbol(), expr2ct::id_shorthand(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), instrument_cover_goals(), irept::is_comment(), java_build_arguments(), json(), ui_message_handlert::json_ui_msg(), Parser::make_subtype(), jsil_typecheckt::make_type_compatible(), cpp_declaratort::merge_type(), move_label_ifthenelse(), cpp_scopest::new_scope(), custom_bitvector_domaint::object2id(), graphml_witnesst::operator()(), class_hierarchyt::operator()(), dump_ct::operator()(), var_mapt::operator()(), goto_symex_statet::level0t::operator()(), goto_symex_statet::level1t::operator()(), cpp_typecheckt::operator_is_overloaded(), c_storage_spect::operator|=(), Parser::optIntegralTypeOrClassSpec(), change_impactt::output_instruction(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), java_bytecode_languaget::parse(), message_handlert::print(), gcc_message_handlert::print(), cpp_typecheckt::put_compound_into_scope(), cpp_scopest::put_into_scope(), cpp_convert_typet::read_function_type(), path_symex_statet::read_symbol_member_index(), 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::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(), 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(), cpp_typecheckt::typecheck_type(), goto_unwindt::unwind(), jsil_typecheckt::update_expr_type(), java_bytecode_convert_methodt::variable(), xml(), and ui_message_handlert::xml_ui_msg().
|
inline |
|
inline |
Definition at line 138 of file dstring.h.
References no.
Referenced by hash_string(), and dstring_hash::operator()().
|
inlinestatic |
Definition at line 36 of file dstring.h.
References dstringt(), and no.
|
inline |
|
inline |
Definition at line 97 of file dstring.h.
References as_string().
|
inline |
Definition at line 100 of file dstring.h.
References as_string().
|
inline |
|
inline |
Definition at line 101 of file dstring.h.
References as_string().
|
inline |
Definition at line 126 of file dstring.h.
References as_string().
|
inline |
Definition at line 103 of file dstring.h.
References as_string().
|
inline |
|
inline |
Definition at line 96 of file dstring.h.
References as_string().
|
inline |
Definition at line 99 of file dstring.h.
References as_string().
|
inline |
Definition at line 102 of file dstring.h.
References as_string().
|
inline |
Definition at line 104 of file dstring.h.
References as_string().
|
inline |
Definition at line 66 of file dstring.h.
References as_string().
|
inline |
Definition at line 77 of file dstring.h.
References as_string().
Referenced by expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), smt2_convt::convert_identifier(), java_bytecode_convert_methodt::convert_instructions(), cpp_typecheck_resolvet::do_builtin(), taint_analysist::instrument(), java_build_arguments(), 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_exprt::simplify_object_size(), and mm2cppt::text2c().
|
inline |
Definition at line 118 of file dstring.h.
References no.
Referenced by cpp_tokent::swap(), ansi_c_scopet::swap(), goto_tracet::swap(), java_bytecode_parse_treet::classt::swap(), irept::dt::swap(), and cpp_typecheckt::typecheck_compound_bases().
|
private |
Definition at line 151 of file dstring.h.
Referenced by as_string(), clear(), compare(), empty(), get_no(), hash(), make_from_table_index(), operator!=(), operator<(), operator=(), operator==(), and swap().