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