CBMC
Loading...
Searching...
No Matches
c_typecast.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_typecast.h"
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/config.h>
14#include <util/expr_util.h>
16#include <util/namespace.h>
17#include <util/pointer_expr.h>
18#include <util/rational.h>
19#include <util/rational_tools.h>
20#include <util/simplify_expr.h>
21#include <util/std_expr.h>
22
23#include "c_qualifiers.h"
24
25#include <algorithm>
26
28 exprt &expr,
29 const typet &dest_type,
30 const namespacet &ns)
31{
33 c_typecast.implicit_typecast(expr, dest_type);
34 return !c_typecast.errors.empty();
35}
36
38 const typet &src_type,
39 const typet &dest_type,
40 const namespacet &ns)
41{
43 exprt tmp;
44 tmp.type()=src_type;
45 c_typecast.implicit_typecast(tmp, dest_type);
46 return !c_typecast.errors.empty();
47}
48
52 const namespacet &ns)
53{
55 c_typecast.implicit_typecast_arithmetic(expr1, expr2);
56 return !c_typecast.errors.empty();
57}
58
59bool has_a_void_pointer(const typet &type)
60{
61 if(type.id()==ID_pointer)
62 {
63 const auto &pointer_type = to_pointer_type(type);
64
65 if(pointer_type.base_type().id() == ID_empty)
66 return true;
67
69 }
70 else
71 return false;
72}
73
75 const typet &src_type,
76 const typet &dest_type)
77{
78 // check qualifiers
79
80 if(
81 src_type.id() == ID_pointer && dest_type.id() == ID_pointer &&
82 to_pointer_type(src_type).base_type().get_bool(ID_C_constant) &&
83 !to_pointer_type(dest_type).base_type().get_bool(ID_C_constant))
84 {
85 return true;
86 }
87
89 return false;
90
91 const irep_idt &src_type_id=src_type.id();
92
94 {
96 to_c_bit_field_type(src_type).underlying_type(), dest_type);
97 }
98
100 {
102 src_type, to_c_bit_field_type(dest_type).underlying_type());
103 }
104
106 {
107 if(
108 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
109 dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
110 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
111 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
112 dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
113 {
114 return false;
115 }
116 }
117 else if(src_type_id==ID_integer)
118 {
119 if(
120 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
121 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
122 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
123 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
124 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
125 dest_type.id() == ID_pointer || dest_type.id() == ID_complex)
126 {
127 return false;
128 }
129 }
130 else if(src_type_id==ID_real)
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_rational)
141 {
142 if(
143 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
144 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
145 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
146 dest_type.id() == ID_complex)
147 {
148 return false;
149 }
150 }
151 else if(src_type_id==ID_bool)
152 {
153 if(
154 dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
155 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
156 dest_type.id() == ID_real || dest_type.id() == ID_unsignedbv ||
157 dest_type.id() == ID_signedbv || dest_type.id() == ID_pointer ||
158 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
159 dest_type.id() == ID_c_enum || dest_type.id() == ID_c_enum_tag ||
160 dest_type.id() == ID_complex)
161 {
162 return false;
163 }
164 }
165 else if(src_type_id==ID_unsignedbv ||
170 {
171 if(
172 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_bool ||
173 dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
174 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
175 dest_type.id() == ID_real || dest_type.id() == ID_signedbv ||
176 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
177 dest_type.id() == ID_pointer || dest_type.id() == ID_c_enum ||
178 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_complex)
179 {
180 return false;
181 }
182 }
183 else if(src_type_id==ID_floatbv ||
185 {
186 if(dest_type.id()==ID_bool ||
187 dest_type.id()==ID_c_bool ||
188 dest_type.id()==ID_integer ||
189 dest_type.id()==ID_real ||
190 dest_type.id()==ID_rational ||
191 dest_type.id()==ID_signedbv ||
192 dest_type.id()==ID_unsignedbv ||
193 dest_type.id()==ID_floatbv ||
194 dest_type.id()==ID_fixedbv ||
195 dest_type.id()==ID_complex)
196 return false;
197 }
198 else if(src_type_id==ID_complex)
199 {
200 if(dest_type.id()==ID_complex)
201 {
203 to_complex_type(src_type).subtype(),
204 to_complex_type(dest_type).subtype());
205 }
206 else
207 {
208 // 6.3.1.7, par 2:
209
210 // When a value of complex type is converted to a real type, the
211 // imaginary part of the complex value is discarded and the value of the
212 // real part is converted according to the conversion rules for the
213 // corresponding real type.
214
217 }
218 }
219 else if(src_type_id==ID_array ||
221 {
222 if(dest_type.id()==ID_pointer)
223 {
224 const irept &dest_subtype = to_pointer_type(dest_type).base_type();
226
228 {
229 return false;
230 }
231 else if(
232 has_a_void_pointer(src_type) || // from void to anything
233 has_a_void_pointer(dest_type)) // to void from anything
234 {
235 return false;
236 }
237 }
238
239 if(
240 dest_type.id() == ID_array && to_type_with_subtype(src_type).subtype() ==
241 to_array_type(dest_type).element_type())
242 {
243 return false;
244 }
245
246 if(dest_type.id()==ID_bool ||
247 dest_type.id()==ID_c_bool ||
248 dest_type.id()==ID_unsignedbv ||
250 return false;
251 }
252 else if(src_type_id==ID_vector)
253 {
254 if(dest_type.id()==ID_vector)
255 return false;
256 }
257 else if(src_type_id==ID_complex)
258 {
259 if(dest_type.id()==ID_complex)
260 {
261 // We convert between complex types if we convert between
262 // their component types.
264 to_complex_type(src_type).subtype(),
265 to_complex_type(dest_type).subtype()))
266 {
267 return false;
268 }
269 }
270 }
271
272 return true;
273}
274
276{
277 if(
278 src_type.id() != ID_struct_tag &&
279 src_type.id() != ID_union_tag)
280 {
281 return src_type;
282 }
283
284 typet result_type=src_type;
285
286 // collect qualifiers
288
289 if(
291 {
292 const typet &followed_type = ns.follow_tag(*struct_tag_type);
293 result_type = followed_type;
295 }
296 else if(
298 {
299 const typet &followed_type = ns.follow_tag(*union_tag_type);
300 result_type = followed_type;
302 }
303
304 qualifiers.write(result_type);
305
306 return result_type;
307}
308
310 const typet &type) const
311{
312 if(type.id()==ID_signedbv)
313 {
314 const std::size_t width = to_bitvector_type(type).get_width();
315
316 if(width<=config.ansi_c.char_width)
317 return CHAR;
318 else if(width<=config.ansi_c.short_int_width)
319 return SHORT;
320 else if(width<=config.ansi_c.int_width)
321 return INT;
322 else if(width<=config.ansi_c.long_int_width)
323 return LONG;
324 else if(width<=config.ansi_c.long_long_int_width)
325 return LONGLONG;
326 else
327 return LARGE_SIGNED_INT;
328 }
329 else if(type.id()==ID_unsignedbv)
330 {
331 const std::size_t width = to_bitvector_type(type).get_width();
332
333 if(width<=config.ansi_c.char_width)
334 return UCHAR;
335 else if(width<=config.ansi_c.short_int_width)
336 return USHORT;
337 else if(width<=config.ansi_c.int_width)
338 return UINT;
339 else if(width<=config.ansi_c.long_int_width)
340 return ULONG;
341 else if(width<=config.ansi_c.long_long_int_width)
342 return ULONGLONG;
343 else
344 return LARGE_UNSIGNED_INT;
345 }
346 else if(type.id()==ID_bool)
347 return BOOL;
348 else if(type.id()==ID_c_bool)
349 return BOOL;
350 else if(type.id()==ID_floatbv)
351 {
352 const std::size_t width = to_bitvector_type(type).get_width();
353
354 if(width<=config.ansi_c.single_width)
355 return SINGLE;
356 else if(width<=config.ansi_c.double_width)
357 return DOUBLE;
358 else if(width<=config.ansi_c.long_double_width)
359 return LONGDOUBLE;
360 else if(width<=128)
361 return FLOAT128;
362 }
363 else if(type.id()==ID_fixedbv)
364 {
365 return FIXEDBV;
366 }
367 else if(type.id()==ID_pointer)
368 {
369 if(to_pointer_type(type).base_type().id() == ID_empty)
370 return VOIDPTR;
371 else
372 return PTR;
373 }
374 else if(type.id()==ID_array)
375 {
376 return PTR;
377 }
378 else if(type.id() == ID_c_enum || type.id() == ID_c_enum_tag)
379 {
380 return INT;
381 }
382 else if(type.id()==ID_rational)
383 return RATIONAL;
384 else if(type.id()==ID_real)
385 return REAL;
386 else if(type.id()==ID_complex)
387 return COMPLEX;
388 else if(type.id()==ID_c_bit_field)
389 {
390 const auto &bit_field_type = to_c_bit_field_type(type);
391
392 // We take the underlying type, and then apply the number
393 // of bits given
394 typet underlying_type;
395
396 if(bit_field_type.underlying_type().id() == ID_c_enum_tag)
397 {
398 const auto &followed =
399 ns.follow_tag(to_c_enum_tag_type(bit_field_type.underlying_type()));
400 if(followed.is_incomplete())
401 return INT;
402 else
403 underlying_type = followed.underlying_type();
404 }
405 else
406 underlying_type = bit_field_type.underlying_type();
407
409 underlying_type.id(), bit_field_type.get_width());
410
411 return get_c_type(new_type);
412 }
413 else if(type.id() == ID_integer)
414 return INTEGER;
415 else if(type.id() == ID_natural)
416 return NATURAL;
417
418 return OTHER;
419}
420
422 exprt &expr,
424{
426
427 switch(c_type)
428 {
429 case PTR:
430 if(expr.type().id() == ID_array)
431 {
432 new_type = pointer_type(to_array_type(expr.type()).element_type());
433 break;
434 }
435 return;
436
437 case BOOL: UNREACHABLE; // should always be promoted to int
438 case CHAR: UNREACHABLE; // should always be promoted to int
439 case UCHAR: UNREACHABLE; // should always be promoted to int
440 case SHORT: UNREACHABLE; // should always be promoted to int
441 case USHORT: UNREACHABLE; // should always be promoted to int
442 case INT: new_type=signed_int_type(); break;
443 case UINT: new_type=unsigned_int_type(); break;
444 case LONG: new_type=signed_long_int_type(); break;
448 case SINGLE: new_type=float_type(); break;
449 case DOUBLE: new_type=double_type(); break;
450 case LONGDOUBLE: new_type=long_double_type(); break;
451 // NOLINTNEXTLINE(whitespace/line_length)
453 case RATIONAL: new_type=rational_typet(); break;
454 case REAL: new_type=real_typet(); break;
455 case INTEGER: new_type=integer_typet(); break;
456 case NATURAL:
458 break;
459 case COMPLEX:
460 case OTHER:
461 case VOIDPTR:
462 case FIXEDBV:
464 case LARGE_SIGNED_INT:
465 return; // do nothing
466 }
467
468 if(new_type != expr.type())
469 do_typecast(expr, new_type);
470}
471
473 const typet &type) const
474{
476
477 // 6.3.1.1, par 2
478
479 // "If an int can represent all values of the original type, the
480 // value is converted to an int; otherwise, it is converted to
481 // an unsigned int."
482
483 c_typet max_type=std::max(c_type, INT); // minimum promotion
484
485 // The second case can arise if we promote any unsigned type
486 // that is as large as unsigned int. In this case the promotion configuration
487 // via the enum is actually wrong, and we need to fix this up.
488 if(
489 config.ansi_c.short_int_width == config.ansi_c.int_width &&
490 c_type == USHORT)
492 else if(
493 config.ansi_c.char_width == config.ansi_c.int_width && c_type == UCHAR)
495
496 if(max_type==UINT &&
497 type.id()==ID_c_bit_field &&
498 to_c_bit_field_type(type).get_width()<config.ansi_c.int_width)
500
501 return max_type;
502}
503
509
523
525 exprt &expr,
526 const typet &src_type,
527 const typet &orig_dest_type,
528 const typet &dest_type)
529{
530 // do transparent union
531 if(dest_type.id()==ID_union &&
533 src_type.id()!=ID_union)
534 {
535 // The argument corresponding to a transparent union type can be of any
536 // type in the union; no explicit cast is required.
537
538 // GCC docs say:
539 // If the union member type is a pointer, qualifiers like const on the
540 // referenced type must be respected, just as with normal pointer
541 // conversions.
542 // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
544 if(
545 src_type.id() == ID_pointer &&
546 to_pointer_type(src_type).base_type().get_bool(ID_C_constant))
547 {
549 }
550
551 // Check union members.
552 for(const auto &comp : to_union_type(dest_type).components())
553 {
555 {
556 // build union constructor
557 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
558 if(!src_type.full_eq(src_type_no_const))
560 expr=union_expr;
561 return; // ok
562 }
563 }
564 }
565
566 if(dest_type.id()==ID_pointer)
567 {
568 // special case: 0 == NULL
569
570 if(simplify_expr(expr, ns).is_zero() && (
571 src_type.id()==ID_unsignedbv ||
572 src_type.id()==ID_signedbv ||
573 src_type.id()==ID_natural ||
574 src_type.id()==ID_integer))
575 {
577 return; // ok
578 }
579
580 if(src_type.id()==ID_pointer ||
581 src_type.id()==ID_array)
582 {
583 // we are quite generous about pointers
584
585 const typet &src_sub = to_type_with_subtype(src_type).subtype();
586 const typet &dest_sub = to_pointer_type(dest_type).base_type();
587
589 {
590 // from/to void is always good
591 }
592 else if(src_sub.id()==ID_code &&
593 dest_sub.id()==ID_code)
594 {
595 // very generous:
596 // between any two function pointers it's ok
597 }
598 else if(src_sub == dest_sub)
599 {
600 // ok
601 }
602 else if((is_number(src_sub) ||
603 src_sub.id()==ID_c_enum ||
604 src_sub.id()==ID_c_enum_tag) &&
606 dest_sub.id()==ID_c_enum ||
607 src_sub.id()==ID_c_enum_tag))
608 {
609 // Also generous: between any to scalar types it's ok.
610 // We should probably check the size.
611 }
612 else if(
613 src_sub.id() == ID_array && dest_sub.id() == ID_array &&
614 to_array_type(src_sub).element_type() ==
615 to_array_type(dest_sub).element_type())
616 {
617 // we ignore the size of the top-level array
618 // in the case of pointers to arrays
619 }
620 else
621 warnings.push_back("incompatible pointer types");
622
623 // check qualifiers
624
625 if(
626 to_type_with_subtype(src_type).subtype().get_bool(ID_C_volatile) &&
627 !to_pointer_type(dest_type).base_type().get_bool(ID_C_volatile))
628 {
629 warnings.push_back("disregarding volatile");
630 }
631
633 {
634 expr.type()=src_type; // because of qualifiers
635 }
636 else
638
639 return; // ok
640 }
641 }
642
644 errors.push_back("implicit conversion not permitted");
645 else if(src_type!=dest_type)
647}
648
650 exprt &expr1,
651 exprt &expr2)
652{
653 const typet &type1 = expr1.type();
654 const typet &type2 = expr2.type();
655
658
659 c_typet max_type=std::max(c_type1, c_type2);
660
662 {
663 // produce type
664 typet result_type = (max_type == c_type1) ? type1 : type2;
665
666 do_typecast(expr1, result_type);
667 do_typecast(expr2, result_type);
668
669 return;
670 }
671 else if(max_type==FIXEDBV)
672 {
673 typet result_type;
674
676 {
677 // get bigger of both
678 std::size_t width1=to_fixedbv_type(type1).get_width();
679 std::size_t width2=to_fixedbv_type(type2).get_width();
680 if(width1>=width2)
681 result_type=type1;
682 else
683 result_type=type2;
684 }
685 else if(c_type1==FIXEDBV)
686 result_type=type1;
687 else
688 result_type=type2;
689
690 do_typecast(expr1, result_type);
691 do_typecast(expr2, result_type);
692
693 return;
694 }
695 else if(max_type==COMPLEX)
696 {
698 {
699 // promote to the one with bigger subtype
700 if(
701 get_c_type(to_complex_type(type1).subtype()) >
702 get_c_type(to_complex_type(type2).subtype()))
703 {
705 }
706 else
708 }
709 else if(c_type1==COMPLEX)
710 {
711 INVARIANT(c_type2 != COMPLEX, "both types were COMPLEX");
714 }
715 else
716 {
717 INVARIANT(c_type2 == COMPLEX, "neither type was COMPLEX");
720 }
721
722 return;
723 }
724 else if(max_type==SINGLE || max_type==DOUBLE ||
726 {
727 // Special-case optimisation:
728 // If we have two non-standard sized floats, don't do implicit type
729 // promotion if we can possibly avoid it.
730 if(type1==type2)
731 return;
732 }
733 else if(max_type == OTHER)
734 {
735 errors.push_back("implicit arithmetic conversion not permitted");
736 return;
737 }
738
741}
742
744{
745 // special case: array -> pointer is actually
746 // something like address_of
747
748 const typet &src_type = expr.type();
749
750 if(src_type.id()==ID_array)
751 {
752 // This is the promotion from an array
753 // to a pointer to the first element.
755 if(error_opt.has_value())
756 {
757 errors.push_back(error_opt.value());
758 return;
759 }
760
761 index_exprt index(expr, from_integer(0, c_index_type()));
763 return;
764 }
765
767 {
768 // C booleans are special; we produce the
769 // explicit comparison with zero.
770 // Note that this requires ieee_float_notequal
771 // in case of floating-point numbers.
772
774 {
775 expr = typecast_exprt(is_not_zero(expr, ns), dest_type);
776 }
777 else if(dest_type.id()==ID_bool)
778 {
779 expr=is_not_zero(expr, ns);
780 }
781 else if(dest_type.id() == ID_rational)
782 {
784 {
785 auto op1 = numeric_cast<mp_integer>(div_expr->lhs());
786 auto op2 = numeric_cast<mp_integer>(div_expr->rhs());
787 if(op1.has_value() && op2.has_value())
788 {
789 rationalt numerator{*op1};
790 expr = from_rational(rationalt{*op1} / rationalt{*op2});
791 return;
792 }
793 }
794 else if(auto int_const = numeric_cast<mp_integer>(expr))
795 {
797 return;
798 }
799
800 expr = typecast_exprt(expr, dest_type);
801 }
802 else
803 {
804 expr = typecast_exprt(expr, dest_type);
805 }
806 }
807}
808
809std::optional<std::string>
811{
812 if(type.id() == ID_c_bit_field)
813 return std::string("cannot take address of a bit field");
814
815 if(type.id() == ID_bool)
816 return std::string("cannot take address of a proper Boolean");
817
819 {
820 // The width of the bitvector must be a multiple of CHAR_BIT.
821 auto width = to_bitvector_type(type).get_width();
822 if(width % config.ansi_c.char_width != 0)
823 {
824 return std::string(
825 "bitvector must have width that is a multiple of CHAR_BIT");
826 }
827 else
828 return {};
829 }
830
831 if(type.id() == ID_array)
832 return check_address_can_be_taken(to_array_type(type).element_type());
833
834 return {}; // ok
835}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
bool has_a_void_pointer(const typet &type)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
floatbv_typet float_type()
Definition c_types.cpp:177
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:93
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
floatbv_typet long_double_type()
Definition c_types.cpp:193
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:185
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:80
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:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class of fixed-width bit-vector types.
Definition std_types.h:909
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:92
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
virtual void implicit_typecast(exprt &expr, const typet &type)
c_typet get_c_type(const typet &type) const
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< std::string > warnings
Definition c_typecast.h:67
const namespacet & ns
Definition c_typecast.h:74
static std::optional< std::string > check_address_can_be_taken(const typet &)
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:66
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:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:82
Array index operator.
Definition std_expr.h:1470
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:364
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Natural numbers including zero (mathematical integers, not bitvectors)
The null pointer constant.
const typet & base_type() const
The type of the data what we point to.
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1770
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:69
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
constant_exprt from_rational(const rationalt &a)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208