cprover
c_typecast.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_typecast.h"
10 
11 #include <algorithm>
12 
13 #include <cassert>
14 
15 #include <util/arith_tools.h>
16 #include <util/c_types.h>
17 #include <util/config.h>
18 #include <util/expr_util.h>
19 #include <util/std_expr.h>
20 #include <util/base_type.h>
21 #include <util/symbol.h>
22 #include <util/simplify_expr.h>
23 
24 #include "c_qualifiers.h"
25 
27  exprt &expr,
28  const typet &dest_type,
29  const namespacet &ns)
30 {
31  c_typecastt c_typecast(ns);
32  c_typecast.implicit_typecast(expr, dest_type);
33  return !c_typecast.errors.empty();
34 }
35 
37  const typet &src_type,
38  const typet &dest_type,
39  const namespacet &ns)
40 {
41  c_typecastt c_typecast(ns);
42  exprt tmp;
43  tmp.type()=src_type;
44  c_typecast.implicit_typecast(tmp, dest_type);
45  return !c_typecast.errors.empty();
46 }
47 
50  exprt &expr1, exprt &expr2,
51  const namespacet &ns)
52 {
53  c_typecastt c_typecast(ns);
54  c_typecast.implicit_typecast_arithmetic(expr1, expr2);
55  return !c_typecast.errors.empty();
56 }
57 
58 bool is_void_pointer(const typet &type)
59 {
60  if(type.id()==ID_pointer)
61  {
62  if(type.subtype().id()==ID_empty)
63  return true;
64 
65  return is_void_pointer(type.subtype());
66  }
67  else
68  return false;
69 }
70 
72  const typet &src_type,
73  const typet &dest_type)
74 {
75  // check qualifiers
76 
77  if(src_type.id()==ID_pointer && dest_type.id()==ID_pointer &&
78  src_type.subtype().get_bool(ID_C_constant) &&
79  !dest_type.subtype().get_bool(ID_C_constant))
80  return true;
81 
82  if(src_type==dest_type)
83  return false;
84 
85  const irep_idt &src_type_id=src_type.id();
86 
87  if(src_type_id==ID_c_bit_field)
88  return check_c_implicit_typecast(src_type.subtype(), dest_type);
89 
90  if(dest_type.id()==ID_c_bit_field)
91  return check_c_implicit_typecast(src_type, dest_type.subtype());
92 
93  if(src_type_id==ID_natural)
94  {
95  if(dest_type.id()==ID_bool ||
96  dest_type.id()==ID_c_bool ||
97  dest_type.id()==ID_integer ||
98  dest_type.id()==ID_real ||
99  dest_type.id()==ID_complex ||
100  dest_type.id()==ID_unsignedbv ||
101  dest_type.id()==ID_signedbv ||
102  dest_type.id()==ID_floatbv ||
103  dest_type.id()==ID_complex)
104  return false;
105  }
106  else if(src_type_id==ID_integer)
107  {
108  if(dest_type.id()==ID_bool ||
109  dest_type.id()==ID_c_bool ||
110  dest_type.id()==ID_real ||
111  dest_type.id()==ID_complex ||
112  dest_type.id()==ID_unsignedbv ||
113  dest_type.id()==ID_signedbv ||
114  dest_type.id()==ID_floatbv ||
115  dest_type.id()==ID_fixedbv ||
116  dest_type.id()==ID_pointer ||
117  dest_type.id()==ID_complex)
118  return false;
119  }
120  else if(src_type_id==ID_real)
121  {
122  if(dest_type.id()==ID_bool ||
123  dest_type.id()==ID_c_bool ||
124  dest_type.id()==ID_complex ||
125  dest_type.id()==ID_floatbv ||
126  dest_type.id()==ID_fixedbv ||
127  dest_type.id()==ID_complex)
128  return false;
129  }
130  else if(src_type_id==ID_rational)
131  {
132  if(dest_type.id()==ID_bool ||
133  dest_type.id()==ID_c_bool ||
134  dest_type.id()==ID_complex ||
135  dest_type.id()==ID_floatbv ||
136  dest_type.id()==ID_fixedbv ||
137  dest_type.id()==ID_complex)
138  return false;
139  }
140  else if(src_type_id==ID_bool)
141  {
142  if(dest_type.id()==ID_c_bool ||
143  dest_type.id()==ID_integer ||
144  dest_type.id()==ID_real ||
145  dest_type.id()==ID_unsignedbv ||
146  dest_type.id()==ID_signedbv ||
147  dest_type.id()==ID_pointer ||
148  dest_type.id()==ID_floatbv ||
149  dest_type.id()==ID_fixedbv ||
150  dest_type.id()==ID_c_enum ||
151  dest_type.id()==ID_c_enum_tag ||
152  dest_type.id()==ID_complex)
153  return false;
154  }
155  else if(src_type_id==ID_unsignedbv ||
156  src_type_id==ID_signedbv ||
157  src_type_id==ID_c_enum ||
158  src_type_id==ID_c_enum_tag ||
159  src_type_id==ID_incomplete_c_enum ||
160  src_type_id==ID_c_bool)
161  {
162  if(dest_type.id()==ID_unsignedbv ||
163  dest_type.id()==ID_bool ||
164  dest_type.id()==ID_c_bool ||
165  dest_type.id()==ID_integer ||
166  dest_type.id()==ID_real ||
167  dest_type.id()==ID_rational ||
168  dest_type.id()==ID_signedbv ||
169  dest_type.id()==ID_floatbv ||
170  dest_type.id()==ID_fixedbv ||
171  dest_type.id()==ID_pointer ||
172  dest_type.id()==ID_c_enum ||
173  dest_type.id()==ID_c_enum_tag ||
174  dest_type.id()==ID_incomplete_c_enum ||
175  dest_type.id()==ID_complex)
176  return false;
177  }
178  else if(src_type_id==ID_floatbv ||
179  src_type_id==ID_fixedbv)
180  {
181  if(dest_type.id()==ID_bool ||
182  dest_type.id()==ID_c_bool ||
183  dest_type.id()==ID_integer ||
184  dest_type.id()==ID_real ||
185  dest_type.id()==ID_rational ||
186  dest_type.id()==ID_signedbv ||
187  dest_type.id()==ID_unsignedbv ||
188  dest_type.id()==ID_floatbv ||
189  dest_type.id()==ID_fixedbv ||
190  dest_type.id()==ID_complex)
191  return false;
192  }
193  else if(src_type_id==ID_complex)
194  {
195  if(dest_type.id()==ID_complex)
196  return check_c_implicit_typecast(src_type.subtype(), dest_type.subtype());
197  else
198  {
199  // 6.3.1.7, par 2:
200 
201  // When a value of complex type is converted to a real type, the
202  // imaginary part of the complex value is discarded and the value of the
203  // real part is converted according to the conversion rules for the
204  // corresponding real type.
205 
206  return check_c_implicit_typecast(src_type.subtype(), dest_type);
207  }
208  }
209  else if(src_type_id==ID_array ||
210  src_type_id==ID_pointer)
211  {
212  if(dest_type.id()==ID_pointer)
213  {
214  const irept &dest_subtype=dest_type.subtype();
215  const irept &src_subtype =src_type.subtype();
216 
217  if(src_subtype==dest_subtype)
218  return false;
219  else if(is_void_pointer(src_type) || // from void to anything
220  is_void_pointer(dest_type)) // to void from anything
221  return false;
222  }
223 
224  if(dest_type.id()==ID_array &&
225  src_type.subtype()==dest_type.subtype())
226  return false;
227 
228  if(dest_type.id()==ID_bool ||
229  dest_type.id()==ID_c_bool ||
230  dest_type.id()==ID_unsignedbv ||
231  dest_type.id()==ID_signedbv)
232  return false;
233  }
234  else if(src_type_id==ID_vector)
235  {
236  if(dest_type.id()==ID_vector)
237  return false;
238  }
239  else if(src_type_id==ID_complex)
240  {
241  if(dest_type.id()==ID_complex)
242  {
243  // We convert between complex types if we convert between
244  // their component types.
245  if(!check_c_implicit_typecast(src_type.subtype(), dest_type.subtype()))
246  return false;
247  }
248  }
249 
250  return true;
251 }
252 
254 {
255  if(src_type.id()!=ID_symbol)
256  return src_type;
257 
258  typet result_type=src_type;
259 
260  // collect qualifiers
261  c_qualifierst qualifiers(src_type);
262 
263  while(result_type.id()==ID_symbol)
264  {
265  const symbolt &followed_type_symbol =
266  ns.lookup(to_symbol_type(result_type));
267 
268  result_type=followed_type_symbol.type;
269  qualifiers+=c_qualifierst(followed_type_symbol.type);
270  }
271 
272  qualifiers.write(result_type);
273 
274  return result_type;
275 }
276 
278  const typet &type) const
279 {
280  unsigned width=type.get_int(ID_width);
281 
282  if(type.id()==ID_signedbv)
283  {
284  if(width<=config.ansi_c.char_width)
285  return CHAR;
286  else if(width<=config.ansi_c.short_int_width)
287  return SHORT;
288  else if(width<=config.ansi_c.int_width)
289  return INT;
290  else if(width<=config.ansi_c.long_int_width)
291  return LONG;
292  else if(width<=config.ansi_c.long_long_int_width)
293  return LONGLONG;
294  else
295  return LARGE_SIGNED_INT;
296  }
297  else if(type.id()==ID_unsignedbv)
298  {
299  if(width<=config.ansi_c.char_width)
300  return UCHAR;
301  else if(width<=config.ansi_c.short_int_width)
302  return USHORT;
303  else if(width<=config.ansi_c.int_width)
304  return UINT;
305  else if(width<=config.ansi_c.long_int_width)
306  return ULONG;
307  else if(width<=config.ansi_c.long_long_int_width)
308  return ULONGLONG;
309  else
310  return LARGE_UNSIGNED_INT;
311  }
312  else if(type.id()==ID_bool)
313  return BOOL;
314  else if(type.id()==ID_c_bool)
315  return BOOL;
316  else if(type.id()==ID_floatbv)
317  {
318  if(width<=config.ansi_c.single_width)
319  return SINGLE;
320  else if(width<=config.ansi_c.double_width)
321  return DOUBLE;
322  else if(width<=config.ansi_c.long_double_width)
323  return LONGDOUBLE;
324  else if(width<=128)
325  return FLOAT128;
326  }
327  else if(type.id()==ID_fixedbv)
328  {
329  return FIXEDBV;
330  }
331  else if(type.id()==ID_pointer)
332  {
333  if(type.subtype().id()==ID_empty)
334  return VOIDPTR;
335  else
336  return PTR;
337  }
338  else if(type.id()==ID_array)
339  {
340  return PTR;
341  }
342  else if(type.id()==ID_c_enum ||
343  type.id()==ID_c_enum_tag ||
344  type.id()==ID_incomplete_c_enum)
345  {
346  return INT;
347  }
348  else if(type.id()==ID_symbol)
349  return get_c_type(ns.follow(type));
350  else if(type.id()==ID_rational)
351  return RATIONAL;
352  else if(type.id()==ID_real)
353  return REAL;
354  else if(type.id()==ID_complex)
355  return COMPLEX;
356  else if(type.id()==ID_c_bit_field)
357  return get_c_type(to_c_bit_field_type(type).subtype());
358 
359  return OTHER;
360 }
361 
363  exprt &expr,
364  c_typet c_type)
365 {
366  typet new_type;
367 
368  const typet &expr_type=ns.follow(expr.type());
369 
370  switch(c_type)
371  {
372  case PTR:
373  if(expr_type.id()==ID_array)
374  {
375  new_type=pointer_type(expr_type.subtype());
376  break;
377  }
378  return;
379 
380  case BOOL: UNREACHABLE; // should always be promoted to int
381  case CHAR: UNREACHABLE; // should always be promoted to int
382  case UCHAR: UNREACHABLE; // should always be promoted to int
383  case SHORT: UNREACHABLE; // should always be promoted to int
384  case USHORT: UNREACHABLE; // should always be promoted to int
385  case INT: new_type=signed_int_type(); break;
386  case UINT: new_type=unsigned_int_type(); break;
387  case LONG: new_type=signed_long_int_type(); break;
388  case ULONG: new_type=unsigned_long_int_type(); break;
389  case LONGLONG: new_type=signed_long_long_int_type(); break;
390  case ULONGLONG: new_type=unsigned_long_long_int_type(); break;
391  case SINGLE: new_type=float_type(); break;
392  case DOUBLE: new_type=double_type(); break;
393  case LONGDOUBLE: new_type=long_double_type(); break;
394  // NOLINTNEXTLINE(whitespace/line_length)
395  case FLOAT128: new_type=ieee_float_spect::quadruple_precision().to_type(); break;
396  case RATIONAL: new_type=rational_typet(); break;
397  case REAL: new_type=real_typet(); break;
398  case INTEGER: new_type=integer_typet(); break;
399  case COMPLEX: return; // do nothing
400  default: return;
401  }
402 
403  if(new_type!=expr_type)
404  do_typecast(expr, new_type);
405 }
406 
408  const typet &type) const
409 {
410  c_typet c_type=get_c_type(type);
411 
412  // 6.3.1.1, par 2
413 
414  // "If an int can represent all values of the original type, the
415  // value is converted to an int; otherwise, it is converted to
416  // an unsigned int."
417 
418  c_typet max_type=std::max(c_type, INT); // minimum promotion
419 
420  // The second case can arise if we promote any unsigned type
421  // that is as large as unsigned int. In this case the promotion configuration
422  // via the enum is actually wrong, and we need to fix this up.
423  if(
425  c_type == USHORT)
426  max_type=UINT;
427  else if(
429  max_type=UINT;
430 
431  if(max_type==UINT &&
432  type.id()==ID_c_bit_field &&
434  max_type=INT;
435 
436  return max_type;
437 }
438 
440 {
441  c_typet c_type=minimum_promotion(expr.type());
442  implicit_typecast_arithmetic(expr, c_type);
443 }
444 
446  exprt &expr,
447  const typet &type)
448 {
449  typet src_type=follow_with_qualifiers(expr.type()),
450  dest_type=follow_with_qualifiers(type);
451 
452  typet type_qual=type;
453  c_qualifierst qualifiers(dest_type);
454  qualifiers.write(type_qual);
455 
456  implicit_typecast_followed(expr, src_type, type_qual, dest_type);
457 }
458 
460  exprt &expr,
461  const typet &src_type,
462  const typet &orig_dest_type,
463  const typet &dest_type)
464 {
465  // do transparent union
466  if(dest_type.id()==ID_union &&
467  dest_type.get_bool(ID_C_transparent_union) &&
468  src_type.id()!=ID_union)
469  {
470  // The argument corresponding to a transparent union type can be of any
471  // type in the union; no explicit cast is required.
472 
473  // GCC docs say:
474  // If the union member type is a pointer, qualifiers like const on the
475  // referenced type must be respected, just as with normal pointer
476  // conversions.
477  // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
478  typet src_type_no_const=src_type;
479  if(src_type.id()==ID_pointer &&
480  src_type.subtype().get_bool(ID_C_constant))
481  src_type_no_const.subtype().remove(ID_C_constant);
482 
483  // Check union members.
484  for(const auto &comp : to_union_type(dest_type).components())
485  {
486  if(!check_c_implicit_typecast(src_type_no_const, comp.type()))
487  {
488  // build union constructor
489  union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
490  if(!src_type.full_eq(src_type_no_const))
491  do_typecast(union_expr.op(), src_type_no_const);
492  expr=union_expr;
493  return; // ok
494  }
495  }
496  }
497 
498  if(dest_type.id()==ID_pointer)
499  {
500  // special case: 0 == NULL
501 
502  if(simplify_expr(expr, ns).is_zero() && (
503  src_type.id()==ID_unsignedbv ||
504  src_type.id()==ID_signedbv ||
505  src_type.id()==ID_natural ||
506  src_type.id()==ID_integer))
507  {
508  expr=exprt(ID_constant, orig_dest_type);
509  expr.set(ID_value, ID_NULL);
510  return; // ok
511  }
512 
513  if(src_type.id()==ID_pointer ||
514  src_type.id()==ID_array)
515  {
516  // we are quite generous about pointers
517 
518  const typet &src_sub=ns.follow(src_type.subtype());
519  const typet &dest_sub=ns.follow(dest_type.subtype());
520 
521  if(is_void_pointer(src_type) ||
522  is_void_pointer(dest_type))
523  {
524  // from/to void is always good
525  }
526  else if(src_sub.id()==ID_code &&
527  dest_sub.id()==ID_code)
528  {
529  // very generous:
530  // between any two function pointers it's ok
531  }
532  else if(base_type_eq(src_sub, dest_sub, ns))
533  {
534  // ok
535  }
536  else if((is_number(src_sub) ||
537  src_sub.id()==ID_c_enum ||
538  src_sub.id()==ID_c_enum_tag) &&
539  (is_number(dest_sub) ||
540  dest_sub.id()==ID_c_enum ||
541  src_sub.id()==ID_c_enum_tag))
542  {
543  // Also generous: between any to scalar types it's ok.
544  // We should probably check the size.
545  }
546  else if(src_sub.id()==ID_array &&
547  dest_sub.id()==ID_array &&
548  base_type_eq(src_sub.subtype(), dest_sub.subtype(), ns))
549  {
550  // we ignore the size of the top-level array
551  // in the case of pointers to arrays
552  }
553  else
554  warnings.push_back("incompatible pointer types");
555 
556  // check qualifiers
557 
558  /*
559  if(src_type.subtype().get_bool(ID_C_constant) &&
560  !dest_type.subtype().get_bool(ID_C_constant))
561  warnings.push_back("disregarding const");
562  */
563 
564  if(src_type.subtype().get_bool(ID_C_volatile) &&
565  !dest_type.subtype().get_bool(ID_C_volatile))
566  warnings.push_back("disregarding volatile");
567 
568  if(src_type==dest_type)
569  {
570  expr.type()=src_type; // because of qualifiers
571  }
572  else
573  do_typecast(expr, orig_dest_type);
574 
575  return; // ok
576  }
577  }
578 
579  if(check_c_implicit_typecast(src_type, dest_type))
580  errors.push_back("implicit conversion not permitted");
581  else if(src_type!=dest_type)
582  do_typecast(expr, orig_dest_type);
583 }
584 
586  exprt &expr1,
587  exprt &expr2)
588 {
589  const typet &type1=ns.follow(expr1.type());
590  const typet &type2=ns.follow(expr2.type());
591 
592  c_typet c_type1=minimum_promotion(type1),
593  c_type2=minimum_promotion(type2);
594 
595  c_typet max_type=std::max(c_type1, c_type2);
596 
597  if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
598  {
599  // get the biggest width of both
600  std::size_t width1=type1.get_size_t(ID_width);
601  std::size_t width2=type2.get_size_t(ID_width);
602 
603  // produce type
604  typet result_type;
605 
606  if(width1==width2)
607  {
608  if(max_type==LARGE_SIGNED_INT)
609  result_type=signedbv_typet(width1);
610  else
611  result_type=unsignedbv_typet(width1);
612  }
613  else if(width1>width2)
614  result_type=type1;
615  else // width1<width2
616  result_type=type2;
617 
618  do_typecast(expr1, result_type);
619  do_typecast(expr2, result_type);
620 
621  return;
622  }
623  else if(max_type==FIXEDBV)
624  {
625  typet result_type;
626 
627  if(c_type1==FIXEDBV && c_type2==FIXEDBV)
628  {
629  // get bigger of both
630  std::size_t width1=to_fixedbv_type(type1).get_width();
631  std::size_t width2=to_fixedbv_type(type2).get_width();
632  if(width1>=width2)
633  result_type=type1;
634  else
635  result_type=type2;
636  }
637  else if(c_type1==FIXEDBV)
638  result_type=type1;
639  else
640  result_type=type2;
641 
642  do_typecast(expr1, result_type);
643  do_typecast(expr2, result_type);
644 
645  return;
646  }
647  else if(max_type==COMPLEX)
648  {
649  if(c_type1==COMPLEX && c_type2==COMPLEX)
650  {
651  // promote to the one with bigger subtype
652  if(get_c_type(type1.subtype())>get_c_type(type2.subtype()))
653  do_typecast(expr2, type1);
654  else
655  do_typecast(expr1, type2);
656  }
657  else if(c_type1==COMPLEX)
658  {
659  assert(c_type1==COMPLEX && c_type2!=COMPLEX);
660  do_typecast(expr2, type1.subtype());
661  do_typecast(expr2, type1);
662  }
663  else
664  {
665  assert(c_type1!=COMPLEX && c_type2==COMPLEX);
666  do_typecast(expr1, type2.subtype());
667  do_typecast(expr1, type2);
668  }
669 
670  return;
671  }
672  else if(max_type==SINGLE || max_type==DOUBLE ||
673  max_type==LONGDOUBLE || max_type==FLOAT128)
674  {
675  // Special-case optimisation:
676  // If we have two non-standard sized floats, don't do implicit type
677  // promotion if we can possibly avoid it.
678  if(type1==type2)
679  return;
680  }
681 
682  implicit_typecast_arithmetic(expr1, max_type);
683  implicit_typecast_arithmetic(expr2, max_type);
684 
685  // arithmetic typecasts only, otherwise this can't be used from
686  // typecheck_expr_trinary
687  #if 0
688  if(max_type==PTR)
689  {
690  if(c_type1==VOIDPTR)
691  do_typecast(expr1, expr2.type());
692 
693  if(c_type2==VOIDPTR)
694  do_typecast(expr2, expr1.type());
695  }
696  #endif
697 }
698 
699 void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
700 {
701  // special case: array -> pointer is actually
702  // something like address_of
703 
704  const typet &src_type=ns.follow(expr.type());
705 
706  if(src_type.id()==ID_array)
707  {
708  index_exprt index;
709  index.array()=expr;
710  index.index()=from_integer(0, index_type());
711  index.type()=src_type.subtype();
712  expr=address_of_exprt(index);
713  if(ns.follow(expr.type())!=ns.follow(dest_type))
714  expr.make_typecast(dest_type);
715  return;
716  }
717 
718  if(src_type!=dest_type)
719  {
720  // C booleans are special; we produce the
721  // explicit comparison with zero.
722  // Note that this requires ieee_float_notequal
723  // in case of floating-point numbers.
724 
725  if(dest_type.get(ID_C_c_type)==ID_bool)
726  {
727  expr=is_not_zero(expr, ns);
728  expr.make_typecast(dest_type);
729  }
730  else if(dest_type.id()==ID_bool)
731  {
732  expr=is_not_zero(expr, ns);
733  }
734  else
735  {
736  expr.make_typecast(dest_type);
737  }
738  }
739 }
The type of an expression.
Definition: type.h:22
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Symbol table entry.
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:699
Deprecated expression utility functions.
bool full_eq(const irept &other) const
Definition: irep.cpp:380
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
std::size_t single_width
Definition: config.h:37
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:36
Unbounded, signed rational numbers.
Definition: std_types.h:90
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
bitvector_typet double_type()
Definition: c_types.cpp:193
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Definition: c_typecast.cpp:459
typet & type()
Definition: expr.h:56
std::size_t double_width
Definition: config.h:38
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:277
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:23
std::size_t char_width
Definition: config.h:33
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
const irep_idt & id() const
Definition: irep.h:189
std::size_t long_long_int_width
Definition: config.h:35
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:84
bitvector_typet float_type()
Definition: c_types.cpp:185
const namespacet & ns
Definition: c_typecast.h:67
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
std::list< std::string > warnings
Definition: c_typecast.h:64
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
std::size_t int_width
Definition: config.h:30
Base class for tree-like data structures with sharing.
Definition: irep.h:86
std::list< std::string > errors
Definition: c_typecast.h:63
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:253
Operator to return the address of an object.
Definition: std_expr.h:3170
std::size_t get_width() const
Definition: std_types.h:1129
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
bitvector_typet long_double_type()
Definition: c_types.cpp:201
Unbounded, signed integers.
Definition: std_types.h:70
typet type
Type of symbol.
Definition: symbol.h:34
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:439
bool is_number(const typet &type)
Definition: type.cpp:25
exprt & index()
Definition: std_expr.h:1496
Unbounded, signed real numbers.
Definition: std_types.h:100
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1334
Base class for all expressions.
Definition: expr.h:42
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:445
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:49
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
#define UNREACHABLE
Definition: invariant.h:250
bool is_void_pointer(const typet &type)
Definition: c_typecast.cpp:58
virtual void write(typet &src) const override
bool is_zero() const
Definition: expr.cpp:161
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1402
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
void remove(const irep_namet &name)
Definition: irep.cpp:270
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
std::size_t long_int_width
Definition: config.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:407
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
std::size_t short_int_width
Definition: config.h:34
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
std::size_t long_double_width
Definition: config.h:39
array index operator
Definition: std_expr.h:1462