cprover
Loading...
Searching...
No Matches
c_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_types.h"
10
11#include "config.h"
12#include "invariant.h"
13#include "pointer_offset_size.h"
14#include "std_types.h"
15
17{
18 // same as signed size type
19 return signed_size_type();
20}
21
26
28{
30 result.set(ID_C_c_type, ID_signed_int);
31 return result;
32}
33
35{
37 result.set(ID_C_c_type, ID_signed_short_int);
38 return result;
39}
40
42{
44 result.set(ID_C_c_type, ID_unsigned_int);
45 return result;
46}
47
49{
51 result.set(ID_C_c_type, ID_unsigned_short_int);
52 return result;
53}
54
56{
57 // The size type varies. This is unsigned int on some systems,
58 // and unsigned long int on others,
59 // and unsigned long long on say Windows 64.
60
62 return unsigned_int_type();
67 else
68 INVARIANT(false, "width of size type"); // aaah!
69}
70
72{
73 // we presume this is the same as pointer difference
74 return pointer_diff_type();
75}
76
78{
80 result.set(ID_C_c_type, ID_signed_long_int);
81 return result;
82}
83
85{
87 result.set(ID_C_c_type, ID_signed_long_long_int);
88 return result;
89}
90
92{
94 result.set(ID_C_c_type, ID_unsigned_long_int);
95 return result;
96}
97
99{
101 result.set(ID_C_c_type, ID_unsigned_long_long_int);
102 return result;
103}
104
106{
108 return result;
109}
110
112{
113 // this can be signed or unsigned, depending on the architecture
114
115 // There are 3 char types, i.e., this one is
116 // different from either signed char or unsigned char!
117
119 {
121 result.set(ID_C_c_type, ID_char);
122 return std::move(result);
123 }
124 else
125 {
127 result.set(ID_C_c_type, ID_char);
128 return std::move(result);
129 }
130}
131
133{
135 result.set(ID_C_c_type, ID_unsigned_char);
136 return result;
137}
138
140{
142 result.set(ID_C_c_type, ID_signed_char);
143 return result;
144}
145
147{
149 {
151 result.set(ID_C_c_type, ID_wchar_t);
152 return std::move(result);
153 }
154 else
155 {
157 result.set(ID_C_c_type, ID_wchar_t);
158 return std::move(result);
159 }
160}
161
163{
164 // Types char16_t and char32_t denote distinct types with the same size,
165 // signedness, and alignment as uint_least16_t and uint_least32_t,
166 // respectively, in <stdint.h>, called the underlying types.
167 unsignedbv_typet result(16);
168 result.set(ID_C_c_type, ID_char16_t);
169 return result;
170}
171
173{
174 // Types char16_t and char32_t denote distinct types with the same size,
175 // signedness, and alignment as uint_least16_t and uint_least32_t,
176 // respectively, in <stdint.h>, called the underlying types.
177 unsignedbv_typet result(32);
178 result.set(ID_C_c_type, ID_char32_t);
179 return result;
180}
181
183{
184 floatbv_typet result=
186 result.set(ID_C_c_type, ID_float);
187 return result;
188}
189
191{
192 floatbv_typet result=
194 result.set(ID_C_c_type, ID_double);
195 return result;
196}
197
199{
200 floatbv_typet result;
203 else if(config.ansi_c.long_double_width==64)
205 else if(config.ansi_c.long_double_width==80)
206 {
207 // x86 extended precision has 80 bits in total, and
208 // deviating from IEEE, does not use a hidden bit.
209 // We use the closest we have got, but the below isn't accurate.
210 result=ieee_float_spect(63, 15).to_type();
211 }
212 else if(config.ansi_c.long_double_width==96)
213 {
214 result=ieee_float_spect(80, 15).to_type();
215 // not quite right. The extra bits beyond 80 are usually padded.
216 }
217 else
218 INVARIANT(false, "width of long double");
219
220 result.set(ID_C_c_type, ID_long_double);
221
222 return result;
223}
224
226{
227 // The pointer-diff type varies. This is signed int on some systems,
228 // and signed long int on others, and signed long long on say Windows.
229
231 return signed_int_type();
233 return signed_long_int_type();
236 else
237 INVARIANT(false, "width of pointer difference");
238}
239
241{
242 return pointer_typet(subtype, config.ansi_c.pointer_width);
243}
244
246{
248}
249
251{
252 static const auto result = empty_typet();
253 return result;
254}
255
256std::string c_type_as_string(const irep_idt &c_type)
257{
258 if(c_type==ID_signed_int)
259 return "signed int";
260 else if(c_type==ID_signed_short_int)
261 return "signed short int";
262 else if(c_type==ID_unsigned_int)
263 return "unsigned int";
264 else if(c_type==ID_unsigned_short_int)
265 return "unsigned short int";
266 else if(c_type==ID_signed_long_int)
267 return "signed long int";
268 else if(c_type==ID_signed_long_long_int)
269 return "signed long long int";
270 else if(c_type==ID_unsigned_long_int)
271 return "unsigned long int";
272 else if(c_type==ID_unsigned_long_long_int)
273 return "unsigned long long int";
274 else if(c_type==ID_bool)
275 return "_Bool";
276 else if(c_type==ID_char)
277 return "char";
278 else if(c_type==ID_unsigned_char)
279 return "unsigned char";
280 else if(c_type==ID_signed_char)
281 return "signed char";
282 else if(c_type==ID_wchar_t)
283 return "wchar_t";
284 else if(c_type==ID_char16_t)
285 return "char16_t";
286 else if(c_type==ID_char32_t)
287 return "char32_t";
288 else if(c_type==ID_float)
289 return "float";
290 else if(c_type==ID_double)
291 return "double";
292 else if(c_type==ID_long_double)
293 return "long double";
294 else if(c_type==ID_gcc_float128)
295 return "__float128";
296 else if(c_type==ID_unsigned_int128)
297 return "unsigned __int128";
298 else if(c_type==ID_signed_int128)
299 return "signed __int128";
300 else
301 return "";
302}
303
306{
307 const union_typet::componentst &comps = components();
308
309 optionalt<mp_integer> max_width;
310 typet max_comp_type;
311 irep_idt max_comp_name;
312
313 for(const auto &comp : comps)
314 {
315 auto element_width = pointer_offset_bits(comp.type(), ns);
316
317 if(!element_width.has_value())
318 return {};
319
320 if(max_width.has_value() && *element_width <= *max_width)
321 continue;
322
323 max_width = *element_width;
324 max_comp_type = comp.type();
325 max_comp_name = comp.get_name();
326 }
327
328 if(!max_width.has_value())
329 return {};
330 else
331 return std::make_pair(
332 struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
333}
configt config
Definition config.cpp:25
floatbv_typet float_type()
Definition c_types.cpp:182
bitvector_typet index_type()
Definition c_types.cpp:22
signedbv_typet signed_long_int_type()
Definition c_types.cpp:77
signedbv_typet signed_char_type()
Definition c_types.cpp:139
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:98
unsignedbv_typet char32_t_type()
Definition c_types.cpp:172
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:91
reference_typet reference_type(const typet &subtype)
Definition c_types.cpp:245
unsignedbv_typet size_type()
Definition c_types.cpp:55
std::string c_type_as_string(const irep_idt &c_type)
Definition c_types.cpp:256
empty_typet void_type()
Definition c_types.cpp:250
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet pointer_diff_type()
Definition c_types.cpp:225
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
signedbv_typet signed_size_type()
Definition c_types.cpp:71
bitvector_typet char_type()
Definition c_types.cpp:111
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:84
bitvector_typet wchar_t_type()
Definition c_types.cpp:146
floatbv_typet long_double_type()
Definition c_types.cpp:198
typet c_bool_type()
Definition c_types.cpp:105
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:190
signedbv_typet signed_short_int_type()
Definition c_types.cpp:34
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:48
unsignedbv_typet char16_t_type()
Definition c_types.cpp:162
Base class of fixed-width bit-vector types.
Definition std_types.h:865
The C/C++ Booleans.
Definition c_types.h:97
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_float_spect single_precision()
Definition ieee_float.h:70
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:82
class floatbv_typet to_type() const
static ieee_float_spect double_precision()
Definition ieee_float.h:76
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The reference type.
Fixed-width bit-vector with two's complement interpretation.
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The type of an expression, extends irept.
Definition type.h:29
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition c_types.cpp:305
Fixed-width bit-vector with unsigned binary interpretation.
nonstd::optional< T > optionalt
Definition optional.h:35
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Pre-defined types.
std::size_t long_double_width
Definition config.h:143
bool wchar_t_is_unsigned
Definition config.h:147
std::size_t pointer_width
Definition config.h:140
std::size_t wchar_t_width
Definition config.h:144
bool char_is_unsigned
Definition config.h:147
std::size_t bool_width
Definition config.h:136
std::size_t long_long_int_width
Definition config.h:139
std::size_t long_int_width
Definition config.h:135
std::size_t short_int_width
Definition config.h:138
std::size_t char_width
Definition config.h:137
std::size_t int_width
Definition config.h:134