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(
256  src_type.id() != ID_struct_tag &&
257  src_type.id() != ID_union_tag)
258  {
259  return src_type;
260  }
261 
262  typet result_type=src_type;
263 
264  // collect qualifiers
265  c_qualifierst qualifiers(src_type);
266 
267  while(result_type.id() == ID_struct_tag || result_type.id() == ID_union_tag)
268  {
269  const typet &followed_type = ns.follow(result_type);
270  result_type = followed_type;
271  qualifiers += c_qualifierst(followed_type);
272  }
273 
274  qualifiers.write(result_type);
275 
276  return result_type;
277 }
278 
280  const typet &type) const
281 {
282  const std::size_t width = type.get_size_t(ID_width);
283 
284  if(type.id()==ID_signedbv)
285  {
286  if(width<=config.ansi_c.char_width)
287  return CHAR;
288  else if(width<=config.ansi_c.short_int_width)
289  return SHORT;
290  else if(width<=config.ansi_c.int_width)
291  return INT;
292  else if(width<=config.ansi_c.long_int_width)
293  return LONG;
294  else if(width<=config.ansi_c.long_long_int_width)
295  return LONGLONG;
296  else
297  return LARGE_SIGNED_INT;
298  }
299  else if(type.id()==ID_unsignedbv)
300  {
301  if(width<=config.ansi_c.char_width)
302  return UCHAR;
303  else if(width<=config.ansi_c.short_int_width)
304  return USHORT;
305  else if(width<=config.ansi_c.int_width)
306  return UINT;
307  else if(width<=config.ansi_c.long_int_width)
308  return ULONG;
309  else if(width<=config.ansi_c.long_long_int_width)
310  return ULONGLONG;
311  else
312  return LARGE_UNSIGNED_INT;
313  }
314  else if(type.id()==ID_bool)
315  return BOOL;
316  else if(type.id()==ID_c_bool)
317  return BOOL;
318  else if(type.id()==ID_floatbv)
319  {
320  if(width<=config.ansi_c.single_width)
321  return SINGLE;
322  else if(width<=config.ansi_c.double_width)
323  return DOUBLE;
324  else if(width<=config.ansi_c.long_double_width)
325  return LONGDOUBLE;
326  else if(width<=128)
327  return FLOAT128;
328  }
329  else if(type.id()==ID_fixedbv)
330  {
331  return FIXEDBV;
332  }
333  else if(type.id()==ID_pointer)
334  {
335  if(type.subtype().id()==ID_empty)
336  return VOIDPTR;
337  else
338  return PTR;
339  }
340  else if(type.id()==ID_array)
341  {
342  return PTR;
343  }
344  else if(type.id()==ID_c_enum ||
345  type.id()==ID_c_enum_tag ||
346  type.id()==ID_incomplete_c_enum)
347  {
348  return INT;
349  }
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  if(src_type.subtype().get_bool(ID_C_volatile) &&
559  !dest_type.subtype().get_bool(ID_C_volatile))
560  warnings.push_back("disregarding volatile");
561 
562  if(src_type==dest_type)
563  {
564  expr.type()=src_type; // because of qualifiers
565  }
566  else
567  do_typecast(expr, orig_dest_type);
568 
569  return; // ok
570  }
571  }
572 
573  if(check_c_implicit_typecast(src_type, dest_type))
574  errors.push_back("implicit conversion not permitted");
575  else if(src_type!=dest_type)
576  do_typecast(expr, orig_dest_type);
577 }
578 
580  exprt &expr1,
581  exprt &expr2)
582 {
583  const typet &type1=ns.follow(expr1.type());
584  const typet &type2=ns.follow(expr2.type());
585 
586  c_typet c_type1=minimum_promotion(type1),
587  c_type2=minimum_promotion(type2);
588 
589  c_typet max_type=std::max(c_type1, c_type2);
590 
591  if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
592  {
593  // get the biggest width of both
594  std::size_t width1=type1.get_size_t(ID_width);
595  std::size_t width2=type2.get_size_t(ID_width);
596 
597  // produce type
598  typet result_type;
599 
600  if(width1==width2)
601  {
602  if(max_type==LARGE_SIGNED_INT)
603  result_type=signedbv_typet(width1);
604  else
605  result_type=unsignedbv_typet(width1);
606  }
607  else if(width1>width2)
608  result_type=type1;
609  else // width1<width2
610  result_type=type2;
611 
612  do_typecast(expr1, result_type);
613  do_typecast(expr2, result_type);
614 
615  return;
616  }
617  else if(max_type==FIXEDBV)
618  {
619  typet result_type;
620 
621  if(c_type1==FIXEDBV && c_type2==FIXEDBV)
622  {
623  // get bigger of both
624  std::size_t width1=to_fixedbv_type(type1).get_width();
625  std::size_t width2=to_fixedbv_type(type2).get_width();
626  if(width1>=width2)
627  result_type=type1;
628  else
629  result_type=type2;
630  }
631  else if(c_type1==FIXEDBV)
632  result_type=type1;
633  else
634  result_type=type2;
635 
636  do_typecast(expr1, result_type);
637  do_typecast(expr2, result_type);
638 
639  return;
640  }
641  else if(max_type==COMPLEX)
642  {
643  if(c_type1==COMPLEX && c_type2==COMPLEX)
644  {
645  // promote to the one with bigger subtype
646  if(get_c_type(type1.subtype())>get_c_type(type2.subtype()))
647  do_typecast(expr2, type1);
648  else
649  do_typecast(expr1, type2);
650  }
651  else if(c_type1==COMPLEX)
652  {
653  assert(c_type1==COMPLEX && c_type2!=COMPLEX);
654  do_typecast(expr2, type1.subtype());
655  do_typecast(expr2, type1);
656  }
657  else
658  {
659  assert(c_type1!=COMPLEX && c_type2==COMPLEX);
660  do_typecast(expr1, type2.subtype());
661  do_typecast(expr1, type2);
662  }
663 
664  return;
665  }
666  else if(max_type==SINGLE || max_type==DOUBLE ||
667  max_type==LONGDOUBLE || max_type==FLOAT128)
668  {
669  // Special-case optimisation:
670  // If we have two non-standard sized floats, don't do implicit type
671  // promotion if we can possibly avoid it.
672  if(type1==type2)
673  return;
674  }
675 
676  implicit_typecast_arithmetic(expr1, max_type);
677  implicit_typecast_arithmetic(expr2, max_type);
678 
679  // arithmetic typecasts only, otherwise this can't be used from
680  // typecheck_expr_trinary
681  #if 0
682  if(max_type==PTR)
683  {
684  if(c_type1==VOIDPTR)
685  do_typecast(expr1, expr2.type());
686 
687  if(c_type2==VOIDPTR)
688  do_typecast(expr2, expr1.type());
689  }
690  #endif
691 }
692 
693 void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
694 {
695  // special case: array -> pointer is actually
696  // something like address_of
697 
698  const typet &src_type=ns.follow(expr.type());
699 
700  if(src_type.id()==ID_array)
701  {
702  index_exprt index;
703  index.array()=expr;
704  index.index()=from_integer(0, index_type());
705  index.type()=src_type.subtype();
706  expr=address_of_exprt(index);
707  if(ns.follow(expr.type())!=ns.follow(dest_type))
708  expr.make_typecast(dest_type);
709  return;
710  }
711 
712  if(src_type!=dest_type)
713  {
714  // C booleans are special; we produce the
715  // explicit comparison with zero.
716  // Note that this requires ieee_float_notequal
717  // in case of floating-point numbers.
718 
719  if(dest_type.get(ID_C_c_type)==ID_bool)
720  {
721  expr=is_not_zero(expr, ns);
722  expr.make_typecast(dest_type);
723  }
724  else if(dest_type.id()==ID_bool)
725  {
726  expr=is_not_zero(expr, ns);
727  }
728  else
729  {
730  expr.make_typecast(dest_type);
731  }
732  }
733 }
c_typecastt::ns
const namespacet & ns
Definition: c_typecast.h:67
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
typet::subtype
const typet & subtype() const
Definition: type.h:38
c_typecastt::LONGLONG
Definition: c_typecast.h:76
arith_tools.h
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
signed_long_long_int_type
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
c_typecastt
Definition: c_typecast.h:41
rational_typet
Unbounded, signed rational numbers.
Definition: mathematical_types.h:39
irept::full_eq
bool full_eq(const irept &other) const
Definition: irep.cpp:379
typet
The type of an expression, extends irept.
Definition: type.h:27
c_typecastt::COMPLEX
Definition: c_typecast.h:82
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
c_typecastt::SINGLE
Definition: c_typecast.h:80
c_typecastt::INT
Definition: c_typecast.h:74
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:21
c_typecastt::BOOL
Definition: c_typecast.h:71
exprt
Base class for all expressions.
Definition: expr.h:54
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
configt::ansi_c
struct configt::ansi_ct ansi_c
c_implicit_typecast_arithmetic
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:49
c_qualifiers.h
c_typecastt::minimum_promotion
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:407
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
is_void_pointer
bool is_void_pointer(const typet &type)
Definition: c_typecast.cpp:58
c_typecastt::UCHAR
Definition: c_typecast.h:72
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
unsigned_long_long_int_type
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
c_typecastt::LONG
Definition: c_typecast.h:75
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
c_typecastt::get_c_type
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:279
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
c_typecastt::warnings
std::list< std::string > warnings
Definition: c_typecast.h:64
real_typet
Unbounded, signed real numbers.
Definition: mathematical_types.h:48
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
check_c_implicit_typecast
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:36
base_type.h
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:38
c_typecastt::INTEGER
Definition: c_typecast.h:78
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:35
c_typecastt::LARGE_SIGNED_INT
Definition: c_typecast.h:77
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
c_typecastt::REAL
Definition: c_typecast.h:81
c_qualifierst
Definition: c_qualifiers.h:60
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:259
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:269
c_implicit_typecast
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
c_typecastt::USHORT
Definition: c_typecast.h:73
c_typecastt::PTR
Definition: c_typecast.h:83
c_typecastt::implicit_typecast_followed
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
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
c_typecastt::UINT
Definition: c_typecast.h:74
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
c_typecastt::LONGDOUBLE
Definition: c_typecast.h:80
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
expr_util.h
Deprecated expression utility functions.
c_typecastt::VOIDPTR
Definition: c_typecast.h:83
c_typecastt::FLOAT128
Definition: c_typecast.h:80
c_typecastt::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:439
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
c_typecast.h
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
c_typecastt::errors
std::list< std::string > errors
Definition: c_typecast.h:63
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:39
c_typecastt::ULONGLONG
Definition: c_typecast.h:76
c_typecastt::LARGE_UNSIGNED_INT
Definition: c_typecast.h:77
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:34
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
c_typecastt::c_typet
c_typet
Definition: c_typecast.h:71
c_typecastt::SHORT
Definition: c_typecast.h:73
c_typecastt::CHAR
Definition: c_typecast.h:72
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:37
c_typecastt::OTHER
Definition: c_typecast.h:83
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
c_typecastt::ULONG
Definition: c_typecast.h:75
c_typecastt::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:445
c_typecastt::follow_with_qualifiers
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:253
c_typecastt::do_typecast
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:693
c_typecastt::DOUBLE
Definition: c_typecast.h:80
std_expr.h
c_typecastt::RATIONAL
Definition: c_typecast.h:81
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
c_types.h
c_typecastt::FIXEDBV
Definition: c_typecast.h:79
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31