CBMC
c_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 {
25  result.set(ID_C_c_type, ID_signed_int);
26  return result;
27 }
28 
30 {
32  result.set(ID_C_c_type, ID_signed_short_int);
33  return result;
34 }
35 
37 {
39  result.set(ID_C_c_type, ID_unsigned_int);
40  return result;
41 }
42 
44 {
46  result.set(ID_C_c_type, ID_unsigned_short_int);
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 
57  return unsigned_int_type();
59  return unsigned_long_int_type();
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 {
75  result.set(ID_C_c_type, ID_signed_long_int);
76  return result;
77 }
78 
80 {
82  result.set(ID_C_c_type, ID_signed_long_long_int);
83  return result;
84 }
85 
87 {
89  result.set(ID_C_c_type, ID_unsigned_long_int);
90  return result;
91 }
92 
94 {
96  result.set(ID_C_c_type, ID_unsigned_long_long_int);
97  return result;
98 }
99 
101 {
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 
114  {
116  result.set(ID_C_c_type, ID_char);
117  return std::move(result);
118  }
119  else
120  {
122  result.set(ID_C_c_type, ID_char);
123  return std::move(result);
124  }
125 }
126 
128 {
130  result.set(ID_C_c_type, ID_unsigned_char);
131  return result;
132 }
133 
135 {
137  result.set(ID_C_c_type, ID_signed_char);
138  return result;
139 }
140 
142 {
144  {
146  result.set(ID_C_c_type, ID_wchar_t);
147  return std::move(result);
148  }
149  else
150  {
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;
198  else if(config.ansi_c.long_double_width==64)
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 
215  result.set(ID_C_c_type, ID_long_double);
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 
226  return signed_int_type();
228  return signed_long_int_type();
230  return signed_long_long_int_type();
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 
251 std::string c_type_as_string(const irep_idt &c_type)
252 {
253  if(c_type==ID_signed_int)
254  return "signed int";
255  else if(c_type==ID_signed_short_int)
256  return "signed short int";
257  else if(c_type==ID_unsigned_int)
258  return "unsigned int";
259  else if(c_type==ID_unsigned_short_int)
260  return "unsigned short int";
261  else if(c_type==ID_signed_long_int)
262  return "signed long int";
263  else if(c_type==ID_signed_long_long_int)
264  return "signed long long int";
265  else if(c_type==ID_unsigned_long_int)
266  return "unsigned long int";
267  else if(c_type==ID_unsigned_long_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 
299 std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
301 {
302  const union_typet::componentst &comps = components();
303 
304  std::optional<mp_integer> max_width;
305  typet max_comp_type;
306  irep_idt max_comp_name;
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 
318  max_width = *element_width;
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(
327  struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
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
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
Definition: ieee_float.cpp:25
static ieee_float_spect double_precision()
Definition: ieee_float.h:76
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:121
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.
std::size_t long_double_width
Definition: config.h:146
bool wchar_t_is_unsigned
Definition: config.h:150
std::size_t pointer_width
Definition: config.h:143
std::size_t wchar_t_width
Definition: config.h:147
bool char_is_unsigned
Definition: config.h:150
std::size_t bool_width
Definition: config.h:139
std::size_t long_long_int_width
Definition: config.h:142
std::size_t long_int_width
Definition: config.h:138
std::size_t short_int_width
Definition: config.h:141
std::size_t char_width
Definition: config.h:140
std::size_t int_width
Definition: config.h:137