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