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