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