cprover
Loading...
Searching...
No Matches
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 // save the location
287 result.add_source_location()=type.source_location();
288
289 type=result;
290 }
291 else if(underlying_type.id()==ID_complex)
292 {
293 // gcc allows this, but clang doesn't -- see enums above
295
296 if(gcc_attr_mode == "__SC__") // 32 bits
298 else if(gcc_attr_mode == "__DC__") // 64 bits
300 else if(gcc_attr_mode == "__TC__") // 128 bits
302 else // give up, just use subtype
303 result = to_type_with_subtype(type).subtype();
304
305 // save the location
306 result.add_source_location()=type.source_location();
307
308 type=complex_typet(result);
309 }
310 else
311 {
313 error() << "attribute mode '" << gcc_attr_mode
314 << "' applied to inappropriate type '" << to_string(type) << "'"
315 << eom;
316 throw 0;
317 }
318 }
319
320 // do a mild bit of rule checking
321
322 if(type.get_bool(ID_C_restricted) &&
323 type.id()!=ID_pointer &&
324 type.id()!=ID_array)
325 {
327 error() << "only a pointer can be 'restrict'" << eom;
328 throw 0;
329 }
330}
331
333{
334 // they all have a width
336 static_cast<const exprt &>(type.find(ID_size));
337
339 source_locationt source_location=size_expr.source_location();
341
344 {
345 error().source_location=source_location;
346 error() << "failed to convert bit vector width to constant" << eom;
347 throw 0;
348 }
349
350 if(size_int<1)
351 {
352 error().source_location=source_location;
353 error() << "bit vector width invalid" << eom;
354 throw 0;
355 }
356
357 type.remove(ID_size);
359
360 // depending on type, there may be a number of fractional bits
361
362 if(type.id()==ID_custom_unsignedbv)
363 type.id(ID_unsignedbv);
364 else if(type.id()==ID_custom_signedbv)
365 type.id(ID_signedbv);
366 else if(type.id()==ID_custom_fixedbv)
367 {
368 type.id(ID_fixedbv);
369
371 static_cast<const exprt &>(type.find(ID_f));
372
374 f_expr.find_source_location();
375
377
379
382 {
384 error() << "failed to convert number of fraction bits to constant" << eom;
385 throw 0;
386 }
387
389 {
391 error() << "fixedbv fraction width invalid" << eom;
392 throw 0;
393 }
394
395 type.remove(ID_f);
397 }
398 else if(type.id()==ID_custom_floatbv)
399 {
400 type.id(ID_floatbv);
401
403 static_cast<const exprt &>(type.find(ID_f));
404
406 f_expr.find_source_location();
407
409
411
414 {
416 error() << "failed to convert number of fraction bits to constant" << eom;
417 throw 0;
418 }
419
421 {
423 error() << "floatbv fraction width invalid" << eom;
424 throw 0;
425 }
426
427 type.remove(ID_f);
429 }
430 else
432}
433
435{
436 // the return type is still 'subtype()'
437 type.return_type() = to_type_with_subtype(type).subtype();
438 type.remove_subtype();
439
440 code_typet::parameterst &parameters=type.parameters();
441
442 // if we don't have any parameters, we assume it's (...)
443 if(parameters.empty())
444 {
445 type.make_ellipsis();
446 }
447 else // we do have parameters
448 {
449 // is the last one ellipsis?
450 if(type.parameters().back().id()==ID_ellipsis)
451 {
452 type.make_ellipsis();
453 type.parameters().pop_back();
454 }
455
457
458 for(auto &param : type.parameters())
459 {
460 // turn the declarations into parameters
461 if(param.id()==ID_declaration)
462 {
463 ansi_c_declarationt &declaration=
465
466
467 // first fix type
469 declaration.full_type(declaration.declarator()));
470 typet &param_type = parameter.type();
471 std::list<codet> tmp_clean_code;
472 tmp_clean_code.swap(clean_code); // ignore side-effects
476
477 // adjust the identifier
478 irep_idt identifier=declaration.declarator().get_name();
479
480 // abstract or not?
481 if(identifier.empty())
482 {
483 // abstract
484 parameter.add_source_location()=declaration.type().source_location();
485 }
486 else
487 {
488 // make visible now, later parameters might use it
489 parameter_map[identifier] = param_type;
490 parameter.set_base_name(declaration.declarator().get_base_name());
491 parameter.add_source_location()=
492 declaration.declarator().source_location();
493 }
494
495 // put the parameter in place of the declaration
496 param.swap(parameter);
497 }
498 }
499
501
502 if(parameters.size() == 1 && parameters[0].type().id() == ID_empty)
503 {
504 // if we just have one parameter of type void, remove it
505 parameters.clear();
506 }
507 }
508
510
511 // 6.7.6.3:
512 // "A function declarator shall not specify a return type that
513 // is a function type or an array type."
514
515 const typet &decl_return_type = type.return_type();
516
517 if(decl_return_type.id() == ID_array)
518 {
520 error() << "function must not return array" << eom;
521 throw 0;
522 }
523
524 if(decl_return_type.id() == ID_code)
525 {
527 error() << "function must not return function type" << eom;
528 throw 0;
529 }
530}
531
533{
534 // Typecheck the element type.
536
537 // We don't allow void as the element type.
538 if(type.element_type().id() == ID_empty)
539 {
541 error() << "array of voids" << eom;
542 throw 0;
543 }
544
545 // We don't allow incomplete structs or unions as element type.
546 const typet &followed_subtype = follow(type.element_type());
547
548 if(
550 to_struct_union_type(followed_subtype).is_incomplete())
551 {
552 // ISO/IEC 9899 6.7.5.2
554 error() << "array has incomplete element type" << eom;
555 throw 0;
556 }
557
558 // We don't allow functions as element type.
559 if(type.element_type().id() == ID_code)
560 {
561 // ISO/IEC 9899 6.7.5.2
563 error() << "array of function element type" << eom;
564 throw 0;
565 }
566
567 // We add the index type.
569
570 // Check the array size, if given.
571 if(type.is_complete())
572 {
573 exprt &size = type.size();
575 typecheck_expr(size);
576 make_index_type(size);
577
578 // The size need not be a constant!
579 // We simplify it, for the benefit of array initialisation.
580
581 exprt tmp_size=size;
583 simplify(tmp_size, *this);
584
585 if(tmp_size.is_constant())
586 {
587 mp_integer s;
589 {
591 error() << "failed to convert constant: "
592 << tmp_size.pretty() << eom;
593 throw 0;
594 }
595
596 if(s<0)
597 {
599 error() << "array size must not be negative, "
600 "but got " << s << eom;
601 throw 0;
602 }
603
604 size=tmp_size;
605 }
606 else if(tmp_size.id()==ID_infinity)
607 {
608 size=tmp_size;
609 }
610 else if(tmp_size.id()==ID_symbol &&
611 tmp_size.type().get_bool(ID_C_constant))
612 {
613 // We allow a constant variable as array size, assuming
614 // it won't change.
615 // This criterion can be tricked:
616 // Of course we can modify a 'const' symbol, e.g.,
617 // using a pointer type cast. Interestingly,
618 // at least gcc 4.2.1 makes the very same mistake!
619 size=tmp_size;
620 }
621 else
622 {
623 // not a constant and not infinity
624
626
628 {
630 error() << "array size of static symbol '" << current_symbol.base_name
631 << "' is not constant" << eom;
632 throw 0;
633 }
634
635 symbolt &new_symbol = get_fresh_aux_symbol(
636 size_type(),
637 id2string(current_symbol.name) + "$array_size",
638 id2string(current_symbol.base_name) + "$array_size",
640 mode,
642 new_symbol.type.set(ID_C_constant, true);
644
645 // produce the code that declares and initializes the symbol
646 symbol_exprt symbol_expr = new_symbol.symbol_expr();
647
648 code_frontend_declt declaration(symbol_expr);
650
651 code_frontend_assignt assignment;
652 assignment.lhs()=symbol_expr;
653 assignment.rhs() = new_symbol.value;
655
656 // store the code
657 clean_code.push_back(declaration);
658 clean_code.push_back(assignment);
659
660 // fix type
661 size=symbol_expr;
662 }
663 }
664}
665
667{
668 // This turns the type with ID_frontend_vector into the type
669 // with ID_vector; the difference is that the latter has
670 // a constant as size, which we establish now.
671 exprt size = static_cast<const exprt &>(type.find(ID_size));
672 const source_locationt source_location = size.find_source_location();
673
674 typecheck_expr(size);
675
676 typet subtype = to_type_with_subtype(type).subtype();
677 typecheck_type(subtype);
678
679 // we are willing to combine 'vector' with various
680 // other types, but not everything!
681
682 if(subtype.id()!=ID_signedbv &&
683 subtype.id()!=ID_unsignedbv &&
684 subtype.id()!=ID_floatbv &&
685 subtype.id()!=ID_fixedbv)
686 {
687 error().source_location=source_location;
688 error() << "cannot make a vector of subtype "
689 << to_string(subtype) << eom;
690 throw 0;
691 }
692
694
695 mp_integer s;
696 if(to_integer(to_constant_expr(size), s))
697 {
698 error().source_location=source_location;
699 error() << "failed to convert constant: "
700 << size.pretty() << eom;
701 throw 0;
702 }
703
704 if(s<=0)
705 {
706 error().source_location=source_location;
707 error() << "vector size must be positive, "
708 "but got " << s << eom;
709 throw 0;
710 }
711
712 // the subtype must have constant size
713 auto sub_size_expr_opt = size_of_expr(subtype, *this);
714
715 if(!sub_size_expr_opt.has_value())
716 {
717 error().source_location = source_location;
718 error() << "failed to determine size of vector base type '"
719 << to_string(subtype) << "'" << eom;
720 throw 0;
721 }
722
723 simplify(sub_size_expr_opt.value(), *this);
724
726
727 if(!sub_size.has_value())
728 {
729 error().source_location=source_location;
730 error() << "failed to determine size of vector base type '"
731 << to_string(subtype) << "'" << eom;
732 throw 0;
733 }
734
735 if(*sub_size == 0)
736 {
737 error().source_location=source_location;
738 error() << "type had size 0: '" << to_string(subtype) << "'" << eom;
739 throw 0;
740 }
741
742 // adjust by width of base type
743 if(s % *sub_size != 0)
744 {
745 error().source_location=source_location;
746 error() << "vector size (" << s
747 << ") expected to be multiple of base type size (" << *sub_size
748 << ")" << eom;
749 throw 0;
750 }
751
752 s /= *sub_size;
753
754 // produce the type with ID_vector
756 c_index_type(), subtype, from_integer(s, signed_size_type()));
757 new_type.add_source_location() = source_location;
758 new_type.size().add_source_location() = source_location;
759 type = new_type;
760}
761
763{
764 // These get replaced by symbol types later.
765 irep_idt identifier;
766
767 bool have_body=type.find(ID_components).is_not_nil();
768
770
771 // the type symbol, which may get re-used in other declarations, must not
772 // carry any qualifiers (other than transparent_union, which isn't really a
773 // qualifier)
775 remove_qualifiers.is_transparent_union =
776 original_qualifiers.is_transparent_union;
777 remove_qualifiers.write(type);
778
779 bool is_packed = type.get_bool(ID_C_packed);
781
782 if(type.find(ID_tag).is_nil())
783 {
784 // Anonymous? Must come with body.
786
787 // produce symbol
789 compound_symbol.location=type.source_location();
790
792
793 std::string typestr = type2name(compound_symbol.type, *this);
794 compound_symbol.base_name = "#anon#" + typestr;
795 compound_symbol.name="tag-#anon#"+typestr;
796 identifier=compound_symbol.name;
797
798 // We might already have the same anonymous union/struct,
799 // and this is simply ok. Note that the C standard treats
800 // these as different types.
801 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
802 {
803 symbolt *new_symbol;
804 move_symbol(compound_symbol, new_symbol);
805 }
806 }
807 else
808 {
809 identifier=type.find(ID_tag).get(ID_identifier);
810
811 // does it exist already?
812 symbol_table_baset::symbolst::const_iterator s_it =
813 symbol_table.symbols.find(identifier);
814
815 if(s_it==symbol_table.symbols.end())
816 {
817 // no, add new symbol
818 irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
819 type.remove(ID_tag);
820 type.set(ID_tag, base_name);
821
822 type_symbolt compound_symbol{identifier, type, mode};
823 compound_symbol.base_name=base_name;
824 compound_symbol.location=type.source_location();
825 compound_symbol.pretty_name=id2string(type.id())+" "+id2string(base_name);
826
828
829 // mark as incomplete
830 to_struct_union_type(compound_symbol.type).make_incomplete();
831
832 symbolt *new_symbol;
833 move_symbol(compound_symbol, new_symbol);
834
835 if(have_body)
836 {
838
839 new_symbol->type.swap(new_type);
840 }
841 }
842 else
843 {
844 // yes, it exists already
845 if(
846 s_it->second.type.id() == type.id() &&
847 to_struct_union_type(s_it->second.type).is_incomplete())
848 {
849 // Maybe we got a body now.
850 if(have_body)
851 {
852 irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
853 type.remove(ID_tag);
854 type.set(ID_tag, base_name);
855
858 }
859 }
860 else if(s_it->second.type.id() != type.id())
861 {
863 error() << "redefinition of '" << s_it->second.pretty_name << "'"
864 << " as different kind of tag" << eom;
865 throw 0;
866 }
867 else if(have_body)
868 {
870 error() << "redefinition of body of '" << s_it->second.pretty_name
871 << "'" << eom;
872 throw 0;
873 }
874 }
875 }
876
878
879 if(type.id() == ID_union)
880 tag_type = union_tag_typet(identifier);
881 else if(type.id() == ID_struct)
882 tag_type = struct_tag_typet(identifier);
883 else
885
886 tag_type.add_source_location() = type.source_location();
887 type.swap(tag_type);
888
889 original_qualifiers.write(type);
890
891 if(is_packed)
892 type.set(ID_C_packed, true);
893 if(alignment.is_not_nil())
895}
896
898 struct_union_typet &type)
899{
901
903 old_components.swap(components);
904
905 // We get these as declarations!
906 for(auto &decl : old_components)
907 {
908 // the arguments are member declarations or static assertions
909 PRECONDITION(decl.id() == ID_declaration);
910
911 ansi_c_declarationt &declaration=
912 to_ansi_c_declaration(static_cast<exprt &>(decl));
913
914 if(declaration.get_is_static_assert())
915 {
918 new_component.add_source_location()=declaration.source_location();
919 PRECONDITION(declaration.operands().size() == 2);
920 new_component.operands().swap(declaration.operands());
921 components.push_back(new_component);
922 }
923 else
924 {
925 // do first half of type
926 typecheck_type(declaration.type());
928
929 for(const auto &declarator : declaration.declarators())
930 {
932 declarator.get_base_name(), declaration.full_type(declarator));
933
934 // There may be a declarator, which we use as location for
935 // the component. Otherwise, use location of the declaration.
936 const source_locationt source_location =
937 declarator.get_name().empty() ? declaration.source_location()
938 : declarator.source_location();
939
940 new_component.add_source_location() = source_location;
941 new_component.set_pretty_name(declarator.get_base_name());
942
944
945 // the rules for anonymous members depend on the type and the compiler,
946 // just bit fields are accepted everywhere
947 if(
948 new_component.get_name().empty() &&
949 new_component.type().id() != ID_c_bit_field)
950 {
952 {
953 // Visual Studio rejects anything other than a struct or union
954 // declaration, but also accepts those when they introduce a tag
955 if(
956 new_component.type().id() != ID_struct_tag &&
957 new_component.type().id() != ID_union_tag)
958 {
960 "no members defined", source_location};
961 }
962 }
963 else
964 {
965 // GCC and Clang ignore anything other than an untagged struct or
966 // union; we could print a warning, but there isn't any ambiguity in
967 // semantics here. Printing a warning could elevate this to an error
968 // when compiling code with goto-cc with -Werror.
969 // Note that our type checking always creates a struct_tag/union_tag
970 // type, but only named struct/union types have an ID_tag member.
971 if(
972 new_component.type().id() == ID_struct_tag &&
974 .find(ID_tag)
975 .is_nil())
976 {
977 // ok, anonymous struct
978 }
979 else if(
980 new_component.type().id() == ID_union_tag &&
982 .find(ID_tag)
983 .is_nil())
984 {
985 // ok, anonymous union
986 }
987 else
988 {
989 continue;
990 }
991 }
992 }
993
994 if(!is_complete_type(new_component.type()) &&
995 (new_component.type().id()!=ID_array ||
996 !to_array_type(new_component.type()).is_incomplete()))
997 {
998 error().source_location = source_location;
999 error() << "incomplete type not permitted here" << eom;
1000 throw 0;
1001 }
1002
1003 if(new_component.type().id() == ID_empty)
1004 {
1005 error().source_location = source_location;
1006 error() << "void-typed member not permitted" << eom;
1007 throw 0;
1008 }
1009
1010 if(
1011 new_component.type().id() == ID_c_bit_field &&
1012 to_c_bit_field_type(new_component.type()).get_width() == 0 &&
1013 !new_component.get_name().empty())
1014 {
1016 "zero-width bit-field with declarator not permitted",
1017 source_location};
1018 }
1019
1020 components.push_back(new_component);
1021 }
1022 }
1023 }
1024
1025 unsigned anon_member_counter=0;
1026
1027 // scan for anonymous members, and name them
1028 for(auto &member : components)
1029 {
1030 if(!member.get_name().empty())
1031 continue;
1032
1033 member.set_name("$anon"+std::to_string(anon_member_counter++));
1034 member.set_anonymous(true);
1035 }
1036
1037 // scan for duplicate members
1038
1039 {
1040 std::unordered_set<irep_idt> members;
1041
1042 for(const auto &c : components)
1043 {
1044 if(!members.insert(c.get_name()).second)
1045 {
1046 error().source_location = c.source_location();
1047 error() << "duplicate member '" << c.get_name() << '\'' << eom;
1048 throw 0;
1049 }
1050 }
1051 }
1052
1053 // We allow an incomplete (C99) array as _last_ member!
1054 // Zero-length is allowed everywhere.
1055
1056 if(type.id()==ID_struct ||
1057 type.id()==ID_union)
1058 {
1059 for(struct_union_typet::componentst::iterator
1060 it=components.begin();
1061 it!=components.end();
1062 it++)
1063 {
1064 typet &c_type=it->type();
1065
1066 if(c_type.id()==ID_array &&
1067 to_array_type(c_type).is_incomplete())
1068 {
1069 // needs to be last member
1070 if(type.id()==ID_struct && it!=--components.end())
1071 {
1072 error().source_location=it->source_location();
1073 error() << "flexible struct member must be last member" << eom;
1074 throw 0;
1075 }
1076
1077 // make it zero-length
1080 }
1081 }
1082 }
1083
1084 // We may add some minimal padding inside and at
1085 // the end of structs and
1086 // as additional member for unions.
1087
1088 if(type.id()==ID_struct)
1089 add_padding(to_struct_type(type), *this);
1090 else if(type.id()==ID_union)
1091 add_padding(to_union_type(type), *this);
1092
1093 // finally, check _Static_assert inside the compound
1094 for(struct_union_typet::componentst::iterator
1095 it=components.begin();
1096 it!=components.end();
1097 ) // no it++
1098 {
1099 if(it->id()==ID_static_assert)
1100 {
1102 {
1103 error().source_location = it->source_location();
1104 error() << "static_assert not supported in compound body" << eom;
1105 throw 0;
1106 }
1107
1108 exprt &assertion = to_binary_expr(*it).op0();
1109 typecheck_expr(assertion);
1110 typecheck_expr(to_binary_expr(*it).op1());
1111 assertion = typecast_exprt(assertion, bool_typet());
1112 make_constant(assertion);
1113
1114 if(assertion.is_false())
1115 {
1116 error().source_location=it->source_location();
1117 error() << "failed _Static_assert" << eom;
1118 throw 0;
1119 }
1120 else if(!assertion.is_true())
1121 {
1122 // should warn/complain
1123 }
1124
1125 it=components.erase(it);
1126 }
1127 else
1128 it++;
1129 }
1130
1131 // Visual Studio strictly follows the C standard and does not permit empty
1132 // struct/union declarations
1133 if(
1134 components.empty() &&
1136 {
1138 "C requires that a struct or union has at least one member",
1139 type.source_location()};
1140 }
1141}
1142
1144 const mp_integer &min_value,
1145 const mp_integer &max_value) const
1146{
1148 {
1149 return signed_int_type();
1150 }
1151 else
1152 {
1153 // enum constants are at least 'int', but may be made larger.
1154 // 'Packing' has no influence.
1155 if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1156 min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1157 return signed_int_type();
1158 else if(max_value<(mp_integer(1)<<config.ansi_c.int_width) &&
1159 min_value>=0)
1160 return unsigned_int_type();
1161 else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width) &&
1162 min_value>=0)
1163 return unsigned_long_int_type();
1164 else if(max_value<(mp_integer(1)<<config.ansi_c.long_long_int_width) &&
1165 min_value>=0)
1167 else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1168 min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1169 return signed_long_int_type();
1170 else
1172 }
1173}
1174
1176 const mp_integer &min_value,
1177 const mp_integer &max_value,
1178 bool is_packed) const
1179{
1181 {
1182 return signed_int_type();
1183 }
1184 else
1185 {
1186 if(min_value<0)
1187 {
1188 // We'll want a signed type.
1189
1190 if(is_packed)
1191 {
1192 // If packed, there are smaller options.
1193 if(max_value<(mp_integer(1)<<(config.ansi_c.char_width-1)) &&
1194 min_value>=-(mp_integer(1)<<(config.ansi_c.char_width-1)))
1195 return signed_char_type();
1196 else if(max_value<(mp_integer(1)<<(config.ansi_c.short_int_width-1)) &&
1197 min_value>=-(mp_integer(1)<<(config.ansi_c.short_int_width-1)))
1198 return signed_short_int_type();
1199 }
1200
1201 if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1202 min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1203 return signed_int_type();
1204 else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1205 min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1206 return signed_long_int_type();
1207 else
1209 }
1210 else
1211 {
1212 // We'll want an unsigned type.
1213
1214 if(is_packed)
1215 {
1216 // If packed, there are smaller options.
1217 if(max_value<(mp_integer(1)<<config.ansi_c.char_width))
1218 return unsigned_char_type();
1219 else if(max_value<(mp_integer(1)<<config.ansi_c.short_int_width))
1220 return unsigned_short_int_type();
1221 }
1222
1223 if(max_value<(mp_integer(1)<<config.ansi_c.int_width))
1224 return unsigned_int_type();
1225 else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width))
1226 return unsigned_long_int_type();
1227 else
1229 }
1230 }
1231}
1232
1234{
1235 // These come with the declarations
1236 // of the enum constants as operands.
1237
1238 exprt &as_expr=static_cast<exprt &>(static_cast<irept &>(type));
1239 source_locationt source_location=type.source_location();
1240
1241 // We allow empty enums in the grammar to get better
1242 // error messages.
1243 if(as_expr.operands().empty())
1244 {
1245 error().source_location=source_location;
1246 error() << "empty enum" << eom;
1247 throw 0;
1248 }
1249
1250 const bool have_underlying_type =
1251 type.find_type(ID_enum_underlying_type).is_not_nil();
1252
1254 {
1256
1257 const typet &underlying_type =
1258 static_cast<const typet &>(type.find(ID_enum_underlying_type));
1259
1260 if(!is_signed_or_unsigned_bitvector(underlying_type))
1261 {
1262 std::ostringstream msg;
1263 msg << "non-integral type '" << underlying_type.get(ID_C_c_type)
1264 << "' is an invalid underlying type";
1265 throw invalid_source_file_exceptiont{msg.str(), source_location};
1266 }
1267 }
1268
1269 // enums start at zero;
1270 // we also track min and max to find a nice base type
1271 mp_integer value=0, min_value=0, max_value=0;
1272
1273 std::vector<c_enum_typet::c_enum_membert> enum_members;
1274 enum_members.reserve(as_expr.operands().size());
1275
1276 // We need to determine a width, and a signedness
1277 // to obtain an 'underlying type'.
1278 // We just do int, but gcc might pick smaller widths
1279 // if the type is marked as 'packed'.
1280 // gcc/clang may also pick a larger width. Visual Studio doesn't.
1281
1282 for(auto &op : as_expr.operands())
1283 {
1285 exprt &v=declaration.declarator().value();
1286
1287 if(v.is_not_nil()) // value given?
1288 {
1289 exprt tmp_v=v;
1292 simplify(tmp_v, *this);
1293 if(tmp_v.is_true())
1294 value=1;
1295 else if(tmp_v.is_false())
1296 value=0;
1297 else if(
1298 tmp_v.is_constant() && !to_integer(to_constant_expr(tmp_v), value))
1299 {
1300 }
1301 else
1302 {
1304 error() << "enum is not a constant" << eom;
1305 throw 0;
1306 }
1307 }
1308
1309 if(value<min_value)
1310 min_value=value;
1311 if(value>max_value)
1312 max_value=value;
1313
1315
1317 {
1320
1321 if(value < tmp.smallest() || value > tmp.largest())
1322 {
1323 std::ostringstream msg;
1324 msg << "enumerator value is not representable in the underlying type '"
1325 << constant_type.get(ID_C_c_type) << "'";
1326 throw invalid_source_file_exceptiont{msg.str(), v.source_location()};
1327 }
1328 }
1329 else
1330 {
1331 constant_type = enum_constant_type(min_value, max_value);
1332 }
1333
1334 v=from_integer(value, constant_type);
1335
1336 declaration.type()=constant_type;
1337 typecheck_declaration(declaration);
1338
1339 irep_idt base_name=
1340 declaration.declarator().get_base_name();
1341
1342 irep_idt identifier=
1343 declaration.declarator().get_name();
1344
1345 // store
1347 member.set_identifier(identifier);
1348 member.set_base_name(base_name);
1349 // Note: The value will be correctly set to a bv type when we know
1350 // the width of the bitvector
1351 member.set_value(integer2string(value));
1352 enum_members.push_back(member);
1353
1354 // produce value for next constant
1355 ++value;
1356 }
1357
1358 // Remove these now; we add them to the
1359 // c_enum symbol later.
1360 as_expr.operands().clear();
1361
1362 bool is_packed=type.get_bool(ID_C_packed);
1363
1364 // We use a subtype to store the underlying type.
1365 bitvector_typet underlying_type(ID_nil);
1366
1368 {
1369 underlying_type =
1371 }
1372 else
1373 {
1374 underlying_type = enum_underlying_type(min_value, max_value, is_packed);
1375 }
1376
1377 // Get the width to make the values have a bitvector type
1378 std::size_t width = underlying_type.get_width();
1379 for(auto &member : enum_members)
1380 {
1381 // Note: This is inefficient as it first turns integers to strings
1382 // and then turns them back to bvrep
1383 auto value = string2integer(id2string(member.get_value()));
1384 member.set_value(integer2bvrep(value, width));
1385 }
1386
1387 // tag?
1388 if(type.find(ID_tag).is_nil())
1389 {
1390 // None, it's anonymous. We generate a tag.
1391 std::string anon_identifier="#anon_enum";
1392
1393 for(const auto &member : enum_members)
1394 {
1395 anon_identifier+='$';
1396 anon_identifier+=id2string(member.get_base_name());
1397 anon_identifier+='=';
1398 anon_identifier+=id2string(member.get_value());
1399 }
1400
1401 if(is_packed)
1402 anon_identifier+="#packed";
1403
1405 }
1406
1407 irept &tag=type.add(ID_tag);
1408 irep_idt base_name=tag.get(ID_C_base_name);
1409 irep_idt identifier=tag.get(ID_identifier);
1410
1411 // Put into symbol table
1412 type_symbolt enum_tag_symbol{identifier, type, mode};
1413 enum_tag_symbol.location=source_location;
1414 enum_tag_symbol.is_file_local=true;
1415 enum_tag_symbol.base_name=base_name;
1416
1417 enum_tag_symbol.type.add_subtype() = underlying_type;
1418
1419 // throw in the enum members as 'body'
1420 to_c_enum_type(enum_tag_symbol.type).members() = std::move(enum_members);
1421
1422 // is it in the symbol table already?
1424
1425 if(existing_symbol)
1426 {
1427 // Yes.
1428 const symbolt &symbol = *existing_symbol;
1429
1430 if(symbol.type.id() != ID_c_enum)
1431 {
1432 error().source_location = source_location;
1433 error() << "use of tag that does not match previous declaration" << eom;
1434 throw 0;
1435 }
1436
1437 if(to_c_enum_type(symbol.type).is_incomplete())
1438 {
1439 // Ok, overwrite the type in the symbol table.
1440 // This gives us the members and the subtype.
1441 existing_symbol->type = enum_tag_symbol.type;
1442 }
1443 else
1444 {
1445 // We might already have the same anonymous enum, and this is
1446 // simply ok. Note that the C standard treats these as
1447 // different types.
1448 if(!base_name.empty())
1449 {
1451 error() << "redeclaration of enum tag" << eom;
1452 throw 0;
1453 }
1454 }
1455 }
1456 else
1457 {
1458 symbolt *new_symbol;
1459 move_symbol(enum_tag_symbol, new_symbol);
1460 }
1461
1462 // We produce a c_enum_tag as the resulting type.
1463 type.id(ID_c_enum_tag);
1464 type.remove(ID_tag);
1465 type.set(ID_identifier, identifier);
1466}
1467
1469{
1470 // It's just a tag.
1471
1472 if(type.find(ID_tag).is_nil())
1473 {
1475 error() << "anonymous enum tag without members" << eom;
1476 throw 0;
1477 }
1478
1479 if(type.find(ID_enum_underlying_type).is_not_nil())
1480 {
1482 warning() << "ignoring specification of underlying type for enum" << eom;
1483 }
1484
1485 source_locationt source_location=type.source_location();
1486
1487 irept &tag=type.add(ID_tag);
1488 irep_idt base_name=tag.get(ID_C_base_name);
1489 irep_idt identifier=tag.get(ID_identifier);
1490
1491 // is it in the symbol table?
1492 symbol_table_baset::symbolst::const_iterator s_it =
1493 symbol_table.symbols.find(identifier);
1494
1495 if(s_it!=symbol_table.symbols.end())
1496 {
1497 // Yes.
1498 const symbolt &symbol=s_it->second;
1499
1500 if(symbol.type.id() != ID_c_enum)
1501 {
1502 error().source_location=source_location;
1503 error() << "use of tag that does not match previous declaration" << eom;
1504 throw 0;
1505 }
1506 }
1507 else
1508 {
1509 // no, add it as an incomplete c_enum
1510 c_enum_typet new_type(signed_int_type()); // default subtype
1511 new_type.add(ID_tag)=tag;
1512 new_type.make_incomplete();
1513
1515 enum_tag_symbol.location=source_location;
1516 enum_tag_symbol.is_file_local=true;
1517 enum_tag_symbol.base_name=base_name;
1518
1519 symbolt *new_symbol;
1520 move_symbol(enum_tag_symbol, new_symbol);
1521 }
1522
1523 // Clean up resulting type
1524 type.remove(ID_tag);
1525 type.set_identifier(identifier);
1526}
1527
1529{
1531
1532 mp_integer i;
1533
1534 {
1535 exprt &width_expr=static_cast<exprt &>(type.add(ID_size));
1536
1539
1541 {
1543 error() << "failed to convert bit field width" << eom;
1544 throw 0;
1545 }
1546
1547 if(i<0)
1548 {
1550 error() << "bit field width is negative" << eom;
1551 throw 0;
1552 }
1553
1555 type.remove(ID_size);
1556 }
1557
1558 const typet &underlying_type = type.underlying_type();
1559
1560 std::size_t sub_width=0;
1561
1562 if(underlying_type.id() == ID_bool)
1563 {
1564 // This is the 'proper' bool.
1565 sub_width=1;
1566 }
1567 else if(
1568 underlying_type.id() == ID_signedbv ||
1569 underlying_type.id() == ID_unsignedbv || underlying_type.id() == ID_c_bool)
1570 {
1571 sub_width = to_bitvector_type(underlying_type).get_width();
1572 }
1573 else if(underlying_type.id() == ID_c_enum_tag)
1574 {
1575 // These point to an enum, which has a sub-subtype,
1576 // which may be smaller or larger than int, and we thus have
1577 // to check.
1578 const auto &c_enum_type =
1579 to_c_enum_type(follow_tag(to_c_enum_tag_type(underlying_type)));
1580
1581 if(c_enum_type.is_incomplete())
1582 {
1584 error() << "bit field has incomplete enum type" << eom;
1585 throw 0;
1586 }
1587
1588 sub_width = to_bitvector_type(c_enum_type.underlying_type()).get_width();
1589 }
1590 else
1591 {
1593 error() << "bit field with non-integer type: " << to_string(underlying_type)
1594 << eom;
1595 throw 0;
1596 }
1597
1598 if(i>sub_width)
1599 {
1601 error() << "bit field (" << i
1602 << " bits) larger than type (" << sub_width << " bits)"
1603 << eom;
1604 throw 0;
1605 }
1606}
1607
1609{
1610 // save location
1611 source_locationt source_location=type.source_location();
1612
1613 // retain the qualifiers as is
1614 c_qualifierst c_qualifiers;
1615 c_qualifiers.read(type);
1616
1617 const auto &as_expr = (const exprt &)type;
1618
1619 if(!as_expr.has_operands())
1620 {
1621 typet t=static_cast<const typet &>(type.find(ID_type_arg));
1622 typecheck_type(t);
1623 type.swap(t);
1624 }
1625 else
1626 {
1627 exprt expr = to_unary_expr(as_expr).op();
1628 typecheck_expr(expr);
1629
1630 // undo an implicit address-of
1631 if(expr.id()==ID_address_of &&
1632 expr.get_bool(ID_C_implicit))
1633 {
1634 expr = to_address_of_expr(expr).object();
1635 }
1636
1637 type.swap(expr.type());
1638 }
1639
1640 type.add_source_location()=source_location;
1641 c_qualifiers.write(type);
1642}
1643
1645{
1646 const irep_idt &identifier = to_typedef_type(type).get_identifier();
1647
1648 symbol_table_baset::symbolst::const_iterator s_it =
1649 symbol_table.symbols.find(identifier);
1650
1651 if(s_it == symbol_table.symbols.end())
1652 {
1654 error() << "typedef symbol '" << identifier << "' not found" << eom;
1655 throw 0;
1656 }
1657
1658 const symbolt &symbol = s_it->second;
1659
1660 if(!symbol.is_type)
1661 {
1663 error() << "expected type symbol for typedef" << eom;
1664 throw 0;
1665 }
1666
1667 // overwrite, but preserve (add) any qualifiers and other flags
1668
1669 c_qualifierst c_qualifiers(type);
1670 bool is_packed = type.get_bool(ID_C_packed);
1672
1673 c_qualifiers += c_qualifierst(symbol.type);
1674 type = symbol.type;
1675 c_qualifiers.write(type);
1676
1677 if(is_packed)
1678 type.set(ID_C_packed, true);
1679 if(alignment.is_not_nil())
1681
1682 // CPROVER extensions
1683 if(symbol.base_name == CPROVER_PREFIX "rational")
1684 {
1685 type=rational_typet();
1686 }
1687 else if(symbol.base_name == CPROVER_PREFIX "integer")
1688 {
1689 type=integer_typet();
1690 }
1691}
1692
1694{
1695 if(type.id()==ID_array)
1696 {
1697 source_locationt source_location=type.source_location();
1698 type = pointer_type(to_array_type(type).element_type());
1699 type.add_source_location()=source_location;
1700 }
1701 else if(type.id()==ID_code)
1702 {
1703 // see ISO/IEC 9899:1999 page 199 clause 8,
1704 // may be hidden in typedef
1705 source_locationt source_location=type.source_location();
1706 type=pointer_type(type);
1707 type.add_source_location()=source_location;
1708 }
1709 else if(type.id()==ID_KnR)
1710 {
1711 // any KnR args without type yet?
1712 type=signed_int_type(); // the default is integer!
1713 // no source location
1714 }
1715}
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:182
signedbv_typet signed_long_int_type()
Definition c_types.cpp:77
signedbv_typet signed_char_type()
Definition c_types.cpp:139
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:98
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:91
unsignedbv_typet size_type()
Definition c_types.cpp:55
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
signedbv_typet signed_size_type()
Definition c_types.cpp:71
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:84
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:190
signedbv_typet signed_short_int_type()
Definition c_types.cpp:34
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:48
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:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:763
bool is_complete() const
Definition std_types.h:808
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
typet & index_type_nonconst()
The type of the index expressions into any instance of this type.
Definition std_types.h:777
Base class of fixed-width bit-vector types.
Definition std_types.h:865
void set_width(std::size_t width)
Definition std_types.h:881
std::size_t get_width() const
Definition std_types.h:876
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 override
virtual void read(const typet &src) override
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: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:1077
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:39
bool empty() const
Definition dstring.h:90
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:223
source_locationt & add_source_location()
Definition expr.h:228
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:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
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:111
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
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:113
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:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:82
const typet & find_type(const irep_idt &name) const
Definition type.h:87
source_locationt & add_source_location()
Definition type.h:77
const source_locationt & source_location() const
Definition type.h:72
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:1008
#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:456
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.
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:18
#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:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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:175
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45