CBMC
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
23{
24 signedbv_typet result(config.ansi_c.int_width);
26 return result;
27}
28
30{
31 signedbv_typet result(config.ansi_c.short_int_width);
33 return result;
34}
35
37{
38 unsignedbv_typet result(config.ansi_c.int_width);
40 return result;
41}
42
44{
45 unsignedbv_typet result(config.ansi_c.short_int_width);
47 return result;
48}
49
51{
52 // The size type varies. This is unsigned int on some systems,
53 // and unsigned long int on others,
54 // and unsigned long long on say Windows 64.
55
56 if(config.ansi_c.pointer_width==config.ansi_c.int_width)
57 return unsigned_int_type();
58 else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
60 else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
62 else
63 INVARIANT(false, "width of size type"); // aaah!
64}
65
67{
68 // we presume this is the same as pointer difference
69 return pointer_diff_type();
70}
71
73{
74 signedbv_typet result(config.ansi_c.long_int_width);
76 return result;
77}
78
80{
81 signedbv_typet result(config.ansi_c.long_long_int_width);
83 return result;
84}
85
87{
88 unsignedbv_typet result(config.ansi_c.long_int_width);
90 return result;
91}
92
94{
95 unsignedbv_typet result(config.ansi_c.long_long_int_width);
97 return result;
98}
99
101{
102 typet result=c_bool_typet(config.ansi_c.bool_width);
103 return result;
104}
105
107{
108 // this can be signed or unsigned, depending on the architecture
109
110 // There are 3 char types, i.e., this one is
111 // different from either signed char or unsigned char!
112
113 if(config.ansi_c.char_is_unsigned)
114 {
115 unsignedbv_typet result(config.ansi_c.char_width);
116 result.set(ID_C_c_type, ID_char);
117 return std::move(result);
118 }
119 else
120 {
121 signedbv_typet result(config.ansi_c.char_width);
122 result.set(ID_C_c_type, ID_char);
123 return std::move(result);
124 }
125}
126
128{
129 unsignedbv_typet result(config.ansi_c.char_width);
131 return result;
132}
133
135{
136 signedbv_typet result(config.ansi_c.char_width);
138 return result;
139}
140
142{
143 if(config.ansi_c.wchar_t_is_unsigned)
144 {
145 unsignedbv_typet result(config.ansi_c.wchar_t_width);
146 result.set(ID_C_c_type, ID_wchar_t);
147 return std::move(result);
148 }
149 else
150 {
151 signedbv_typet result(config.ansi_c.wchar_t_width);
152 result.set(ID_C_c_type, ID_wchar_t);
153 return std::move(result);
154 }
155}
156
158{
159 // Types char16_t and char32_t denote distinct types with the same size,
160 // signedness, and alignment as uint_least16_t and uint_least32_t,
161 // respectively, in <stdint.h>, called the underlying types.
162 unsignedbv_typet result(16);
163 result.set(ID_C_c_type, ID_char16_t);
164 return result;
165}
166
168{
169 // Types char16_t and char32_t denote distinct types with the same size,
170 // signedness, and alignment as uint_least16_t and uint_least32_t,
171 // respectively, in <stdint.h>, called the underlying types.
172 unsignedbv_typet result(32);
173 result.set(ID_C_c_type, ID_char32_t);
174 return result;
175}
176
178{
179 floatbv_typet result=
181 result.set(ID_C_c_type, ID_float);
182 return result;
183}
184
186{
187 floatbv_typet result=
189 result.set(ID_C_c_type, ID_double);
190 return result;
191}
192
194{
195 floatbv_typet result;
196 if(config.ansi_c.long_double_width==128)
197 result=ieee_float_spect::quadruple_precision().to_type();
198 else if(config.ansi_c.long_double_width==64)
199 result=ieee_float_spect::double_precision().to_type();
200 else if(config.ansi_c.long_double_width==80)
201 {
202 // x86 extended precision has 80 bits in total, and
203 // deviating from IEEE, does not use a hidden bit.
204 // We use the closest we have got, but the below isn't accurate.
205 result=ieee_float_spect(63, 15).to_type();
206 }
207 else if(config.ansi_c.long_double_width==96)
208 {
209 result=ieee_float_spect(80, 15).to_type();
210 // not quite right. The extra bits beyond 80 are usually padded.
211 }
212 else
213 INVARIANT(false, "width of long double");
214
216
217 return result;
218}
219
221{
222 // The pointer-diff type varies. This is signed int on some systems,
223 // and signed long int on others, and signed long long on say Windows.
224
225 if(config.ansi_c.pointer_width==config.ansi_c.int_width)
226 return signed_int_type();
227 else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
228 return signed_long_int_type();
229 else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
231 else
232 INVARIANT(false, "width of pointer difference");
233}
234
236{
237 return pointer_typet(subtype, config.ansi_c.pointer_width);
238}
239
241{
242 return reference_typet(subtype, config.ansi_c.pointer_width);
243}
244
246{
247 static const auto result = empty_typet();
248 return result;
249}
250
252{
254 return "signed int";
256 return "signed short int";
257 else if(c_type==ID_unsigned_int)
258 return "unsigned int";
260 return "unsigned short int";
261 else if(c_type==ID_signed_long_int)
262 return "signed long int";
264 return "signed long long int";
266 return "unsigned long int";
268 return "unsigned long long int";
269 else if(c_type==ID_bool)
270 return "_Bool";
271 else if(c_type==ID_char)
272 return "char";
273 else if(c_type==ID_unsigned_char)
274 return "unsigned char";
275 else if(c_type==ID_signed_char)
276 return "signed char";
277 else if(c_type==ID_wchar_t)
278 return "wchar_t";
279 else if(c_type==ID_char16_t)
280 return "char16_t";
281 else if(c_type==ID_char32_t)
282 return "char32_t";
283 else if(c_type==ID_float)
284 return "float";
285 else if(c_type==ID_double)
286 return "double";
287 else if(c_type==ID_long_double)
288 return "long double";
289 else if(c_type==ID_gcc_float128)
290 return "__float128";
291 else if(c_type==ID_unsigned_int128)
292 return "unsigned __int128";
293 else if(c_type==ID_signed_int128)
294 return "signed __int128";
295 else
296 return "";
297}
298
299std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
301{
303
304 std::optional<mp_integer> max_width;
307
308 for(const auto &comp : comps)
309 {
310 auto element_width = pointer_offset_bits(comp.type(), ns);
311
312 if(!element_width.has_value())
313 return {};
314
315 if(max_width.has_value() && *element_width <= *max_width)
316 continue;
317
319 max_comp_type = comp.type();
320 max_comp_name = comp.get_name();
321 }
322
323 if(!max_width.has_value())
324 return {};
325 else
326 return std::make_pair(
328}
configt config
Definition config.cpp:25
floatbv_typet float_type()
Definition c_types.cpp:177
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
signedbv_typet signed_char_type()
Definition c_types.cpp:134
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:93
unsignedbv_typet char32_t_type()
Definition c_types.cpp:167
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
reference_typet reference_type(const typet &subtype)
Definition c_types.cpp:240
unsignedbv_typet size_type()
Definition c_types.cpp:50
std::string c_type_as_string(const irep_idt &c_type)
Definition c_types.cpp:251
empty_typet void_type()
Definition c_types.cpp:245
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:127
signedbv_typet signed_size_type()
Definition c_types.cpp:66
bitvector_typet char_type()
Definition c_types.cpp:106
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
bitvector_typet wchar_t_type()
Definition c_types.cpp:141
floatbv_typet long_double_type()
Definition c_types.cpp:193
typet c_bool_type()
Definition c_types.cpp:100
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:185
signedbv_typet signed_short_int_type()
Definition c_types.cpp:29
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:43
unsignedbv_typet char16_t_type()
Definition c_types.cpp:157
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class of fixed-width bit-vector types.
Definition std_types.h:909
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:38
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:412
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
std::optional< 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:300
Fixed-width bit-vector with unsigned binary interpretation.
std::optional< 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.