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(result_type.get(ID_identifier));
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.id(ID_pointer);
376  new_type.subtype()=expr_type.subtype();
377  break;
378  }
379  return;
380 
381  case BOOL: assert(false); // should always be promoted to int
382  case CHAR: assert(false); // should always be promoted to int
383  case UCHAR: assert(false); // should always be promoted to int
384  case SHORT: assert(false); // should always be promoted to int
385  case USHORT: assert(false); // should always be promoted to int
386  case INT: new_type=signed_int_type(); break;
387  case UINT: new_type=unsigned_int_type(); break;
388  case LONG: new_type=signed_long_int_type(); break;
389  case ULONG: new_type=unsigned_long_int_type(); break;
390  case LONGLONG: new_type=signed_long_long_int_type(); break;
391  case ULONGLONG: new_type=unsigned_long_long_int_type(); break;
392  case SINGLE: new_type=float_type(); break;
393  case DOUBLE: new_type=double_type(); break;
394  case LONGDOUBLE: new_type=long_double_type(); break;
395  // NOLINTNEXTLINE(whitespace/line_length)
396  case FLOAT128: new_type=ieee_float_spect::quadruple_precision().to_type(); break;
397  case RATIONAL: new_type=rational_typet(); break;
398  case REAL: new_type=real_typet(); break;
399  case INTEGER: new_type=integer_typet(); break;
400  case COMPLEX: return; // do nothing
401  default: return;
402  }
403 
404  if(new_type!=expr_type)
405  do_typecast(expr, new_type);
406 }
407 
409  const typet &type) const
410 {
411  c_typet c_type=get_c_type(type);
412 
413  // 6.3.1.1, par 2
414 
415  // "If an int can represent all values of the original type, the
416  // value is converted to an int; otherwise, it is converted to
417  // an unsigned int."
418 
419  c_typet max_type=std::max(c_type, INT); // minimum promotion
420 
421  // The second case can arise if we promote any unsigned type
422  // that is as large as unsigned int.
423 
425  max_type==USHORT)
426  max_type=UINT;
428  max_type==UCHAR)
429  max_type=UINT;
430  else
431  max_type=std::max(max_type, INT);
432 
433  if(max_type==UINT &&
434  type.id()==ID_c_bit_field &&
436  max_type=INT;
437 
438  return max_type;
439 }
440 
442 {
443  c_typet c_type=minimum_promotion(expr.type());
444  implicit_typecast_arithmetic(expr, c_type);
445 }
446 
448  exprt &expr,
449  const typet &type)
450 {
451  typet src_type=follow_with_qualifiers(expr.type()),
452  dest_type=follow_with_qualifiers(type);
453 
454  typet type_qual=type;
455  c_qualifierst qualifiers(dest_type);
456  qualifiers.write(type_qual);
457 
458  implicit_typecast_followed(expr, src_type, type_qual, dest_type);
459 }
460 
462  exprt &expr,
463  const typet &src_type,
464  const typet &orig_dest_type,
465  const typet &dest_type)
466 {
467  // do transparent union
468  if(dest_type.id()==ID_union &&
469  dest_type.get_bool(ID_C_transparent_union) &&
470  src_type.id()!=ID_union)
471  {
472  // The argument corresponding to a transparent union type can be of any
473  // type in the union; no explicit cast is required.
474 
475  // GCC docs say:
476  // If the union member type is a pointer, qualifiers like const on the
477  // referenced type must be respected, just as with normal pointer
478  // conversions.
479  // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
480  typet src_type_no_const=src_type;
481  if(src_type.id()==ID_pointer &&
482  src_type.subtype().get_bool(ID_C_constant))
483  src_type_no_const.subtype().remove(ID_C_constant);
484 
485  // Check union members.
486  for(const auto &comp : to_union_type(dest_type).components())
487  {
488  if(!check_c_implicit_typecast(src_type_no_const, comp.type()))
489  {
490  // build union constructor
491  exprt union_expr(ID_union, orig_dest_type);
492  union_expr.move_to_operands(expr);
493  if(!src_type.full_eq(src_type_no_const))
494  do_typecast(union_expr.op0(), src_type_no_const);
495  union_expr.set(ID_component_name, comp.get_name());
496  expr=union_expr;
497  return; // ok
498  }
499  }
500  }
501 
502  if(dest_type.id()==ID_pointer)
503  {
504  // special case: 0 == NULL
505 
506  if(simplify_expr(expr, ns).is_zero() && (
507  src_type.id()==ID_unsignedbv ||
508  src_type.id()==ID_signedbv ||
509  src_type.id()==ID_natural ||
510  src_type.id()==ID_integer))
511  {
512  expr=exprt(ID_constant, orig_dest_type);
513  expr.set(ID_value, ID_NULL);
514  return; // ok
515  }
516 
517  if(src_type.id()==ID_pointer ||
518  src_type.id()==ID_array)
519  {
520  // we are quite generous about pointers
521 
522  const typet &src_sub=ns.follow(src_type.subtype());
523  const typet &dest_sub=ns.follow(dest_type.subtype());
524 
525  if(is_void_pointer(src_type) ||
526  is_void_pointer(dest_type))
527  {
528  // from/to void is always good
529  }
530  else if(src_sub.id()==ID_code &&
531  dest_sub.id()==ID_code)
532  {
533  // very generous:
534  // between any two function pointers it's ok
535  }
536  else if(base_type_eq(src_sub, dest_sub, ns))
537  {
538  // ok
539  }
540  else if((is_number(src_sub) ||
541  src_sub.id()==ID_c_enum ||
542  src_sub.id()==ID_c_enum_tag) &&
543  (is_number(dest_sub) ||
544  dest_sub.id()==ID_c_enum ||
545  src_sub.id()==ID_c_enum_tag))
546  {
547  // Also generous: between any to scalar types it's ok.
548  // We should probably check the size.
549  }
550  else
551  warnings.push_back("incompatible pointer types");
552 
553  // check qualifiers
554 
555  /*
556  if(src_type.subtype().get_bool(ID_C_constant) &&
557  !dest_type.subtype().get_bool(ID_C_constant))
558  warnings.push_back("disregarding const");
559  */
560 
561  if(src_type.subtype().get_bool(ID_C_volatile) &&
562  !dest_type.subtype().get_bool(ID_C_volatile))
563  warnings.push_back("disregarding volatile");
564 
565  if(src_type==dest_type)
566  {
567  expr.type()=src_type; // because of qualifiers
568  }
569  else
570  do_typecast(expr, orig_dest_type);
571 
572  return; // ok
573  }
574  }
575 
576  if(check_c_implicit_typecast(src_type, dest_type))
577  errors.push_back("implicit conversion not permitted");
578  else if(src_type!=dest_type)
579  do_typecast(expr, orig_dest_type);
580 }
581 
583  exprt &expr1,
584  exprt &expr2)
585 {
586  const typet &type1=ns.follow(expr1.type());
587  const typet &type2=ns.follow(expr2.type());
588 
589  c_typet c_type1=minimum_promotion(type1),
590  c_type2=minimum_promotion(type2);
591 
592  c_typet max_type=std::max(c_type1, c_type2);
593 
594  if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
595  {
596  // get the biggest width of both
597  std::size_t width1=type1.get_size_t(ID_width);
598  std::size_t width2=type2.get_size_t(ID_width);
599 
600  // produce type
601  typet result_type;
602 
603  if(width1==width2)
604  {
605  if(max_type==LARGE_SIGNED_INT)
606  result_type=signedbv_typet(width1);
607  else
608  result_type=unsignedbv_typet(width1);
609  }
610  else if(width1>width2)
611  result_type=type1;
612  else // width1<width2
613  result_type=type2;
614 
615  do_typecast(expr1, result_type);
616  do_typecast(expr2, result_type);
617 
618  return;
619  }
620  else if(max_type==FIXEDBV)
621  {
622  typet result_type;
623 
624  if(c_type1==FIXEDBV && c_type2==FIXEDBV)
625  {
626  // get bigger of both
627  std::size_t width1=to_fixedbv_type(type1).get_width();
628  std::size_t width2=to_fixedbv_type(type2).get_width();
629  if(width1>=width2)
630  result_type=type1;
631  else
632  result_type=type2;
633  }
634  else if(c_type1==FIXEDBV)
635  result_type=type1;
636  else
637  result_type=type2;
638 
639  do_typecast(expr1, result_type);
640  do_typecast(expr2, result_type);
641 
642  return;
643  }
644  else if(max_type==COMPLEX)
645  {
646  if(c_type1==COMPLEX && c_type2==COMPLEX)
647  {
648  // promote to the one with bigger subtype
649  if(get_c_type(type1.subtype())>get_c_type(type2.subtype()))
650  do_typecast(expr2, type1);
651  else
652  do_typecast(expr1, type2);
653  }
654  else if(c_type1==COMPLEX)
655  {
656  assert(c_type1==COMPLEX && c_type2!=COMPLEX);
657  do_typecast(expr2, type1.subtype());
658  do_typecast(expr2, type1);
659  }
660  else
661  {
662  assert(c_type1!=COMPLEX && c_type2==COMPLEX);
663  do_typecast(expr1, type2.subtype());
664  do_typecast(expr1, type2);
665  }
666 
667  return;
668  }
669  else if(max_type==SINGLE || max_type==DOUBLE ||
670  max_type==LONGDOUBLE || max_type==FLOAT128)
671  {
672  // Special-case optimisation:
673  // If we have two non-standard sized floats, don't do implicit type
674  // promotion if we can possibly avoid it.
675  if(type1==type2)
676  return;
677  }
678 
679  implicit_typecast_arithmetic(expr1, max_type);
680  implicit_typecast_arithmetic(expr2, max_type);
681 
682  // arithmetic typecasts only, otherwise this can't be used from
683  // typecheck_expr_trinary
684  #if 0
685  if(max_type==PTR)
686  {
687  if(c_type1==VOIDPTR)
688  do_typecast(expr1, expr2.type());
689 
690  if(c_type2==VOIDPTR)
691  do_typecast(expr2, expr1.type());
692  }
693  #endif
694 }
695 
696 void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
697 {
698  // special case: array -> pointer is actually
699  // something like address_of
700 
701  const typet &src_type=ns.follow(expr.type());
702 
703  if(src_type.id()==ID_array)
704  {
705  index_exprt index;
706  index.array()=expr;
707  index.index()=from_integer(0, index_type());
708  index.type()=src_type.subtype();
709  expr=address_of_exprt(index);
710  if(ns.follow(expr.type())!=ns.follow(dest_type))
711  expr.make_typecast(dest_type);
712  return;
713  }
714 
715  if(src_type!=dest_type)
716  {
717  // C booleans are special; we produce the
718  // explicit comparison with zero.
719  // Note that this requires ieee_float_notequal
720  // in case of floating-point numbers.
721 
722  if(dest_type.get(ID_C_c_type)==ID_bool)
723  {
724  expr=is_not_zero(expr, ns);
725  expr.make_typecast(dest_type);
726  }
727  else if(dest_type.id()==ID_bool)
728  {
729  expr=is_not_zero(expr, ns);
730  }
731  else
732  {
733  expr.make_typecast(dest_type);
734  }
735  }
736 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
unsigned int_width
Definition: config.h:30
Symbol table entry.
unsigned single_width
Definition: config.h:37
exprt & op0()
Definition: expr.h:84
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:270
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:696
Deprecated expression utility functions.
bool full_eq(const irept &other) const
Definition: irep.cpp:380
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
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:89
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
unsigned short_int_width
Definition: config.h:34
bitvector_typet double_type()
Definition: c_types.cpp:203
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Definition: c_typecast.cpp:461
typet & type()
Definition: expr.h:60
unsigned char_width
Definition: config.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
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:21
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
const irep_idt & id() const
Definition: irep.h:189
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:91
bitvector_typet float_type()
Definition: c_types.cpp:184
const namespacet & ns
Definition: c_typecast.h:65
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:75
unsigned long_long_int_width
Definition: config.h:35
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
std::list< std::string > warnings
Definition: c_typecast.h:62
void write(typet &src) const
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:79
Base class for tree-like data structures with sharing.
Definition: irep.h:87
std::list< std::string > errors
Definition: c_typecast.h:61
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:1319
bitvector_typet index_type()
Definition: c_types.cpp:15
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:253
Operator to return the address of an object.
Definition: std_expr.h:2593
std::size_t get_width() const
Definition: std_types.h:1030
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:222
Unbounded, signed integers.
Definition: std_types.h:69
typet type
Type of symbol.
Definition: symbol.h:37
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:441
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
bool is_number(const typet &type)
Definition: type.cpp:24
exprt & index()
Definition: std_expr.h:1208
Unbounded, signed real numbers.
Definition: std_types.h:99
Base class for all expressions.
Definition: expr.h:46
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:447
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:49
unsigned long_double_width
Definition: config.h:39
bool is_void_pointer(const typet &type)
Definition: c_typecast.cpp:58
unsigned double_width
Definition: config.h:38
bool is_zero() const
Definition: expr.cpp:236
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:100
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
void remove(const irep_namet &name)
Definition: irep.cpp:270
unsigned long_int_width
Definition: config.h:31
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:93
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:86
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:408
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
array index operator
Definition: std_expr.h:1170