CBMC
Loading...
Searching...
No Matches
dstring.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Container for C-Strings
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_DSTRING_H
13#define CPROVER_UTIL_DSTRING_H
14
15#include <iosfwd>
16#include <string>
17
18#include "magic.h"
19#include "string_container.h"
20
21template <typename T>
23
37class dstringt final
38{
39public:
40 // this is safe for static objects
41 #ifdef __GNUC__
42 constexpr
43 #endif
45 {
46 }
47
48 // this is safe for static objects
49 #ifdef __GNUC__
50 constexpr
51 #endif
53 {
54 return dstringt(no);
55 }
56
57 #if 0
58 // This conversion allows the use of dstrings
59 // in switch ... case statements.
60 constexpr operator int() const { return no; }
61 #endif
62
63 // this one is not safe for static objects
64 // NOLINTNEXTLINE(runtime/explicit)
65 dstringt(const char *s):no(get_string_container()[s])
66 {
67 }
68
69 // this one is not safe for static objects
70 // NOLINTNEXTLINE(runtime/explicit)
71 dstringt(const std::string &s):no(get_string_container()[s])
72 {
73 }
74
75 dstringt(const dstringt &) = default;
76
79#ifdef __GNUC__
80 constexpr
81#endif
83 : no(other.no)
84 {
85 }
86
87 // access
88
89 bool empty() const
90 {
91 return no==0; // string 0 is exactly the empty string
92 }
93
95 bool starts_with(const char *s) const
96 {
97 for(const char *t = c_str(); *s != 0; s++, t++)
98 if(*t != *s)
99 return false;
100
101 return true;
102 }
103
105 bool starts_with(const std::string &prefix) const
106 {
107 return as_string().compare(0, prefix.size(), prefix) == 0;
108 }
109
110 char operator[](size_t i) const
111 {
112 return as_string()[i];
113 }
114
115 // the pointer is guaranteed to be stable
116 const char *c_str() const
117 {
118 return as_string().c_str();
119 }
120
121 size_t size() const
122 {
123 return as_string().size();
124 }
125
126 // ordering -- not the same as lexicographical ordering
127
128 bool operator< (const dstringt &b) const { return no<b.no; }
129
130 // comparison with same type
131
132 bool operator==(const dstringt &b) const
133 { return no==b.no; } // really fast equality testing
134
135 bool operator!=(const dstringt &b) const
136 { return no!=b.no; } // really fast equality testing
137
138 // comparison with other types
139
140 bool operator==(const char *b) const { return as_string()==b; }
141 bool operator!=(const char *b) const { return as_string()!=b; }
142
143 bool operator==(const std::string &b) const { return as_string()==b; }
144 bool operator!=(const std::string &b) const { return as_string()!=b; }
145 bool operator<(const std::string &b) const { return as_string()<b; }
146 bool operator>(const std::string &b) const { return as_string()>b; }
147 bool operator<=(const std::string &b) const { return as_string()<=b; }
148 bool operator>=(const std::string &b) const { return as_string()>=b; }
149
150 int compare(const dstringt &b) const
151 {
152 if(no==b.no)
153 return 0; // equal
154 return as_string().compare(b.as_string());
155 }
156
157 // modifying
158
159 void clear()
160 { no=0; }
161
163 { unsigned t=no; no=b.no; b.no=t; }
164
166 { no=b.no; return *this; }
167
171 {
172 no = other.no;
173 return *this;
174 }
175
176 // output
177
178 std::ostream &operator<<(std::ostream &out) const;
179
180 // non-standard
181
182 unsigned get_no() const
183 {
184 return no;
185 }
186
187 size_t hash() const
188 {
189 return no;
190 }
191
192 // iterators for the underlying string
193 std::string::const_iterator begin() const
194 {
195 return as_string().begin();
196 }
197
198 std::string::const_iterator end() const
199 {
200 return as_string().end();
201 }
202
203private:
204 #ifdef __GNUC__
205 constexpr
206 #endif
207 explicit dstringt(unsigned _no):no(_no)
208 {
209 }
210
211 unsigned no;
212
213 // the reference returned is guaranteed to be stable
214 const std::string &as_string() const
215 { return get_string_container().get_string(no); }
216};
217
218// the reference returned is guaranteed to be stable
219inline const std::string &as_string(const dstringt &s)
220{ return get_string_container().get_string(s.get_no()); }
221
222// NOLINTNEXTLINE(readability/identifiers)
224{
225 size_t operator()(const dstringt &s) const { return s.hash(); }
226};
227
228inline size_t hash_string(const dstringt &s)
229{
230 return s.hash();
231}
232
233inline std::ostream &operator<<(std::ostream &out, const dstringt &a)
234{
235 return a.operator<<(out);
236}
237
238// NOLINTNEXTLINE [allow specialisation within 'std']
239namespace std
240{
242template <>
243struct hash<dstringt> // NOLINT(readability/identifiers)
244{
245 size_t operator()(const dstringt &dstring) const
246 {
247 return dstring.hash();
248 }
249};
250}
251
252template <>
254{
255 static std::string diagnostics_as_string(const dstringt &dstring)
256 {
257 return as_string(dstring);
258 }
259};
260
261dstringt get_dstring_number(std::size_t);
262
265template <typename T>
266static inline
267 typename std::enable_if<std::is_integral<T>::value, dstringt>::type
268 to_dstring(T value)
269{
270 if(value >= 0 && value <= static_cast<T>(DSTRING_NUMBERS_MAX))
271 return get_dstring_number(value);
272 else
273 return std::to_string(value);
274}
275
276#endif // CPROVER_UTIL_DSTRING_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool operator!=(const char *b) const
Definition dstring.h:141
const std::string & as_string() const
Definition dstring.h:214
bool operator<(const dstringt &b) const
Definition dstring.h:128
dstringt(unsigned _no)
Definition dstring.h:207
dstringt(const std::string &s)
Definition dstring.h:71
void swap(dstringt &b)
Definition dstring.h:162
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool operator!=(const std::string &b) const
Definition dstring.h:144
bool starts_with(const std::string &prefix) const
equivalent of as_string().starts_with(s)
Definition dstring.h:105
dstringt(const char *s)
Definition dstring.h:65
dstringt(const dstringt &)=default
bool empty() const
Definition dstring.h:89
bool operator<(const std::string &b) const
Definition dstring.h:145
dstringt & operator=(const dstringt &b)
Definition dstring.h:165
bool operator<=(const std::string &b) const
Definition dstring.h:147
void clear()
Definition dstring.h:159
static dstringt make_from_table_index(unsigned no)
Definition dstring.h:52
bool operator==(const char *b) const
Definition dstring.h:140
bool operator!=(const dstringt &b) const
Definition dstring.h:135
int compare(const dstringt &b) const
Definition dstring.h:150
std::string::const_iterator end() const
Definition dstring.h:198
std::ostream & operator<<(std::ostream &out) const
Definition dstring.cpp:16
const char * c_str() const
Definition dstring.h:116
bool operator==(const dstringt &b) const
Definition dstring.h:132
size_t size() const
Definition dstring.h:121
size_t hash() const
Definition dstring.h:187
unsigned get_no() const
Definition dstring.h:182
std::string::const_iterator begin() const
Definition dstring.h:193
dstringt(dstringt &&other)
Move constructor.
Definition dstring.h:82
char operator[](size_t i) const
Definition dstring.h:110
bool operator==(const std::string &b) const
Definition dstring.h:143
dstringt()
Definition dstring.h:44
bool operator>=(const std::string &b) const
Definition dstring.h:148
unsigned no
Definition dstring.h:211
bool operator>(const std::string &b) const
Definition dstring.h:146
dstringt & operator=(dstringt &&other)
Move assignment.
Definition dstring.h:170
const std::string & get_string(size_t no) const
size_t hash_string(const dstringt &s)
Definition dstring.h:228
dstringt get_dstring_number(std::size_t)
Definition dstring.cpp:21
const std::string & as_string(const dstringt &s)
Definition dstring.h:219
std::ostream & operator<<(std::ostream &out, const dstringt &a)
Definition dstring.h:233
static std::enable_if< std::is_integral< T >::value, dstringt >::type to_dstring(T value)
equivalent to dstringt(std::to_string(value)), i.e., produces a string from a number
Definition dstring.h:268
Magic numbers used throughout the codebase.
constexpr std::size_t DSTRING_NUMBERS_MAX
Definition magic.h:17
STL namespace.
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.
static std::string diagnostics_as_string(const dstringt &dstring)
Definition dstring.h:255
Helper to give us some diagnostic in a usable form on assertion failure.
Definition invariant.h:299
size_t operator()(const dstringt &s) const
Definition dstring.h:225
size_t operator()(const dstringt &dstring) const
Definition dstring.h:245