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 {
24  return c_index_type();
25 }
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();
64  return unsigned_long_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();
235  return signed_long_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 {
247  return reference_typet(subtype, config.ansi_c.pointer_width);
248 }
249 
251 {
252  static const auto result = empty_typet();
253  return result;
254 }
255 
256 std::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 }
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:75
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
Definition: ieee_float.cpp:24
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 ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:107
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.
configt config
Definition: config.cpp:25
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:133
bool wchar_t_is_unsigned
Definition: config.h:137
std::size_t pointer_width
Definition: config.h:130
std::size_t wchar_t_width
Definition: config.h:134
bool char_is_unsigned
Definition: config.h:137
std::size_t bool_width
Definition: config.h:126
std::size_t long_long_int_width
Definition: config.h:129
std::size_t long_int_width
Definition: config.h:125
std::size_t short_int_width
Definition: config.h:128
std::size_t char_width
Definition: config.h:127
std::size_t int_width
Definition: config.h:124