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 is typedef-ed to dstringt in irep.h.

Note: Marked final to disable inheritance. No virtual destructor, so runtime-polymorphic use would be unsafe.

Definition at line 37 of file dstring.h.

Constructor & Destructor Documentation

◆ dstringt() [1/7]

dstringt::dstringt ( )

inline

Definition at line 44 of file dstring.h.

◆ dstringt() [2/7]

dstringt::dstringt ( const char * s )

inline

Definition at line 71 of file dstring.h.

◆ dstringt() [3/7]

dstringt::dstringt ( std::string_view s )

inline

Definition at line 77 of file dstring.h.

◆ dstringt() [4/7]

dstringt::dstringt ( const std::string & s )

inline

Definition at line 83 of file dstring.h.

◆ dstringt() [5/7]

dstringt::dstringt ( const dstringt & )

default

◆ dstringt() [6/7]

dstringt::dstringt ( dstringt && other )

inline

Move constructor.

There is no need and no point in actually destroying the source object other, this is effectively just a copy constructor.

Definition at line 94 of file dstring.h.

◆ dstringt() [7/7]

dstringt::dstringt ( unsigned _no )

inlineexplicitprivate

Definition at line 219 of file dstring.h.

Member Function Documentation

◆ as_string()

const std::string & dstringt::as_string ( ) const

inlineprivate

Definition at line 226 of file dstring.h.

◆ begin()

std::string::const_iterator dstringt::begin ( ) const

inline

Definition at line 205 of file dstring.h.

◆ c_str()

const char * dstringt::c_str ( ) const

inline

Definition at line 128 of file dstring.h.

◆ clear()

void dstringt::clear ( )

inline

Definition at line 171 of file dstring.h.

◆ compare()

int dstringt::compare ( const dstringt & b ) const

inline

Definition at line 162 of file dstring.h.

◆ empty()

bool dstringt::empty ( ) const

inline

Definition at line 101 of file dstring.h.

◆ end()

std::string::const_iterator dstringt::end ( ) const

inline

Definition at line 210 of file dstring.h.

◆ get_no()

unsigned dstringt::get_no ( ) const

inline

Definition at line 194 of file dstring.h.

◆ hash()

size_t dstringt::hash ( ) const

inline

Definition at line 199 of file dstring.h.

◆ make_from_table_index()

static dstringt dstringt::make_from_table_index ( unsigned no )

inlinestatic

Definition at line 52 of file dstring.h.

◆ operator!=() [1/3]

bool dstringt::operator!= ( const char * b ) const

inline

Definition at line 153 of file dstring.h.

◆ operator!=() [2/3]

bool dstringt::operator!= ( const dstringt & b ) const

inline

Definition at line 147 of file dstring.h.

◆ operator!=() [3/3]

bool dstringt::operator!= ( const std::string & b ) const

inline

Definition at line 156 of file dstring.h.

◆ operator<() [1/2]

bool dstringt::operator< ( const dstringt & b ) const

inline

Definition at line 140 of file dstring.h.

◆ operator<() [2/2]

bool dstringt::operator< ( const std::string & b ) const

inline

Definition at line 157 of file dstring.h.

◆ operator<<()

std::ostream & dstringt::operator<< ( std::ostream & out ) const

Definition at line 16 of file dstring.cpp.

◆ operator<=()

bool dstringt::operator<= ( const std::string & b ) const

inline

Definition at line 159 of file dstring.h.

◆ operator=() [1/2]

dstringt & dstringt::operator= ( const dstringt & b )

inline

Definition at line 177 of file dstring.h.

◆ operator=() [2/2]

dstringt & dstringt::operator= ( dstringt && other )

inline

Move assignment.

There is no need and no point in actually destroying the source object other, this is effectively just an assignment.

Definition at line 182 of file dstring.h.

◆ operator==() [1/3]

bool dstringt::operator== ( const char * b ) const

inline

Definition at line 152 of file dstring.h.

◆ operator==() [2/3]

bool dstringt::operator== ( const dstringt & b ) const

inline

Definition at line 144 of file dstring.h.

◆ operator==() [3/3]

bool dstringt::operator== ( const std::string & b ) const

inline

Definition at line 155 of file dstring.h.

◆ operator>()

bool dstringt::operator> ( const std::string & b ) const

inline

Definition at line 158 of file dstring.h.

◆ operator>=()

bool dstringt::operator>= ( const std::string & b ) const

inline

Definition at line 160 of file dstring.h.

◆ operator[]()

char dstringt::operator[] ( size_t i ) const

inline

Definition at line 122 of file dstring.h.

◆ size()

size_t dstringt::size ( ) const

inline

Definition at line 133 of file dstring.h.

◆ starts_with() [1/2]

bool dstringt::starts_with ( const char * s ) const

inline

equivalent of as_string().starts_with(s)

Definition at line 107 of file dstring.h.

◆ starts_with() [2/2]

bool dstringt::starts_with ( std::string_view prefix ) const

inline

equivalent of as_string().starts_with(s)

Definition at line 117 of file dstring.h.

◆ swap()

void dstringt::swap ( dstringt & b )

inline

Definition at line 174 of file dstring.h.

Member Data Documentation

◆ no

unsigned dstringt::no

private

Definition at line 223 of file dstring.h.

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

/home/runner/work/cbmc/cbmc/src/util/dstring.h
/home/runner/work/cbmc/cbmc/src/util/dstring.cpp