cprover
c_typecheck_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "c_typecheck_base.h"
13
14#include <unordered_set>
15
17
18#include <util/arith_tools.h>
19#include <util/c_types.h>
20#include <util/config.h>
21#include <util/fresh_symbol.h>
23#include <util/pointer_expr.h>
25#include <util/simplify_expr.h>
26
27#include "ansi_c_convert_type.h"
28#include "ansi_c_declaration.h"
29#include "c_qualifiers.h"
30#include "gcc_types.h"
31#include "padding.h"
32#include "type2name.h"
33#include "typedef_type.h"
34
36{
37 // we first convert, and then check
38 {
39 ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
40
41 ansi_c_convert_type.read(type);
42 ansi_c_convert_type.write(type);
43 }
44
45 if(type.id()==ID_already_typechecked)
46 {
47 already_typechecked_typet &already_typechecked =
49
50 // need to preserve any qualifiers
51 c_qualifierst c_qualifiers(type);
52 c_qualifiers += c_qualifierst(already_typechecked.get_type());
53 bool packed=type.get_bool(ID_C_packed);
54 exprt alignment=static_cast<const exprt &>(type.find(ID_C_alignment));
55 irept _typedef=type.find(ID_C_typedef);
56
57 type = already_typechecked.get_type();
58
59 c_qualifiers.write(type);
60 if(packed)
61 type.set(ID_C_packed, true);
62 if(alignment.is_not_nil())
63 type.add(ID_C_alignment, alignment);
64 if(_typedef.is_not_nil())
65 type.add(ID_C_typedef, _typedef);
66
67 return; // done
68 }
69
70 // do we have alignment?
71 if(type.find(ID_C_alignment).is_not_nil())
72 {
73 exprt &alignment=static_cast<exprt &>(type.add(ID_C_alignment));
74 if(alignment.id()!=ID_default)
75 {
78 }
79 }
80
81 if(type.id()==ID_code)
83 else if(type.id()==ID_array)
85 else if(type.id()==ID_pointer)
86 {
87 typecheck_type(type.subtype());
89 to_bitvector_type(type).get_width() > 0, "pointers must have width");
90 }
91 else if(type.id()==ID_struct ||
92 type.id()==ID_union)
94 else if(type.id()==ID_c_enum)
96 else if(type.id()==ID_c_enum_tag)
98 else if(type.id()==ID_c_bit_field)
100 else if(type.id()==ID_typeof)
102 else if(type.id() == ID_typedef_type)
104 else if(type.id() == ID_struct_tag ||
105 type.id() == ID_union_tag)
106 {
107 // nothing to do, these stay as is
108 }
109 else if(type.id()==ID_vector)
110 {
111 // already done
112 }
113 else if(type.id() == ID_frontend_vector)
114 {
116 }
117 else if(type.id()==ID_custom_unsignedbv ||
118 type.id()==ID_custom_signedbv ||
119 type.id()==ID_custom_floatbv ||
120 type.id()==ID_custom_fixedbv)
122 else if(type.id()==ID_gcc_attribute_mode)
123 {
124 // get that mode
125 const irep_idt gcc_attr_mode = type.get(ID_size);
126
127 // A list of all modes is at
128 // http://www.delorie.com/gnu/docs/gcc/gccint_53.html
129 typecheck_type(type.subtype());
130
131 typet underlying_type=type.subtype();
132
133 // gcc allows this, but clang doesn't; it's a compiler hint only,
134 // but we'll try to interpret it the GCC way
135 if(underlying_type.id()==ID_c_enum_tag)
136 {
137 underlying_type =
138 follow_tag(to_c_enum_tag_type(underlying_type)).underlying_type();
139
140 assert(underlying_type.id()==ID_signedbv ||
141 underlying_type.id()==ID_unsignedbv);
142 }
143
144 if(underlying_type.id()==ID_signedbv ||
145 underlying_type.id()==ID_unsignedbv)
146 {
147 bool is_signed=underlying_type.id()==ID_signedbv;
148
150
151 if(gcc_attr_mode == "__QI__") // 8 bits
152 {
153 if(is_signed)
155 else
157 }
158 else if(gcc_attr_mode == "__byte__") // 8 bits
159 {
160 if(is_signed)
162 else
164 }
165 else if(gcc_attr_mode == "__HI__") // 16 bits
166 {
167 if(is_signed)
169 else
171 }
172 else if(gcc_attr_mode == "__SI__") // 32 bits
173 {
174 if(is_signed)
176 else
178 }
179 else if(gcc_attr_mode == "__word__") // long int, we think
180 {
181 if(is_signed)
183 else
185 }
186 else if(gcc_attr_mode == "__pointer__") // size_t/ssize_t, we think
187 {
188 if(is_signed)
190 else
192 }
193 else if(gcc_attr_mode == "__DI__") // 64 bits
194 {
196 {
197 if(is_signed)
199 else
201 }
202 else
203 {
205
206 if(is_signed)
208 else
210 }
211 }
212 else if(gcc_attr_mode == "__TI__") // 128 bits
213 {
214 if(is_signed)
216 else
218 }
219 else if(gcc_attr_mode == "__V2SI__") // vector of 2 ints, deprecated
220 {
221 if(is_signed)
224 from_integer(2, size_type()));
225 else
228 from_integer(2, size_type()));
229 }
230 else if(gcc_attr_mode == "__V4SI__") // vector of 4 ints, deprecated
231 {
232 if(is_signed)
235 from_integer(4, size_type()));
236 else
239 from_integer(4, size_type()));
240 }
241 else // give up, just use subtype
242 result=type.subtype();
243
244 // save the location
245 result.add_source_location()=type.source_location();
246
247 if(type.subtype().id()==ID_c_enum_tag)
248 {
249 const irep_idt &tag_name=
252 }
253
254 type=result;
255 }
256 else if(underlying_type.id()==ID_floatbv)
257 {
259
260 if(gcc_attr_mode == "__SF__") // 32 bits
262 else if(gcc_attr_mode == "__DF__") // 64 bits
264 else if(gcc_attr_mode == "__TF__") // 128 bits
266 else if(gcc_attr_mode == "__V2SF__") // deprecated vector of 2 floats
268 else if(gcc_attr_mode == "__V2DF__") // deprecated vector of 2 doubles
270 else if(gcc_attr_mode == "__V4SF__") // deprecated vector of 4 floats
272 else if(gcc_attr_mode == "__V4DF__") // deprecated vector of 4 doubles
274 else // give up, just use subtype
275 result=type.subtype();
276
277 // save the location
278 result.add_source_location()=type.source_location();
279
280 type=result;
281 }
282 else if(underlying_type.id()==ID_complex)
283 {
284 // gcc allows this, but clang doesn't -- see enums above
286
287 if(gcc_attr_mode == "__SC__") // 32 bits
289 else if(gcc_attr_mode == "__DC__") // 64 bits
291 else if(gcc_attr_mode == "__TC__") // 128 bits
293 else // give up, just use subtype
294 result=type.subtype();
295
296 // save the location
297 result.add_source_location()=type.source_location();
298
299 type=complex_typet(result);
300 }
301 else
302 {
304 error() << "attribute mode '" << gcc_attr_mode
305 << "' applied to inappropriate type '" << to_string(type) << "'"
306 << eom;
307 throw 0;
308 }
309 }
310
311 // do a mild bit of rule checking
312
313 if(type.get_bool(ID_C_restricted) &&
314 type.id()!=ID_pointer &&
315 type.id()!=ID_array)
316 {
318 error() << "only a pointer can be 'restrict'" << eom;
319 throw 0;
320 }
321}
322
324{
325 // they all have a width
326 exprt size_expr=
327 static_cast<const exprt &>(type.find(ID_size));
328
329 typecheck_expr(size_expr);
330 source_locationt source_location=size_expr.source_location();
331 make_constant_index(size_expr);
332
333 mp_integer size_int;
334 if(to_integer(to_constant_expr(size_expr), size_int))
335 {
336 error().source_location=source_location;
337 error() << "failed to convert bit vector width to constant" << eom;
338 throw 0;
339 }
340
341 if(size_int<1)
342 {
343 error().source_location=source_location;
344 error() << "bit vector width invalid" << eom;
345 throw 0;
346 }
347
348 type.remove(ID_size);
349 type.set(ID_width, integer2string(size_int));
350
351 // depending on type, there may be a number of fractional bits
352
353 if(type.id()==ID_custom_unsignedbv)
354 type.id(ID_unsignedbv);
355 else if(type.id()==ID_custom_signedbv)
356 type.id(ID_signedbv);
357 else if(type.id()==ID_custom_fixedbv)
358 {
359 type.id(ID_fixedbv);
360
361 exprt f_expr=
362 static_cast<const exprt &>(type.find(ID_f));
363
364 const source_locationt fraction_source_location =
365 f_expr.find_source_location();
366
367 typecheck_expr(f_expr);
368
369 make_constant_index(f_expr);
370
371 mp_integer f_int;
372 if(to_integer(to_constant_expr(f_expr), f_int))
373 {
374 error().source_location = fraction_source_location;
375 error() << "failed to convert number of fraction bits to constant" << eom;
376 throw 0;
377 }
378
379 if(f_int<0 || f_int>size_int)
380 {
381 error().source_location = fraction_source_location;
382 error() << "fixedbv fraction width invalid" << eom;
383 throw 0;
384 }
385
386 type.remove(ID_f);
387 type.set(ID_integer_bits, integer2string(size_int-f_int));
388 }
389 else if(type.id()==ID_custom_floatbv)
390 {
391 type.id(ID_floatbv);
392
393 exprt f_expr=
394 static_cast<const exprt &>(type.find(ID_f));
395
396 const source_locationt fraction_source_location =
397 f_expr.find_source_location();
398
399 typecheck_expr(f_expr);
400
401 make_constant_index(f_expr);
402
403 mp_integer f_int;
404 if(to_integer(to_constant_expr(f_expr), f_int))
405 {
406 error().source_location = fraction_source_location;
407 error() << "failed to convert number of fraction bits to constant" << eom;
408 throw 0;
409 }
410
411 if(f_int<1 || f_int+1>=size_int)
412 {
413 error().source_location = fraction_source_location;
414 error() << "floatbv fraction width invalid" << eom;
415 throw 0;
416 }
417
418 type.remove(ID_f);
419 type.set(ID_f, integer2string(f_int));
420 }
421 else
423}
424
426{
427 // the return type is still 'subtype()'
428 type.return_type()=type.subtype();
429 type.remove_subtype();
430
431 code_typet::parameterst &parameters=type.parameters();
432
433 // if we don't have any parameters, we assume it's (...)
434 if(parameters.empty())
435 {
436 type.make_ellipsis();
437 }
438 else // we do have parameters
439 {
440 // is the last one ellipsis?
441 if(type.parameters().back().id()==ID_ellipsis)
442 {
443 type.make_ellipsis();
444 type.parameters().pop_back();
445 }
446
447 parameter_map.clear();
448
449 for(auto &param : type.parameters())
450 {
451 // turn the declarations into parameters
452 if(param.id()==ID_declaration)
453 {
454 ansi_c_declarationt &declaration=
456
457
458 // first fix type
459 code_typet::parametert parameter(
460 declaration.full_type(declaration.declarator()));
461 typet &param_type = parameter.type();
462 std::list<codet> tmp_clean_code;
463 tmp_clean_code.swap(clean_code); // ignore side-effects
464 typecheck_type(param_type);
465 tmp_clean_code.swap(clean_code);
466 adjust_function_parameter(param_type);
467
468 // adjust the identifier
469 irep_idt identifier=declaration.declarator().get_name();
470
471 // abstract or not?
472 if(identifier.empty())
473 {
474 // abstract
475 parameter.add_source_location()=declaration.type().source_location();
476 }
477 else
478 {
479 // make visible now, later parameters might use it
480 parameter_map[identifier] = param_type;
481 parameter.set_base_name(declaration.declarator().get_base_name());
482 parameter.add_source_location()=
483 declaration.declarator().source_location();
484 }
485
486 // put the parameter in place of the declaration
487 param.swap(parameter);
488 }
489 }
490
491 parameter_map.clear();
492
493 if(parameters.size() == 1 && parameters[0].type().id() == ID_empty)
494 {
495 // if we just have one parameter of type void, remove it
496 parameters.clear();
497 }
498 }
499
501
502 // 6.7.6.3:
503 // "A function declarator shall not specify a return type that
504 // is a function type or an array type."
505
506 const typet &decl_return_type = type.return_type();
507
508 if(decl_return_type.id() == ID_array)
509 {
511 error() << "function must not return array" << eom;
512 throw 0;
513 }
514
515 if(decl_return_type.id() == ID_code)
516 {
518 error() << "function must not return function type" << eom;
519 throw 0;
520 }
521}
522
524{
525 exprt &size=type.size();
526 const source_locationt size_source_location = size.find_source_location();
527
528 // check subtype
530
531 // we don't allow void as subtype
532 if(type.element_type().id() == ID_empty)
533 {
535 error() << "array of voids" << eom;
536 throw 0;
537 }
538
539 // we don't allow incomplete structs or unions as subtype
540 const typet &followed_subtype = follow(type.element_type());
541
542 if(
543 (followed_subtype.id() == ID_struct || followed_subtype.id() == ID_union) &&
544 to_struct_union_type(followed_subtype).is_incomplete())
545 {
546 // ISO/IEC 9899 6.7.5.2
548 error() << "array has incomplete element type" << eom;
549 throw 0;
550 }
551
552 // we don't allow functions as subtype
553 if(type.element_type().id() == ID_code)
554 {
555 // ISO/IEC 9899 6.7.5.2
557 error() << "array of function element type" << eom;
558 throw 0;
559 }
560
561 // check size, if any
562
563 if(size.is_not_nil())
564 {
565 typecheck_expr(size);
566 make_index_type(size);
567
568 // The size need not be a constant!
569 // We simplify it, for the benefit of array initialisation.
570
571 exprt tmp_size=size;
572 add_rounding_mode(tmp_size);
573 simplify(tmp_size, *this);
574
575 if(tmp_size.is_constant())
576 {
577 mp_integer s;
578 if(to_integer(to_constant_expr(tmp_size), s))
579 {
580 error().source_location = size_source_location;
581 error() << "failed to convert constant: "
582 << tmp_size.pretty() << eom;
583 throw 0;
584 }
585
586 if(s<0)
587 {
588 error().source_location = size_source_location;
589 error() << "array size must not be negative, "
590 "but got " << s << eom;
591 throw 0;
592 }
593
594 size=tmp_size;
595 }
596 else if(tmp_size.id()==ID_infinity)
597 {
598 size=tmp_size;
599 }
600 else if(tmp_size.id()==ID_symbol &&
601 tmp_size.type().get_bool(ID_C_constant))
602 {
603 // We allow a constant variable as array size, assuming
604 // it won't change.
605 // This criterion can be tricked:
606 // Of course we can modify a 'const' symbol, e.g.,
607 // using a pointer type cast. Interestingly,
608 // at least gcc 4.2.1 makes the very same mistake!
609 size=tmp_size;
610 }
611 else
612 {
613 // not a constant and not infinity
614
616
618 {
620 error() << "array size of static symbol '" << current_symbol.base_name
621 << "' is not constant" << eom;
622 throw 0;
623 }
624
625 symbolt &new_symbol = get_fresh_aux_symbol(
626 size_type(),
627 id2string(current_symbol.name) + "$array_size",
628 id2string(current_symbol.base_name) + "$array_size",
629 size_source_location,
630 mode,
632 new_symbol.type.set(ID_C_constant, true);
634
635 // produce the code that declares and initializes the symbol
636 symbol_exprt symbol_expr = new_symbol.symbol_expr();
637
638 code_frontend_declt declaration(symbol_expr);
639 declaration.add_source_location() = size_source_location;
640
641 code_frontend_assignt assignment;
642 assignment.lhs()=symbol_expr;
643 assignment.rhs() = new_symbol.value;
644 assignment.add_source_location() = size_source_location;
645
646 // store the code
647 clean_code.push_back(declaration);
648 clean_code.push_back(assignment);
649
650 // fix type
651 size=symbol_expr;
652 }
653 }
654}
655
657{
658 // This turns the type with ID_frontend_vector into the type
659 // with ID_vector; the difference is that the latter has
660 // a constant as size, which we establish now.
661 exprt size = static_cast<const exprt &>(type.find(ID_size));
662 const source_locationt source_location = size.find_source_location();
663
664 typecheck_expr(size);
665
666 typet subtype = type.subtype();
667 typecheck_type(subtype);
668
669 // we are willing to combine 'vector' with various
670 // other types, but not everything!
671
672 if(subtype.id()!=ID_signedbv &&
673 subtype.id()!=ID_unsignedbv &&
674 subtype.id()!=ID_floatbv &&
675 subtype.id()!=ID_fixedbv)
676 {
677 error().source_location=source_location;
678 error() << "cannot make a vector of subtype "
679 << to_string(subtype) << eom;
680 throw 0;
681 }
682
684
685 mp_integer s;
686 if(to_integer(to_constant_expr(size), s))
687 {
688 error().source_location=source_location;
689 error() << "failed to convert constant: "
690 << size.pretty() << eom;
691 throw 0;
692 }
693
694 if(s<=0)
695 {
696 error().source_location=source_location;
697 error() << "vector size must be positive, "
698 "but got " << s << eom;
699 throw 0;
700 }
701
702 // the subtype must have constant size
703 auto sub_size_expr_opt = size_of_expr(subtype, *this);
704
705 if(!sub_size_expr_opt.has_value())
706 {
707 error().source_location = source_location;
708 error() << "failed to determine size of vector base type '"
709 << to_string(subtype) << "'" << eom;
710 throw 0;
711 }
712
713 simplify(sub_size_expr_opt.value(), *this);
714
715 const auto sub_size = numeric_cast<mp_integer>(sub_size_expr_opt.value());
716
717 if(!sub_size.has_value())
718 {
719 error().source_location=source_location;
720 error() << "failed to determine size of vector base type '"
721 << to_string(subtype) << "'" << eom;
722 throw 0;
723 }
724
725 if(*sub_size == 0)
726 {
727 error().source_location=source_location;
728 error() << "type had size 0: '" << to_string(subtype) << "'" << eom;
729 throw 0;
730 }
731
732 // adjust by width of base type
733 if(s % *sub_size != 0)
734 {
735 error().source_location=source_location;
736 error() << "vector size (" << s
737 << ") expected to be multiple of base type size (" << *sub_size
738 << ")" << eom;
739 throw 0;
740 }
741
742 s /= *sub_size;
743
744 // produce the type with ID_vector
745 vector_typet new_type(subtype, from_integer(s, signed_size_type()));
746 new_type.add_source_location() = source_location;
747 new_type.size().add_source_location() = source_location;
748 type = new_type;
749}
750
752{
753 // These get replaced by symbol types later.
754 irep_idt identifier;
755
756 bool have_body=type.find(ID_components).is_not_nil();
757
758 c_qualifierst original_qualifiers(type);
759
760 // the type symbol, which may get re-used in other declarations, must not
761 // carry any qualifiers (other than transparent_union, which isn't really a
762 // qualifier)
763 c_qualifierst remove_qualifiers;
764 remove_qualifiers.is_transparent_union =
765 original_qualifiers.is_transparent_union;
766 remove_qualifiers.write(type);
767
768 bool is_packed = type.get_bool(ID_C_packed);
769 irept alignment = type.find(ID_C_alignment);
770
771 if(type.find(ID_tag).is_nil())
772 {
773 // Anonymous? Must come with body.
774 assert(have_body);
775
776 // produce symbol
777 symbolt compound_symbol;
778 compound_symbol.is_type=true;
779 compound_symbol.type=type;
780 compound_symbol.location=type.source_location();
781
783
784 std::string typestr = type2name(compound_symbol.type, *this);
785 compound_symbol.base_name = "#anon#" + typestr;
786 compound_symbol.name="tag-#anon#"+typestr;
787 identifier=compound_symbol.name;
788
789 // We might already have the same anonymous union/struct,
790 // and this is simply ok. Note that the C standard treats
791 // these as different types.
792 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
793 {
794 symbolt *new_symbol;
795 move_symbol(compound_symbol, new_symbol);
796 }
797 }
798 else
799 {
800 identifier=type.find(ID_tag).get(ID_identifier);
801
802 // does it exist already?
803 symbol_tablet::symbolst::const_iterator s_it=
804 symbol_table.symbols.find(identifier);
805
806 if(s_it==symbol_table.symbols.end())
807 {
808 // no, add new symbol
809 irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
810 type.remove(ID_tag);
811 type.set(ID_tag, base_name);
812
813 symbolt compound_symbol;
814 compound_symbol.is_type=true;
815 compound_symbol.name=identifier;
816 compound_symbol.base_name=base_name;
817 compound_symbol.type=type;
818 compound_symbol.location=type.source_location();
819 compound_symbol.pretty_name=id2string(type.id())+" "+id2string(base_name);
820
821 typet new_type=compound_symbol.type;
822
823 // mark as incomplete
824 to_struct_union_type(compound_symbol.type).make_incomplete();
825
826 symbolt *new_symbol;
827 move_symbol(compound_symbol, new_symbol);
828
829 if(have_body)
830 {
832
833 new_symbol->type.swap(new_type);
834 }
835 }
836 else
837 {
838 // yes, it exists already
839 if(
840 s_it->second.type.id() == type.id() &&
841 to_struct_union_type(s_it->second.type).is_incomplete())
842 {
843 // Maybe we got a body now.
844 if(have_body)
845 {
846 irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
847 type.remove(ID_tag);
848 type.set(ID_tag, base_name);
849
851 symbol_table.get_writeable_ref(s_it->first).type.swap(type);
852 }
853 }
854 else if(s_it->second.type.id() != type.id())
855 {
857 error() << "redefinition of '" << s_it->second.pretty_name << "'"
858 << " as different kind of tag" << eom;
859 throw 0;
860 }
861 else if(have_body)
862 {
864 error() << "redefinition of body of '" << s_it->second.pretty_name
865 << "'" << eom;
866 throw 0;
867 }
868 }
869 }
870
871 typet tag_type;
872
873 if(type.id() == ID_union)
874 tag_type = union_tag_typet(identifier);
875 else if(type.id() == ID_struct)
876 tag_type = struct_tag_typet(identifier);
877 else
879
880 tag_type.add_source_location() = type.source_location();
881 type.swap(tag_type);
882
883 original_qualifiers.write(type);
884
885 if(is_packed)
886 type.set(ID_C_packed, true);
887 if(alignment.is_not_nil())
888 type.set(ID_C_alignment, alignment);
889}
890
892 struct_union_typet &type)
893{
895
896 struct_union_typet::componentst old_components;
897 old_components.swap(components);
898
899 // We get these as declarations!
900 for(auto &decl : old_components)
901 {
902 // the arguments are member declarations or static assertions
903 assert(decl.id()==ID_declaration);
904
905 ansi_c_declarationt &declaration=
906 to_ansi_c_declaration(static_cast<exprt &>(decl));
907
908 if(declaration.get_is_static_assert())
909 {
910 struct_union_typet::componentt new_component;
911 new_component.id(ID_static_assert);
912 new_component.add_source_location()=declaration.source_location();
913 new_component.operands().swap(declaration.operands());
914 assert(new_component.operands().size()==2);
915 components.push_back(new_component);
916 }
917 else
918 {
919 // do first half of type
920 typecheck_type(declaration.type());
922
923 for(const auto &declarator : declaration.declarators())
924 {
925 struct_union_typet::componentt new_component(
926 declarator.get_base_name(), declaration.full_type(declarator));
927
928 // There may be a declarator, which we use as location for
929 // the component. Otherwise, use location of the declaration.
930 const source_locationt source_location =
931 declarator.get_name().empty() ? declaration.source_location()
932 : declarator.source_location();
933
934 new_component.add_source_location() = source_location;
935 new_component.set_pretty_name(declarator.get_base_name());
936
937 typecheck_type(new_component.type());
938
939 if(!is_complete_type(new_component.type()) &&
940 (new_component.type().id()!=ID_array ||
941 !to_array_type(new_component.type()).is_incomplete()))
942 {
943 error().source_location = source_location;
944 error() << "incomplete type not permitted here" << eom;
945 throw 0;
946 }
947
948 if(new_component.type().id() == ID_empty)
949 {
950 error().source_location = source_location;
951 error() << "void-typed member not permitted" << eom;
952 throw 0;
953 }
954
955 components.push_back(new_component);
956 }
957 }
958 }
959
960 unsigned anon_member_counter=0;
961
962 // scan for anonymous members, and name them
963 for(auto &member : components)
964 {
965 if(!member.get_name().empty())
966 continue;
967
968 member.set_name("$anon"+std::to_string(anon_member_counter++));
969 member.set_anonymous(true);
970 }
971
972 // scan for duplicate members
973
974 {
975 std::unordered_set<irep_idt> members;
976
977 for(const auto &c : components)
978 {
979 if(!members.insert(c.get_name()).second)
980 {
981 error().source_location = c.source_location();
982 error() << "duplicate member '" << c.get_name() << '\'' << eom;
983 throw 0;
984 }
985 }
986 }
987
988 // We allow an incomplete (C99) array as _last_ member!
989 // Zero-length is allowed everywhere.
990
991 if(type.id()==ID_struct ||
992 type.id()==ID_union)
993 {
994 for(struct_union_typet::componentst::iterator
995 it=components.begin();
996 it!=components.end();
997 it++)
998 {
999 typet &c_type=it->type();
1000
1001 if(c_type.id()==ID_array &&
1002 to_array_type(c_type).is_incomplete())
1003 {
1004 // needs to be last member
1005 if(type.id()==ID_struct && it!=--components.end())
1006 {
1007 error().source_location=it->source_location();
1008 error() << "flexible struct member must be last member" << eom;
1009 throw 0;
1010 }
1011
1012 // make it zero-length
1013 c_type.id(ID_array);
1014 c_type.set(ID_size, from_integer(0, c_index_type()));
1015 }
1016 }
1017 }
1018
1019 // We may add some minimal padding inside and at
1020 // the end of structs and
1021 // as additional member for unions.
1022
1023 if(type.id()==ID_struct)
1024 add_padding(to_struct_type(type), *this);
1025 else if(type.id()==ID_union)
1026 add_padding(to_union_type(type), *this);
1027
1028 // Now remove zero-width bit-fields, these are just
1029 // for adjusting alignment.
1030 for(struct_typet::componentst::iterator
1031 it=components.begin();
1032 it!=components.end();
1033 ) // blank
1034 {
1035 if(it->type().id()==ID_c_bit_field &&
1036 to_c_bit_field_type(it->type()).get_width()==0)
1037 it=components.erase(it);
1038 else
1039 it++;
1040 }
1041
1042 // finally, check _Static_assert inside the compound
1043 for(struct_union_typet::componentst::iterator
1044 it=components.begin();
1045 it!=components.end();
1046 ) // no it++
1047 {
1048 if(it->id()==ID_static_assert)
1049 {
1051 {
1052 error().source_location = it->source_location();
1053 error() << "static_assert not supported in compound body" << eom;
1054 throw 0;
1055 }
1056
1057 exprt &assertion = to_binary_expr(*it).op0();
1058 typecheck_expr(assertion);
1060 assertion = typecast_exprt(assertion, bool_typet());
1061 make_constant(assertion);
1062
1063 if(assertion.is_false())
1064 {
1065 error().source_location=it->source_location();
1066 error() << "failed _Static_assert" << eom;
1067 throw 0;
1068 }
1069 else if(!assertion.is_true())
1070 {
1071 // should warn/complain
1072 }
1073
1074 it=components.erase(it);
1075 }
1076 else
1077 it++;
1078 }
1079}
1080
1082 const mp_integer &min_value,
1083 const mp_integer &max_value) const
1084{
1086 {
1087 return signed_int_type();
1088 }
1089 else
1090 {
1091 // enum constants are at least 'int', but may be made larger.
1092 // 'Packing' has no influence.
1093 if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1094 min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1095 return signed_int_type();
1096 else if(max_value<(mp_integer(1)<<config.ansi_c.int_width) &&
1097 min_value>=0)
1098 return unsigned_int_type();
1099 else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width) &&
1100 min_value>=0)
1101 return unsigned_long_int_type();
1102 else if(max_value<(mp_integer(1)<<config.ansi_c.long_long_int_width) &&
1103 min_value>=0)
1105 else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1106 min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1107 return signed_long_int_type();
1108 else
1110 }
1111}
1112
1114 const mp_integer &min_value,
1115 const mp_integer &max_value,
1116 bool is_packed) const
1117{
1119 {
1120 return signed_int_type();
1121 }
1122 else
1123 {
1124 if(min_value<0)
1125 {
1126 // We'll want a signed type.
1127
1128 if(is_packed)
1129 {
1130 // If packed, there are smaller options.
1131 if(max_value<(mp_integer(1)<<(config.ansi_c.char_width-1)) &&
1132 min_value>=-(mp_integer(1)<<(config.ansi_c.char_width-1)))
1133 return signed_char_type();
1134 else if(max_value<(mp_integer(1)<<(config.ansi_c.short_int_width-1)) &&
1135 min_value>=-(mp_integer(1)<<(config.ansi_c.short_int_width-1)))
1136 return signed_short_int_type();
1137 }
1138
1139 if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1140 min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1141 return signed_int_type();
1142 else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1143 min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1144 return signed_long_int_type();
1145 else
1147 }
1148 else
1149 {
1150 // We'll want an unsigned type.
1151
1152 if(is_packed)
1153 {
1154 // If packed, there are smaller options.
1155 if(max_value<(mp_integer(1)<<config.ansi_c.char_width))
1156 return unsigned_char_type();
1157 else if(max_value<(mp_integer(1)<<config.ansi_c.short_int_width))
1158 return unsigned_short_int_type();
1159 }
1160
1161 if(max_value<(mp_integer(1)<<config.ansi_c.int_width))
1162 return unsigned_int_type();
1163 else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width))
1164 return unsigned_long_int_type();
1165 else
1167 }
1168 }
1169}
1170
1172{
1173 // These come with the declarations
1174 // of the enum constants as operands.
1175
1176 exprt &as_expr=static_cast<exprt &>(static_cast<irept &>(type));
1177 source_locationt source_location=type.source_location();
1178
1179 // We allow empty enums in the grammar to get better
1180 // error messages.
1181 if(as_expr.operands().empty())
1182 {
1183 error().source_location=source_location;
1184 error() << "empty enum" << eom;
1185 throw 0;
1186 }
1187
1188 const bool have_underlying_type =
1189 type.find_type(ID_enum_underlying_type).is_not_nil();
1190
1191 if(have_underlying_type)
1192 {
1193 typecheck_type(type.add_type(ID_enum_underlying_type));
1194
1195 const typet &underlying_type =
1196 static_cast<const typet &>(type.find(ID_enum_underlying_type));
1197
1198 if(!is_signed_or_unsigned_bitvector(underlying_type))
1199 {
1200 std::ostringstream msg;
1201 msg << source_location << ": non-integral type '"
1202 << underlying_type.get(ID_C_c_type)
1203 << "' is an invalid underlying type";
1204 throw invalid_source_file_exceptiont{msg.str()};
1205 }
1206 }
1207
1208 // enums start at zero;
1209 // we also track min and max to find a nice base type
1210 mp_integer value=0, min_value=0, max_value=0;
1211
1212 std::list<c_enum_typet::c_enum_membert> enum_members;
1213
1214 // We need to determine a width, and a signedness
1215 // to obtain an 'underlying type'.
1216 // We just do int, but gcc might pick smaller widths
1217 // if the type is marked as 'packed'.
1218 // gcc/clang may also pick a larger width. Visual Studio doesn't.
1219
1220 for(auto &op : as_expr.operands())
1221 {
1223 exprt &v=declaration.declarator().value();
1224
1225 if(v.is_not_nil()) // value given?
1226 {
1227 exprt tmp_v=v;
1228 typecheck_expr(tmp_v);
1229 add_rounding_mode(tmp_v);
1230 simplify(tmp_v, *this);
1231 if(tmp_v.is_true())
1232 value=1;
1233 else if(tmp_v.is_false())
1234 value=0;
1235 else if(
1236 tmp_v.id() == ID_constant &&
1237 !to_integer(to_constant_expr(tmp_v), value))
1238 {
1239 }
1240 else
1241 {
1243 error() << "enum is not a constant" << eom;
1244 throw 0;
1245 }
1246 }
1247
1248 if(value<min_value)
1249 min_value=value;
1250 if(value>max_value)
1251 max_value=value;
1252
1253 typet constant_type;
1254
1255 if(have_underlying_type)
1256 {
1257 constant_type = type.find_type(ID_enum_underlying_type);
1258 const auto &tmp = to_integer_bitvector_type(constant_type);
1259
1260 if(value < tmp.smallest() || value > tmp.largest())
1261 {
1262 std::ostringstream msg;
1263 msg
1264 << v.source_location()
1265 << ": enumerator value is not representable in the underlying type '"
1266 << constant_type.get(ID_C_c_type) << "'";
1267 throw invalid_source_file_exceptiont{msg.str()};
1268 }
1269 }
1270 else
1271 {
1272 constant_type = enum_constant_type(min_value, max_value);
1273 }
1274
1275 v=from_integer(value, constant_type);
1276
1277 declaration.type()=constant_type;
1278 typecheck_declaration(declaration);
1279
1280 irep_idt base_name=
1281 declaration.declarator().get_base_name();
1282
1283 irep_idt identifier=
1284 declaration.declarator().get_name();
1285
1286 // store
1288 member.set_identifier(identifier);
1289 member.set_base_name(base_name);
1290 // Note: The value will be correctly set to a bv type when we know
1291 // the width of the bitvector
1292 member.set_value(integer2string(value));
1293 enum_members.push_back(member);
1294
1295 // produce value for next constant
1296 ++value;
1297 }
1298
1299 // Remove these now; we add them to the
1300 // c_enum symbol later.
1301 as_expr.operands().clear();
1302
1303 bool is_packed=type.get_bool(ID_C_packed);
1304
1305 // We use a subtype to store the underlying type.
1306 bitvector_typet underlying_type(ID_nil);
1307
1308 if(have_underlying_type)
1309 {
1310 underlying_type =
1311 to_bitvector_type(type.find_type(ID_enum_underlying_type));
1312 }
1313 else
1314 {
1315 underlying_type = enum_underlying_type(min_value, max_value, is_packed);
1316 }
1317
1318 // Get the width to make the values have a bitvector type
1319 std::size_t width = underlying_type.get_width();
1320 for(auto &member : enum_members)
1321 {
1322 // Note: This is inefficient as it first turns integers to strings
1323 // and then turns them back to bvrep
1324 auto value = string2integer(id2string(member.get_value()));
1325 member.set_value(integer2bvrep(value, width));
1326 }
1327
1328 // tag?
1329 if(type.find(ID_tag).is_nil())
1330 {
1331 // None, it's anonymous. We generate a tag.
1332 std::string anon_identifier="#anon_enum";
1333
1334 for(const auto &member : enum_members)
1335 {
1336 anon_identifier+='$';
1337 anon_identifier+=id2string(member.get_base_name());
1338 anon_identifier+='=';
1339 anon_identifier+=id2string(member.get_value());
1340 }
1341
1342 if(is_packed)
1343 anon_identifier+="#packed";
1344
1345 type.add(ID_tag).set(ID_identifier, anon_identifier);
1346 }
1347
1348 irept &tag=type.add(ID_tag);
1349 irep_idt base_name=tag.get(ID_C_base_name);
1350 irep_idt identifier=tag.get(ID_identifier);
1351
1352 // Put into symbol table
1353 symbolt enum_tag_symbol;
1354
1355 enum_tag_symbol.is_type=true;
1356 enum_tag_symbol.type=type;
1357 enum_tag_symbol.location=source_location;
1358 enum_tag_symbol.is_file_local=true;
1359 enum_tag_symbol.base_name=base_name;
1360 enum_tag_symbol.name=identifier;
1361
1362 // throw in the enum members as 'body'
1363 irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub();
1364
1365 for(const auto &member : enum_members)
1366 body.push_back(member);
1367
1368 enum_tag_symbol.type.subtype()=underlying_type;
1369
1370 // is it in the symbol table already?
1371 symbol_tablet::symbolst::const_iterator s_it=
1372 symbol_table.symbols.find(identifier);
1373
1374 if(s_it!=symbol_table.symbols.end())
1375 {
1376 // Yes.
1377 const symbolt &symbol=s_it->second;
1378
1379 if(symbol.type.id() != ID_c_enum)
1380 {
1381 error().source_location = source_location;
1382 error() << "use of tag that does not match previous declaration" << eom;
1383 throw 0;
1384 }
1385
1386 if(to_c_enum_type(symbol.type).is_incomplete())
1387 {
1388 // Ok, overwrite the type in the symbol table.
1389 // This gives us the members and the subtype.
1390 symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
1391 }
1392 else
1393 {
1394 // We might already have the same anonymous enum, and this is
1395 // simply ok. Note that the C standard treats these as
1396 // different types.
1397 if(!base_name.empty())
1398 {
1400 error() << "redeclaration of enum tag" << eom;
1401 throw 0;
1402 }
1403 }
1404 }
1405 else
1406 {
1407 symbolt *new_symbol;
1408 move_symbol(enum_tag_symbol, new_symbol);
1409 }
1410
1411 // We produce a c_enum_tag as the resulting type.
1412 type.id(ID_c_enum_tag);
1413 type.remove(ID_tag);
1414 type.set(ID_identifier, identifier);
1415}
1416
1418{
1419 // It's just a tag.
1420
1421 if(type.find(ID_tag).is_nil())
1422 {
1424 error() << "anonymous enum tag without members" << eom;
1425 throw 0;
1426 }
1427
1428 if(type.find(ID_enum_underlying_type).is_not_nil())
1429 {
1431 warning() << "ignoring specification of underlying type for enum" << eom;
1432 }
1433
1434 source_locationt source_location=type.source_location();
1435
1436 irept &tag=type.add(ID_tag);
1437 irep_idt base_name=tag.get(ID_C_base_name);
1438 irep_idt identifier=tag.get(ID_identifier);
1439
1440 // is it in the symbol table?
1441 symbol_tablet::symbolst::const_iterator s_it=
1442 symbol_table.symbols.find(identifier);
1443
1444 if(s_it!=symbol_table.symbols.end())
1445 {
1446 // Yes.
1447 const symbolt &symbol=s_it->second;
1448
1449 if(symbol.type.id() != ID_c_enum)
1450 {
1451 error().source_location=source_location;
1452 error() << "use of tag that does not match previous declaration" << eom;
1453 throw 0;
1454 }
1455 }
1456 else
1457 {
1458 // no, add it as an incomplete c_enum
1459 c_enum_typet new_type(signed_int_type()); // default subtype
1460 new_type.add(ID_tag)=tag;
1461 new_type.make_incomplete();
1462
1463 symbolt enum_tag_symbol;
1464
1465 enum_tag_symbol.is_type=true;
1466 enum_tag_symbol.type=new_type;
1467 enum_tag_symbol.location=source_location;
1468 enum_tag_symbol.is_file_local=true;
1469 enum_tag_symbol.base_name=base_name;
1470 enum_tag_symbol.name=identifier;
1471
1472 symbolt *new_symbol;
1473 move_symbol(enum_tag_symbol, new_symbol);
1474 }
1475
1476 // Clean up resulting type
1477 type.remove(ID_tag);
1478 type.set_identifier(identifier);
1479}
1480
1482{
1484
1485 mp_integer i;
1486
1487 {
1488 exprt &width_expr=static_cast<exprt &>(type.add(ID_size));
1489
1490 typecheck_expr(width_expr);
1491 make_constant_index(width_expr);
1492
1493 if(to_integer(to_constant_expr(width_expr), i))
1494 {
1496 error() << "failed to convert bit field width" << eom;
1497 throw 0;
1498 }
1499
1500 if(i<0)
1501 {
1503 error() << "bit field width is negative" << eom;
1504 throw 0;
1505 }
1506
1507 type.set_width(numeric_cast_v<std::size_t>(i));
1508 type.remove(ID_size);
1509 }
1510
1511 const typet &underlying_type = type.underlying_type();
1512
1513 std::size_t sub_width=0;
1514
1515 if(underlying_type.id() == ID_bool)
1516 {
1517 // This is the 'proper' bool.
1518 sub_width=1;
1519 }
1520 else if(
1521 underlying_type.id() == ID_signedbv ||
1522 underlying_type.id() == ID_unsignedbv || underlying_type.id() == ID_c_bool)
1523 {
1524 sub_width = to_bitvector_type(underlying_type).get_width();
1525 }
1526 else if(underlying_type.id() == ID_c_enum_tag)
1527 {
1528 // These point to an enum, which has a sub-subtype,
1529 // which may be smaller or larger than int, and we thus have
1530 // to check.
1531 const auto &c_enum_type =
1532 to_c_enum_type(follow_tag(to_c_enum_tag_type(underlying_type)));
1533
1534 if(c_enum_type.is_incomplete())
1535 {
1537 error() << "bit field has incomplete enum type" << eom;
1538 throw 0;
1539 }
1540
1541 sub_width = to_bitvector_type(c_enum_type.underlying_type()).get_width();
1542 }
1543 else
1544 {
1546 error() << "bit field with non-integer type: " << to_string(underlying_type)
1547 << eom;
1548 throw 0;
1549 }
1550
1551 if(i>sub_width)
1552 {
1554 error() << "bit field (" << i
1555 << " bits) larger than type (" << sub_width << " bits)"
1556 << eom;
1557 throw 0;
1558 }
1559}
1560
1562{
1563 // save location
1564 source_locationt source_location=type.source_location();
1565
1566 // retain the qualifiers as is
1567 c_qualifierst c_qualifiers;
1568 c_qualifiers.read(type);
1569
1570 const auto &as_expr = (const exprt &)type;
1571
1572 if(!as_expr.has_operands())
1573 {
1574 typet t=static_cast<const typet &>(type.find(ID_type_arg));
1575 typecheck_type(t);
1576 type.swap(t);
1577 }
1578 else
1579 {
1580 exprt expr = to_unary_expr(as_expr).op();
1581 typecheck_expr(expr);
1582
1583 // undo an implicit address-of
1584 if(expr.id()==ID_address_of &&
1585 expr.get_bool(ID_C_implicit))
1586 {
1587 expr = to_address_of_expr(expr).object();
1588 }
1589
1590 type.swap(expr.type());
1591 }
1592
1593 type.add_source_location()=source_location;
1594 c_qualifiers.write(type);
1595}
1596
1598{
1599 const irep_idt &identifier = to_typedef_type(type).get_identifier();
1600
1601 symbol_tablet::symbolst::const_iterator s_it =
1602 symbol_table.symbols.find(identifier);
1603
1604 if(s_it == symbol_table.symbols.end())
1605 {
1607 error() << "typedef symbol '" << identifier << "' not found" << eom;
1608 throw 0;
1609 }
1610
1611 const symbolt &symbol = s_it->second;
1612
1613 if(!symbol.is_type)
1614 {
1616 error() << "expected type symbol for typedef" << eom;
1617 throw 0;
1618 }
1619
1620 // overwrite, but preserve (add) any qualifiers and other flags
1621
1622 c_qualifierst c_qualifiers(type);
1623 bool is_packed = type.get_bool(ID_C_packed);
1624 irept alignment = type.find(ID_C_alignment);
1625
1626 c_qualifiers += c_qualifierst(symbol.type);
1627 type = symbol.type;
1628 c_qualifiers.write(type);
1629
1630 if(is_packed)
1631 type.set(ID_C_packed, true);
1632 if(alignment.is_not_nil())
1633 type.set(ID_C_alignment, alignment);
1634
1635 // CPROVER extensions
1636 if(symbol.base_name == CPROVER_PREFIX "rational")
1637 {
1638 type=rational_typet();
1639 }
1640 else if(symbol.base_name == CPROVER_PREFIX "integer")
1641 {
1642 type=integer_typet();
1643 }
1644}
1645
1647{
1648 if(type.id()==ID_array)
1649 {
1650 source_locationt source_location=type.source_location();
1651 type=pointer_type(type.subtype());
1652 type.add_source_location()=source_location;
1653 }
1654 else if(type.id()==ID_code)
1655 {
1656 // see ISO/IEC 9899:1999 page 199 clause 8,
1657 // may be hidden in typedef
1658 source_locationt source_location=type.source_location();
1659 type=pointer_type(type);
1660 type.add_source_location()=source_location;
1661 }
1662 else if(type.id()==ID_KnR)
1663 {
1664 // any KnR args without type yet?
1665 type=signed_int_type(); // the default is integer!
1666 // no source location
1667 }
1668}
ANSI-C Language Conversion.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
ANSI-C Language Type Checking.
already_typechecked_typet & to_already_typechecked_type(typet &type)
floatbv_typet float_type()
Definition: c_types.cpp:195
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:90
signedbv_typet signed_char_type()
Definition: c_types.cpp:152
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:111
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:104
unsignedbv_typet size_type()
Definition: c_types.cpp:68
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:145
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:97
bitvector_typet c_index_type()
Definition: c_types.cpp:16
floatbv_typet double_type()
Definition: c_types.cpp:203
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:47
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:61
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
exprt & object()
Definition: pointer_expr.h:370
static void make_already_typechecked(typet &type)
virtual void read(const typet &type)
virtual void write(typet &type)
const ansi_c_declaratort & declarator() const
const declaratorst & declarators() const
typet full_type(const ansi_c_declaratort &) const
bool get_is_static_assert() const
irep_idt get_base_name() const
irep_idt get_name() const
Arrays with given size.
Definition: std_types.h:763
bool is_incomplete() const
Definition: std_types.h:805
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
void set_width(std::size_t width)
Definition: std_types.h:869
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:20
const typet & underlying_type() const
Definition: c_types.h:30
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
void set_identifier(const irep_idt &identifier)
Definition: c_types.h:239
void set_value(const irep_idt &value)
Definition: c_types.h:231
void set_base_name(const irep_idt &base_name)
Definition: c_types.h:247
The type of C enums.
Definition: c_types.h:217
void make_incomplete()
enum types may be incomplete
Definition: c_types.h:267
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:261
virtual void write(typet &src) const override
bool is_transparent_union
Definition: c_qualifiers.h:98
virtual void read(const typet &src) override
virtual void typecheck_compound_body(struct_union_typet &type)
virtual void make_index_type(exprt &expr)
virtual void typecheck_code_type(code_typet &type)
virtual void typecheck_expr(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_vector_type(typet &type)
const irep_idt mode
virtual void typecheck_c_enum_type(typet &type)
virtual void make_constant(exprt &expr)
symbol_tablet & symbol_table
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
virtual void adjust_function_parameter(typet &type) const
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
virtual void typecheck_custom_type(typet &type)
virtual void make_constant_index(exprt &expr)
bitvector_typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual void typecheck_compound_type(struct_union_typet &type)
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_typedef_type(typet &type)
virtual void typecheck_array_type(array_typet &type)
virtual void typecheck_typeof_type(typet &type)
virtual void typecheck_type(typet &type)
A codet representing an assignment in the program.
Definition: std_code.h:24
A codet representing the declaration of a local variable.
Definition: std_code.h:347
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
void make_ellipsis()
Definition: std_types.h:635
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
std::string::const_iterator end() const
Definition: dstring.h:181
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
Unbounded, signed integers (mathematical integers, not bitvectors)
Thrown when we can't handle something in an input source file.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
Unbounded, signed rational numbers.
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:114
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:191
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
const irep_idt & get_identifier() const
Definition: std_types.h:410
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:405
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
const irep_idt & get_identifier() const
Definition: typedef_type.h:28
The type of an expression, extends irept.
Definition: type.h:29
typet & add_type(const irep_idt &name)
Definition: type.h:84
const typet & find_type(const irep_idt &name) const
Definition: type.h:89
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
void remove_subtype()
Definition: type.h:71
const exprt & op() const
Definition: std_expr.h:293
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:82
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:75
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:57
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Mathematical types.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:458
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t long_long_int_width
Definition: config.h:114
std::size_t long_int_width
Definition: config.h:110
std::size_t short_int_width
Definition: config.h:113
std::size_t char_width
Definition: config.h:112
flavourt mode
Definition: config.h:222
std::size_t int_width
Definition: config.h:109
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:81
Type Naming for C.
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
Definition: typedef_type.h:39
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45