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_symbol && 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_symbol || result_type.id() == ID_struct_tag ||
268  result_type.id() == ID_union_tag)
269  {
270  const typet &followed_type = ns.follow(result_type);
271  result_type = followed_type;
272  qualifiers += c_qualifierst(followed_type);
273  }
274 
275  qualifiers.write(result_type);
276 
277  return result_type;
278 }
279 
281  const typet &type) const
282 {
283  const std::size_t width = type.get_size_t(ID_width);
284 
285  if(type.id()==ID_signedbv)
286  {
287  if(width<=config.ansi_c.char_width)
288  return CHAR;
289  else if(width<=config.ansi_c.short_int_width)
290  return SHORT;
291  else if(width<=config.ansi_c.int_width)
292  return INT;
293  else if(width<=config.ansi_c.long_int_width)
294  return LONG;
295  else if(width<=config.ansi_c.long_long_int_width)
296  return LONGLONG;
297  else
298  return LARGE_SIGNED_INT;
299  }
300  else if(type.id()==ID_unsignedbv)
301  {
302  if(width<=config.ansi_c.char_width)
303  return UCHAR;
304  else if(width<=config.ansi_c.short_int_width)
305  return USHORT;
306  else if(width<=config.ansi_c.int_width)
307  return UINT;
308  else if(width<=config.ansi_c.long_int_width)
309  return ULONG;
310  else if(width<=config.ansi_c.long_long_int_width)
311  return ULONGLONG;
312  else
313  return LARGE_UNSIGNED_INT;
314  }
315  else if(type.id()==ID_bool)
316  return BOOL;
317  else if(type.id()==ID_c_bool)
318  return BOOL;
319  else if(type.id()==ID_floatbv)
320  {
321  if(width<=config.ansi_c.single_width)
322  return SINGLE;
323  else if(width<=config.ansi_c.double_width)
324  return DOUBLE;
325  else if(width<=config.ansi_c.long_double_width)
326  return LONGDOUBLE;
327  else if(width<=128)
328  return FLOAT128;
329  }
330  else if(type.id()==ID_fixedbv)
331  {
332  return FIXEDBV;
333  }
334  else if(type.id()==ID_pointer)
335  {
336  if(type.subtype().id()==ID_empty)
337  return VOIDPTR;
338  else
339  return PTR;
340  }
341  else if(type.id()==ID_array)
342  {
343  return PTR;
344  }
345  else if(type.id()==ID_c_enum ||
346  type.id()==ID_c_enum_tag ||
347  type.id()==ID_incomplete_c_enum)
348  {
349  return INT;
350  }
351  else if(type.id()==ID_symbol)
352  return get_c_type(ns.follow(type));
353  else if(type.id()==ID_rational)
354  return RATIONAL;
355  else if(type.id()==ID_real)
356  return REAL;
357  else if(type.id()==ID_complex)
358  return COMPLEX;
359  else if(type.id()==ID_c_bit_field)
360  return get_c_type(to_c_bit_field_type(type).subtype());
361 
362  return OTHER;
363 }
364 
366  exprt &expr,
367  c_typet c_type)
368 {
369  typet new_type;
370 
371  const typet &expr_type=ns.follow(expr.type());
372 
373  switch(c_type)
374  {
375  case PTR:
376  if(expr_type.id()==ID_array)
377  {
378  new_type=pointer_type(expr_type.subtype());
379  break;
380  }
381  return;
382 
383  case BOOL: UNREACHABLE; // should always be promoted to int
384  case CHAR: UNREACHABLE; // should always be promoted to int
385  case UCHAR: UNREACHABLE; // should always be promoted to int
386  case SHORT: UNREACHABLE; // should always be promoted to int
387  case USHORT: UNREACHABLE; // should always be promoted to int
388  case INT: new_type=signed_int_type(); break;
389  case UINT: new_type=unsigned_int_type(); break;
390  case LONG: new_type=signed_long_int_type(); break;
391  case ULONG: new_type=unsigned_long_int_type(); break;
392  case LONGLONG: new_type=signed_long_long_int_type(); break;
393  case ULONGLONG: new_type=unsigned_long_long_int_type(); break;
394  case SINGLE: new_type=float_type(); break;
395  case DOUBLE: new_type=double_type(); break;
396  case LONGDOUBLE: new_type=long_double_type(); break;
397  // NOLINTNEXTLINE(whitespace/line_length)
398  case FLOAT128: new_type=ieee_float_spect::quadruple_precision().to_type(); break;
399  case RATIONAL: new_type=rational_typet(); break;
400  case REAL: new_type=real_typet(); break;
401  case INTEGER: new_type=integer_typet(); break;
402  case COMPLEX: return; // do nothing
403  default: return;
404  }
405 
406  if(new_type!=expr_type)
407  do_typecast(expr, new_type);
408 }
409 
411  const typet &type) const
412 {
413  c_typet c_type=get_c_type(type);
414 
415  // 6.3.1.1, par 2
416 
417  // "If an int can represent all values of the original type, the
418  // value is converted to an int; otherwise, it is converted to
419  // an unsigned int."
420 
421  c_typet max_type=std::max(c_type, INT); // minimum promotion
422 
423  // The second case can arise if we promote any unsigned type
424  // that is as large as unsigned int. In this case the promotion configuration
425  // via the enum is actually wrong, and we need to fix this up.
426  if(
428  c_type == USHORT)
429  max_type=UINT;
430  else if(
432  max_type=UINT;
433 
434  if(max_type==UINT &&
435  type.id()==ID_c_bit_field &&
437  max_type=INT;
438 
439  return max_type;
440 }
441 
443 {
444  c_typet c_type=minimum_promotion(expr.type());
445  implicit_typecast_arithmetic(expr, c_type);
446 }
447 
449  exprt &expr,
450  const typet &type)
451 {
452  typet src_type=follow_with_qualifiers(expr.type()),
453  dest_type=follow_with_qualifiers(type);
454 
455  typet type_qual=type;
456  c_qualifierst qualifiers(dest_type);
457  qualifiers.write(type_qual);
458 
459  implicit_typecast_followed(expr, src_type, type_qual, dest_type);
460 }
461 
463  exprt &expr,
464  const typet &src_type,
465  const typet &orig_dest_type,
466  const typet &dest_type)
467 {
468  // do transparent union
469  if(dest_type.id()==ID_union &&
470  dest_type.get_bool(ID_C_transparent_union) &&
471  src_type.id()!=ID_union)
472  {
473  // The argument corresponding to a transparent union type can be of any
474  // type in the union; no explicit cast is required.
475 
476  // GCC docs say:
477  // If the union member type is a pointer, qualifiers like const on the
478  // referenced type must be respected, just as with normal pointer
479  // conversions.
480  // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
481  typet src_type_no_const=src_type;
482  if(src_type.id()==ID_pointer &&
483  src_type.subtype().get_bool(ID_C_constant))
484  src_type_no_const.subtype().remove(ID_C_constant);
485 
486  // Check union members.
487  for(const auto &comp : to_union_type(dest_type).components())
488  {
489  if(!check_c_implicit_typecast(src_type_no_const, comp.type()))
490  {
491  // build union constructor
492  union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
493  if(!src_type.full_eq(src_type_no_const))
494  do_typecast(union_expr.op(), src_type_no_const);
495  expr=union_expr;
496  return; // ok
497  }
498  }
499  }
500 
501  if(dest_type.id()==ID_pointer)
502  {
503  // special case: 0 == NULL
504 
505  if(simplify_expr(expr, ns).is_zero() && (
506  src_type.id()==ID_unsignedbv ||
507  src_type.id()==ID_signedbv ||
508  src_type.id()==ID_natural ||
509  src_type.id()==ID_integer))
510  {
511  expr=exprt(ID_constant, orig_dest_type);
512  expr.set(ID_value, ID_NULL);
513  return; // ok
514  }
515 
516  if(src_type.id()==ID_pointer ||
517  src_type.id()==ID_array)
518  {
519  // we are quite generous about pointers
520 
521  const typet &src_sub=ns.follow(src_type.subtype());
522  const typet &dest_sub=ns.follow(dest_type.subtype());
523 
524  if(is_void_pointer(src_type) ||
525  is_void_pointer(dest_type))
526  {
527  // from/to void is always good
528  }
529  else if(src_sub.id()==ID_code &&
530  dest_sub.id()==ID_code)
531  {
532  // very generous:
533  // between any two function pointers it's ok
534  }
535  else if(base_type_eq(src_sub, dest_sub, ns))
536  {
537  // ok
538  }
539  else if((is_number(src_sub) ||
540  src_sub.id()==ID_c_enum ||
541  src_sub.id()==ID_c_enum_tag) &&
542  (is_number(dest_sub) ||
543  dest_sub.id()==ID_c_enum ||
544  src_sub.id()==ID_c_enum_tag))
545  {
546  // Also generous: between any to scalar types it's ok.
547  // We should probably check the size.
548  }
549  else if(src_sub.id()==ID_array &&
550  dest_sub.id()==ID_array &&
551  base_type_eq(src_sub.subtype(), dest_sub.subtype(), ns))
552  {
553  // we ignore the size of the top-level array
554  // in the case of pointers to arrays
555  }
556  else
557  warnings.push_back("incompatible pointer types");
558 
559  // check qualifiers
560 
561  /*
562  if(src_type.subtype().get_bool(ID_C_constant) &&
563  !dest_type.subtype().get_bool(ID_C_constant))
564  warnings.push_back("disregarding const");
565  */
566 
567  if(src_type.subtype().get_bool(ID_C_volatile) &&
568  !dest_type.subtype().get_bool(ID_C_volatile))
569  warnings.push_back("disregarding volatile");
570 
571  if(src_type==dest_type)
572  {
573  expr.type()=src_type; // because of qualifiers
574  }
575  else
576  do_typecast(expr, orig_dest_type);
577 
578  return; // ok
579  }
580  }
581 
582  if(check_c_implicit_typecast(src_type, dest_type))
583  errors.push_back("implicit conversion not permitted");
584  else if(src_type!=dest_type)
585  do_typecast(expr, orig_dest_type);
586 }
587 
589  exprt &expr1,
590  exprt &expr2)
591 {
592  const typet &type1=ns.follow(expr1.type());
593  const typet &type2=ns.follow(expr2.type());
594 
595  c_typet c_type1=minimum_promotion(type1),
596  c_type2=minimum_promotion(type2);
597 
598  c_typet max_type=std::max(c_type1, c_type2);
599 
600  if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
601  {
602  // get the biggest width of both
603  std::size_t width1=type1.get_size_t(ID_width);
604  std::size_t width2=type2.get_size_t(ID_width);
605 
606  // produce type
607  typet result_type;
608 
609  if(width1==width2)
610  {
611  if(max_type==LARGE_SIGNED_INT)
612  result_type=signedbv_typet(width1);
613  else
614  result_type=unsignedbv_typet(width1);
615  }
616  else if(width1>width2)
617  result_type=type1;
618  else // width1<width2
619  result_type=type2;
620 
621  do_typecast(expr1, result_type);
622  do_typecast(expr2, result_type);
623 
624  return;
625  }
626  else if(max_type==FIXEDBV)
627  {
628  typet result_type;
629 
630  if(c_type1==FIXEDBV && c_type2==FIXEDBV)
631  {
632  // get bigger of both
633  std::size_t width1=to_fixedbv_type(type1).get_width();
634  std::size_t width2=to_fixedbv_type(type2).get_width();
635  if(width1>=width2)
636  result_type=type1;
637  else
638  result_type=type2;
639  }
640  else if(c_type1==FIXEDBV)
641  result_type=type1;
642  else
643  result_type=type2;
644 
645  do_typecast(expr1, result_type);
646  do_typecast(expr2, result_type);
647 
648  return;
649  }
650  else if(max_type==COMPLEX)
651  {
652  if(c_type1==COMPLEX && c_type2==COMPLEX)
653  {
654  // promote to the one with bigger subtype
655  if(get_c_type(type1.subtype())>get_c_type(type2.subtype()))
656  do_typecast(expr2, type1);
657  else
658  do_typecast(expr1, type2);
659  }
660  else if(c_type1==COMPLEX)
661  {
662  assert(c_type1==COMPLEX && c_type2!=COMPLEX);
663  do_typecast(expr2, type1.subtype());
664  do_typecast(expr2, type1);
665  }
666  else
667  {
668  assert(c_type1!=COMPLEX && c_type2==COMPLEX);
669  do_typecast(expr1, type2.subtype());
670  do_typecast(expr1, type2);
671  }
672 
673  return;
674  }
675  else if(max_type==SINGLE || max_type==DOUBLE ||
676  max_type==LONGDOUBLE || max_type==FLOAT128)
677  {
678  // Special-case optimisation:
679  // If we have two non-standard sized floats, don't do implicit type
680  // promotion if we can possibly avoid it.
681  if(type1==type2)
682  return;
683  }
684 
685  implicit_typecast_arithmetic(expr1, max_type);
686  implicit_typecast_arithmetic(expr2, max_type);
687 
688  // arithmetic typecasts only, otherwise this can't be used from
689  // typecheck_expr_trinary
690  #if 0
691  if(max_type==PTR)
692  {
693  if(c_type1==VOIDPTR)
694  do_typecast(expr1, expr2.type());
695 
696  if(c_type2==VOIDPTR)
697  do_typecast(expr2, expr1.type());
698  }
699  #endif
700 }
701 
702 void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
703 {
704  // special case: array -> pointer is actually
705  // something like address_of
706 
707  const typet &src_type=ns.follow(expr.type());
708 
709  if(src_type.id()==ID_array)
710  {
711  index_exprt index;
712  index.array()=expr;
713  index.index()=from_integer(0, index_type());
714  index.type()=src_type.subtype();
715  expr=address_of_exprt(index);
716  if(ns.follow(expr.type())!=ns.follow(dest_type))
717  expr.make_typecast(dest_type);
718  return;
719  }
720 
721  if(src_type!=dest_type)
722  {
723  // C booleans are special; we produce the
724  // explicit comparison with zero.
725  // Note that this requires ieee_float_notequal
726  // in case of floating-point numbers.
727 
728  if(dest_type.get(ID_C_c_type)==ID_bool)
729  {
730  expr=is_not_zero(expr, ns);
731  expr.make_typecast(dest_type);
732  }
733  else if(dest_type.id()==ID_bool)
734  {
735  expr=is_not_zero(expr, ns);
736  }
737  else
738  {
739  expr.make_typecast(dest_type);
740  }
741  }
742 }
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:1229
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:702
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
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
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:462
typet & type()
Definition: expr.h:56
std::size_t double_width
Definition: config.h:38
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:280
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:259
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:97
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:1271
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:156
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
std::size_t get_width() const
Definition: std_types.h:1138
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
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:442
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:1343
Base class for all expressions.
Definition: expr.h:42
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:448
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:271
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:1411
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:410
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
std::size_t short_int_width
Definition: config.h:34
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
std::size_t long_double_width
Definition: config.h:39
array index operator
Definition: std_expr.h:1462