CBMC: /home/runner/work/cbmc/cbmc/src/util/dstring.h Source File

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>
22struct diagnostics_helpert;
23
37 class 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 // The const char* and const std::string& constructors below are
64 // semantically equivalent to the std::string_view one (both implicitly
65 // convert to std::string_view); they are retained only so that overload
66 // resolution prefers them and avoids an extra conversion, not for any
67 // distinct behaviour.
68
69 // this one is not safe for static objects
70 // NOLINTNEXTLINE(runtime/explicit)
71 dstringt(const char *s):no(get_string_container()[s])
72 {
73 }
74
75 // this one is not safe for static objects
76 // NOLINTNEXTLINE(runtime/explicit)
77 dstringt(std::string_view s) : no(get_string_container()[s])
78 {
79 }
80
81 // this one is not safe for static objects
82 // NOLINTNEXTLINE(runtime/explicit)
83 dstringt(const std::string &s):no(get_string_container()[s])
84 {
85 }
86
87 dstringt(const dstringt &) = default;
88
91#ifdef __GNUC__
92 constexpr
93#endif
95 : no(other.no)
96 {
97 }
98
99 // access
100
101 bool empty() const
102{
103 return no==0; // string 0 is exactly the empty string
104 }
105
107 bool starts_with(const char *s) const
108{
109 for(const char *t = c_str(); *s != 0; s++, t++)
110 if(*t != *s)
111 return false;
112
113 return true;
114 }
115
117 bool starts_with(std::string_view prefix) const
118{
119 return as_string().compare(0, prefix.size(), prefix) == 0;
120 }
121
122 char operator[](size_t i) const
123{
124 return as_string()[i];
125 }
126
127 // the pointer is guaranteed to be stable
128 const char *c_str() const
129{
130 return as_string().c_str();
131 }
132
133 size_t size() const
134{
135 return as_string().size();
136 }
137
138 // ordering -- not the same as lexicographical ordering
139
140 bool operator< (const dstringt &b) const { return no<b.no; }
141
142 // comparison with same type
143
144 bool operator==(const dstringt &b) const
145{ return no==b.no; } // really fast equality testing
146
147 bool operator!=(const dstringt &b) const
148{ return no!=b.no; } // really fast equality testing
149
150 // comparison with other types
151
152 bool operator==(const char *b) const { return as_string()==b; }
153 bool operator!=(const char *b) const { return as_string()!=b; }
154
155 bool operator==(const std::string &b) const { return as_string()==b; }
156 bool operator!=(const std::string &b) const { return as_string()!=b; }
157 bool operator<(const std::string &b) const { return as_string()<b; }
158 bool operator>(const std::string &b) const { return as_string()>b; }
159 bool operator<=(const std::string &b) const { return as_string()<=b; }
160 bool operator>=(const std::string &b) const { return as_string()>=b; }
161
162 int compare(const dstringt &b) const
163{
164 if(no==b.no)
165 return 0; // equal
166 return as_string().compare(b.as_string());
167 }
168
169 // modifying
170
171 void clear()
172 { no=0; }
173
175 { unsigned t=no; no=b.no; b.no=t; }
176
178 { no=b.no; return *this; }
179
183 {
184 no = other.no;
185 return *this;
186 }
187
188 // output
189
190 std::ostream &operator<<(std::ostream &out) const;
191
192 // non-standard
193
194 unsigned get_no() const
195{
196 return no;
197 }
198
199 size_t hash() const
200{
201 return no;
202 }
203
204 // iterators for the underlying string
205 std::string::const_iterator begin() const
206{
207 return as_string().begin();
208 }
209
210 std::string::const_iterator end() const
211{
212 return as_string().end();
213 }
214
215private:
216 #ifdef __GNUC__
217 constexpr
218 #endif
219 explicit dstringt(unsigned _no):no(_no)
220 {
221 }
222
223 unsigned no;
224
225 // the reference returned is guaranteed to be stable
226 const std::string &as_string() const
228};
229
230// the reference returned is guaranteed to be stable
231 inline const std::string &as_string(const dstringt &s)
232{ return get_string_container().get_string(s.get_no()); }
233
234// NOLINTNEXTLINE(readability/identifiers)
236{
237 size_t operator()(const dstringt &s) const { return s.hash(); }
238};
239
240 inline size_t hash_string(const dstringt &s)
241{
242 return s.hash();
243}
244
245 inline std::ostream &operator<<(std::ostream &out, const dstringt &a)
246{
247 return a.operator<<(out);
248}
249
250// NOLINTNEXTLINE [allow specialisation within 'std']
251namespace std
252{
254template <>
255 struct hash<dstringt> // NOLINT(readability/identifiers)
256{
257 size_t operator()(const dstringt &dstring) const
258{
259 return dstring.hash();
260 }
261};
262}
263
264template <>
266{
267 static std::string diagnostics_as_string(const dstringt &dstring)
268 {
269 return as_string(dstring);
270 }
271};
272
273dstringt get_dstring_number(std::size_t);
274
277template <typename T>
278static inline
279 typename std::enable_if<std::is_integral<T>::value, dstringt>::type
280 to_dstring(T value)
281{
282 if(value >= 0 && value <= static_cast<T>(DSTRING_NUMBERS_MAX))
283 return get_dstring_number(value);
284 else
285 return std::to_string(value);
286}
287
288#endif // CPROVER_UTIL_DSTRING_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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:153
const std::string & as_string() const
Definition dstring.h:226
bool operator<(const dstringt &b) const
Definition dstring.h:140
dstringt(unsigned _no)
Definition dstring.h:219
dstringt(const std::string &s)
Definition dstring.h:83
void swap(dstringt &b)
Definition dstring.h:174
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:107
bool operator!=(const std::string &b) const
Definition dstring.h:156
bool starts_with(std::string_view prefix) const
equivalent of as_string().starts_with(s)
Definition dstring.h:117
dstringt(const char *s)
Definition dstring.h:71
dstringt(const dstringt &)=default
bool empty() const
Definition dstring.h:101
bool operator<(const std::string &b) const
Definition dstring.h:157
dstringt & operator=(const dstringt &b)
Definition dstring.h:177
bool operator<=(const std::string &b) const
Definition dstring.h:159
void clear()
Definition dstring.h:171
dstringt(std::string_view s)
Definition dstring.h:77
static dstringt make_from_table_index(unsigned no)
Definition dstring.h:52
bool operator==(const char *b) const
Definition dstring.h:152
bool operator!=(const dstringt &b) const
Definition dstring.h:147
int compare(const dstringt &b) const
Definition dstring.h:162
std::string::const_iterator end() const
Definition dstring.h:210
std::ostream & operator<<(std::ostream &out) const
Definition dstring.cpp:16
const char * c_str() const
Definition dstring.h:128
bool operator==(const dstringt &b) const
Definition dstring.h:144
size_t size() const
Definition dstring.h:133
size_t hash() const
Definition dstring.h:199
unsigned get_no() const
Definition dstring.h:194
std::string::const_iterator begin() const
Definition dstring.h:205
dstringt(dstringt &&other)
Move constructor.
Definition dstring.h:94
char operator[](size_t i) const
Definition dstring.h:122
bool operator==(const std::string &b) const
Definition dstring.h:155
dstringt()
Definition dstring.h:44
bool operator>=(const std::string &b) const
Definition dstring.h:160
unsigned no
Definition dstring.h:223
bool operator>(const std::string &b) const
Definition dstring.h:158
dstringt & operator=(dstringt &&other)
Move assignment.
Definition dstring.h:182
const std::string & get_string(size_t no) const
size_t hash_string(const dstringt &s)
Definition dstring.h:240
dstringt get_dstring_number(std::size_t)
Definition dstring.cpp:21
const std::string & as_string(const dstringt &s)
Definition dstring.h:231
std::ostream & operator<<(std::ostream &out, const dstringt &a)
Definition dstring.h:245
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:280
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:267
Helper to give us some diagnostic in a usable form on assertion failure.
Definition invariant.h:299
Definition dstring.h:236
size_t operator()(const dstringt &s) const
Definition dstring.h:237
size_t operator()(const dstringt &dstring) const
Definition dstring.h:257

AltStyle によって変換されたページ (->オリジナル) /