CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_compound_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
14#ifdef DEBUG
15#include <iostream>
16#endif
17
18#include <util/arith_tools.h>
19#include <util/c_types.h>
20#include <util/std_types.h>
22
23#include <ansi-c/c_qualifiers.h>
24
26#include "cpp_name.h"
27#include "cpp_type2name.h"
28#include "cpp_util.h"
29
30#include <algorithm>
31
33{
34 if(type.id()==ID_const)
35 return true;
36 else if(type.id()==ID_merged_type)
37 {
38 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
39 {
40 if(has_const(subtype))
41 return true;
42 }
43
44 return false;
45 }
46 else
47 return false;
48}
49
51{
52 if(type.id()==ID_volatile)
53 return true;
54 else if(type.id()==ID_merged_type)
55 {
56 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
57 {
58 if(has_volatile(subtype))
59 return true;
60 }
61
62 return false;
63 }
64 else
65 return false;
66}
67
69{
70 if(type.id() == ID_auto)
71 return true;
72 else if(
73 type.id() == ID_merged_type || type.id() == ID_frontend_pointer ||
74 type.id() == ID_pointer)
75 {
76 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
77 {
78 if(has_auto(subtype))
79 return true;
80 }
81
82 return false;
83 }
84 else
85 return false;
86}
87
89 const irep_idt &base_name,
90 bool has_body,
92{
93 // The scope of a compound identifier is difficult,
94 // and is different from C.
95 //
96 // For instance:
97 // class A { class B {} } --> A::B
98 // class A { class B; } --> A::B
99 // class A { class B *p; } --> ::B
100 // class B { }; class A { class B *p; } --> ::B
101 // class B { }; class A { class B; class B *p; } --> A::B
102
103 // If there is a body, or it's a tag-only declaration,
104 // it's always in the current scope, even if we already have
105 // it in an upwards scope.
106
107 if(has_body || tag_only_declaration)
108 return cpp_scopes.current_scope();
109
110 // No body. Not a tag-only-declaration.
111 // Check if we have it already. If so, take it.
112
113 // we should only look for tags, but we don't
114 const auto id_set =
116
117 for(const auto &id : id_set)
118 if(id->is_class())
119 return static_cast<cpp_scopet &>(id->get_parent());
120
121 // Tags without body that we don't have already
122 // and that are not a tag-only declaration go into
123 // the global scope of the namespace.
125}
126
128 struct_union_typet &type)
129{
130 // first save qualifiers
132
133 // now clear them from the type
134 type.remove(ID_C_constant);
135 type.remove(ID_C_volatile);
137
138 // get the tag name
139 bool has_tag=type.find(ID_tag).is_not_nil();
140 irep_idt base_name;
141 cpp_scopet *dest_scope=nullptr;
142 bool has_body=type.find(ID_body).is_not_nil();
144 bool is_union = type.id() == ID_union;
145
146 if(!has_tag)
147 {
148 // most of these should be named by now; see
149 // cpp_declarationt::name_anon_struct_union()
150
151 base_name=std::string("#anon_")+std::to_string(++anon_counter);
152 type.set(ID_C_is_anonymous, true);
154 }
155 else
156 {
157 const cpp_namet &cpp_name=
158 to_cpp_name(type.find(ID_tag));
159
160 // scope given?
161 if(cpp_name.is_simple_name())
162 {
163 base_name=cpp_name.get_base_name();
164
165 // anonymous structs always go into the current scope
168 else
169 dest_scope=&tag_scope(base_name, has_body, tag_only_declaration);
170 }
171 else
172 {
177 &cpp_typecheck_resolve.resolve_scope(cpp_name, base_name, t_args);
178 }
179 }
180
181 // The identifier 'tag-X' matches what the C front-end does!
182 // The hyphen is deliberate to avoid collisions with other
183 // identifiers.
184 const irep_idt symbol_name=
185 dest_scope->prefix+
186 "tag-"+id2string(base_name)+
187 dest_scope->suffix;
188
189 // check if we have it already
190
192 {
193 // we do!
194 const symbolt &symbol=*maybe_symbol;
195
196 if(has_body)
197 {
198 if(
199 symbol.type.id() == type.id() &&
200 to_struct_union_type(symbol.type).is_incomplete())
201 {
202 // a previously incomplete struct/union becomes complete
204 writeable_symbol.type.swap(type);
206 }
207 else if(symbol.type.get_bool(ID_C_is_anonymous))
208 {
209 // we silently ignore
210 }
211 else
212 {
214 error() << "compound tag '" << base_name << "' declared previously\n"
215 << "location of previous definition: " << symbol.location
216 << eom;
217 throw 0;
218 }
219 }
220 else if(symbol.type.id() != type.id())
221 {
223 error() << "redefinition of '" << symbol.pretty_name << "'"
224 << " as different kind of tag" << eom;
225 throw 0;
226 }
227 }
228 else
229 {
230 // produce new symbol
231 type_symbolt symbol{symbol_name, type, ID_cpp};
232 symbol.base_name=base_name;
233 symbol.location=type.source_location();
234 symbol.module=module;
235 symbol.pretty_name=
237 id2string(symbol.base_name)+
239 symbol.type.set(
240 ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
241
242 // move early, must be visible before doing body
243 symbolt *new_symbol;
244
245 if(symbol_table.move(symbol, new_symbol))
246 {
247 error().source_location=symbol.location;
248 error() << "cpp_typecheckt::typecheck_compound_type: "
249 << "symbol_table.move() failed" << eom;
250 throw 0;
251 }
252
253 // put into dest_scope
254 cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol, *dest_scope);
255
257 id.is_scope=true;
258 id.prefix=cpp_scopes.current_scope().prefix+
259 id2string(new_symbol->base_name)+
261 id.class_identifier=new_symbol->name;
262 id.id_class=cpp_idt::id_classt::CLASS;
263
264 if(has_body)
265 typecheck_compound_body(*new_symbol);
266 else
267 {
268 struct_union_typet new_type(new_symbol->type.id());
269 new_type.set(ID_tag, new_symbol->base_name);
270 new_type.make_incomplete();
271 new_type.add_source_location() = type.source_location();
272 new_symbol->type.swap(new_type);
273 }
274 }
275
276 if(is_union)
277 {
278 // create union tag
280 qualifiers.write(tag_type);
281 type.swap(tag_type);
282 }
283 else
284 {
285 // create struct tag
287 qualifiers.write(tag_type);
288 type.swap(tag_type);
289 }
290}
291
293 const symbolt &symbol,
294 const cpp_declarationt &declaration,
295 cpp_declaratort &declarator,
296 struct_typet::componentst &components,
297 const irep_idt &access,
298 bool is_static,
299 bool is_typedef,
300 bool is_mutable)
301{
302 bool is_cast_operator=
303 declaration.type().id()=="cpp-cast-operator";
304
306 {
308 declarator.name().get_sub().size() == 2 &&
309 declarator.name().get_sub().front().id() == ID_operator);
310
311 typet type=static_cast<typet &>(declarator.name().get_sub()[1]);
312 declarator.type().add_subtype() = type;
313
314 cpp_namet::namet name("(" + cpp_type2name(type) + ")");
315 declarator.name().get_sub().back().swap(name);
316 }
317
318 typet final_type=
319 declarator.merge_type(declaration.type());
320
321 // this triggers template elaboration
322 elaborate_class_template(final_type);
323
324 typecheck_type(final_type);
325
326 if(final_type.id() == ID_empty)
327 {
328 error().source_location = declaration.type().source_location();
329 error() << "void-typed member not permitted" << eom;
330 throw 0;
331 }
332
334 cpp_name.swap(declarator.name());
335
336 irep_idt base_name;
337
338 if(cpp_name.is_nil())
339 {
340 // Yes, there can be members without name.
341 base_name=irep_idt();
342 }
343 else if(cpp_name.is_simple_name())
344 {
345 base_name=cpp_name.get_base_name();
346 }
347 else
348 {
349 error().source_location=cpp_name.source_location();
350 error() << "declarator in compound needs to be simple name"
351 << eom;
352 throw 0;
353 }
354
355 bool is_method=!is_typedef && final_type.id()==ID_code;
356 bool is_constructor=declaration.is_constructor();
357 bool is_destructor=declaration.is_destructor();
358 bool is_virtual=declaration.member_spec().is_virtual();
359 bool is_explicit=declaration.member_spec().is_explicit();
360 bool is_inline=declaration.member_spec().is_inline();
361
362 final_type.set(ID_C_member_name, symbol.name);
363
364 // first do some sanity checks
365
366 if(is_virtual && !is_method)
367 {
368 error().source_location=cpp_name.source_location();
369 error() << "only methods can be virtual" << eom;
370 throw 0;
371 }
372
373 if(is_inline && !is_method)
374 {
375 error().source_location=cpp_name.source_location();
376 error() << "only methods can be inlined" << eom;
377 throw 0;
378 }
379
380 if(is_virtual && is_static)
381 {
382 error().source_location=cpp_name.source_location();
383 error() << "static methods cannot be virtual" << eom;
384 throw 0;
385 }
386
387 if(is_cast_operator && is_static)
388 {
389 error().source_location=cpp_name.source_location();
390 error() << "cast operators cannot be static" << eom;
391 throw 0;
392 }
393
394 if(is_constructor && is_virtual)
395 {
396 error().source_location=cpp_name.source_location();
397 error() << "constructors cannot be virtual" << eom;
398 throw 0;
399 }
400
401 if(!is_constructor && is_explicit)
402 {
403 error().source_location=cpp_name.source_location();
404 error() << "only constructors can be explicit" << eom;
405 throw 0;
406 }
407
408 if(is_constructor && base_name != symbol.base_name)
409 {
410 error().source_location=cpp_name.source_location();
411 error() << "member function must return a value or void" << eom;
412 throw 0;
413 }
414
415 if(is_destructor &&
416 base_name!="~"+id2string(symbol.base_name))
417 {
418 error().source_location=cpp_name.source_location();
419 error() << "destructor with wrong name" << eom;
420 throw 0;
421 }
422
423 // now do actual work
424
425 irep_idt identifier;
426
427 // the below is a temporary hack
428 // if(is_method || is_static)
429 if(id2string(cpp_scopes.current_scope().prefix).find("#anon")==
430 std::string::npos ||
431 is_method || is_static)
432 {
433 // Identifiers for methods include the scope prefix.
434 // Identifiers for static members include the scope prefix.
435 identifier=
437 id2string(base_name);
438 }
439 else
440 {
441 // otherwise, we keep them simple
442 identifier=base_name;
443 }
444
445 struct_typet::componentt component(identifier, final_type);
447 component.set_base_name(base_name);
448 component.set_pretty_name(base_name);
449 component.add_source_location()=cpp_name.source_location();
450
451 if(cpp_name.is_operator())
452 {
453 component.set(ID_is_operator, true);
454 component.type().set(ID_C_is_operator, true);
455 }
456
459
460 if(declaration.member_spec().is_explicit())
461 component.set(ID_is_explicit, true);
462
463 // either blank, const, volatile, or const volatile
464 const typet &method_qualifier=
465 static_cast<const typet &>(declarator.add(ID_method_qualifier));
466
467 if(is_static)
468 {
469 component.set(ID_is_static, true);
470 component.type().set(ID_C_is_static, true);
471 }
472
473 if(is_typedef)
474 component.set(ID_is_type, true);
475
476 if(is_mutable)
477 component.set(ID_is_mutable, true);
478
479 exprt &value=declarator.value();
481
482 if(is_method)
483 {
484 if(
485 value.id() == ID_code &&
486 to_code(value).get_statement() == ID_cpp_delete)
487 {
488 value.make_nil();
490 }
491
492 component.set(ID_is_inline, declaration.member_spec().is_inline());
493
494 // the 'virtual' name of the function
495 std::string virtual_name = id2string(component.get_base_name()) +
497
498 if(has_const(method_qualifier))
499 virtual_name+="$const";
500
501 if(has_volatile(method_qualifier))
502 virtual_name += "$volatile";
503
504 if(to_code_type(component.type()).return_type().id() == ID_destructor)
505 virtual_name="@dtor";
506
507 // The method may be virtual implicitly.
508 std::set<irep_idt> virtual_bases;
509
510 for(const auto &comp : components)
511 {
512 if(comp.get_bool(ID_is_virtual))
513 {
515 {
516 is_virtual=true;
517 const code_typet &code_type=to_code_type(comp.type());
519 !code_type.parameters().empty(), "must have parameters");
520 const typet &pointer_type=code_type.parameters()[0].type();
522 pointer_type.id() == ID_pointer, "this must be pointer");
523 virtual_bases.insert(
524 to_pointer_type(pointer_type).base_type().get(ID_identifier));
525 }
526 }
527 }
528
529 if(!is_virtual)
530 {
532 symbol, component, initializers,
533 method_qualifier, value);
534
535 if(!value.is_nil() && !is_static)
536 {
537 error().source_location=cpp_name.source_location();
538 error() << "no initialization allowed here" << eom;
539 throw 0;
540 }
541 }
542 else // virtual
543 {
544 component.type().set(ID_C_is_virtual, true);
546
547 // Check if it is a pure virtual method
548 if(value.is_not_nil() && value.is_constant())
549 {
550 mp_integer i;
551 to_integer(to_constant_expr(value), i);
552 if(i!=0)
553 {
554 error().source_location = declarator.name().source_location();
555 error() << "expected 0 to mark pure virtual method, got " << i << eom;
556 throw 0;
557 }
558 component.set(ID_is_pure_virtual, true);
559 value.make_nil();
560 }
561
563 symbol,
564 component,
566 method_qualifier,
567 value);
568
569 // get the virtual-table symbol type
570 irep_idt vt_name="virtual_table::"+id2string(symbol.name);
571
573 {
574 // first time: create a virtual-table symbol type
576 vt_symb_type.base_name="virtual_table::"+id2string(symbol.base_name);
577 vt_symb_type.pretty_name=vt_symb_type.base_name;
578 vt_symb_type.module=module;
579 vt_symb_type.location=symbol.location;
580 vt_symb_type.type.set(ID_name, vt_symb_type.name);
581
582 const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
584
585 // add a virtual-table pointer
587 id2string(symbol.name) + "::@vtable_pointer",
589 compo.set_base_name("@vtable_pointer");
590 compo.set_pretty_name(id2string(symbol.base_name) + "@vtable_pointer");
591 compo.set(ID_is_vtptr, true);
593 components.push_back(compo);
595 }
596
598 INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");
600
602 component.set(ID_is_virtual, is_virtual);
603
604 // add an entry to the virtual table
607 pointer_type(component.type()));
608 vt_entry.set_base_name(virtual_name);
609 vt_entry.set_pretty_name(virtual_name);
611 vt_entry.add_source_location()=symbol.location;
612 virtual_table.components().push_back(vt_entry);
613
614 // take care of overloading
615 while(!virtual_bases.empty())
616 {
618
619 // a new function that does 'late casting' of the 'this' parameter
621 id2string(component.get_name()) + "::" + id2string(virtual_base),
622 component.type(),
623 symbol.mode};
624 func_symb.base_name = component.get_base_name();
625 func_symb.pretty_name = component.get_base_name();
626 func_symb.module=module;
627 func_symb.location=component.source_location();
628
629 // change the type of the 'this' pointer
631 code_typet::parametert &this_parameter = code_type.parameters().front();
633 .base_type()
635
636 // create symbols for the parameters
637 code_typet::parameterst &args=code_type.parameters();
638 std::size_t i=0;
639 for(auto &arg : args)
640 {
641 irep_idt param_base_name = arg.get_base_name();
642
643 if(param_base_name.empty())
644 param_base_name = "arg" + std::to_string(i++);
645
648 arg.type(),
649 symbol.mode};
650 arg_symb.base_name = param_base_name;
651 arg_symb.pretty_name = param_base_name;
652 arg_symb.location=func_symb.location;
653
654 arg.set_identifier(arg_symb.name);
655
656 // add the parameter to the symbol table
657 const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
659 }
660
661 // do the body of the function
663 lookup(args[0].get_identifier()).symbol_expr(),
664 to_code_type(component.type()).parameters()[0].type());
665
667 symbol_exprt(component.get_name(), component.type()),
668 {late_cast},
671 expr_call.arguments().reserve(args.size());
672
673 for(const auto &arg : args)
674 {
675 expr_call.arguments().push_back(
676 lookup(arg.get_identifier()).symbol_expr());
677 }
678
679 if(code_type.return_type().id()!=ID_empty &&
680 code_type.return_type().id()!=ID_destructor)
681 {
682 expr_call.type()=to_code_type(component.type()).return_type();
683
686 }
687 else
688 {
691 }
692
693 // add this new function to the list of components
694
696 new_compo.type()=func_symb.type;
697 new_compo.set_name(func_symb.name);
698 components.push_back(new_compo);
699
700 // add the function to the symbol table
701 {
702 const bool failed=!symbol_table.insert(std::move(func_symb)).second;
704 }
705
707
708 // next base
709 virtual_bases.erase(virtual_bases.begin());
710 }
711 }
712 }
713
714 if(is_static && !is_method) // static non-method member
715 {
716 // add as global variable to symbol_table
717 symbolt static_symbol{identifier, component.type(), symbol.mode};
718 static_symbol.base_name = component.get_base_name();
719 static_symbol.is_lvalue=true;
720 static_symbol.is_static_lifetime=true;
721 static_symbol.location=cpp_name.source_location();
722 static_symbol.is_extern=true;
723
724 // TODO: not sure about this: should be defined separately!
726
727 symbolt *new_symbol;
728 if(symbol_table.move(static_symbol, new_symbol))
729 {
730 error().source_location=cpp_name.source_location();
731 error() << "redeclaration of static member '" << static_symbol.base_name
732 << "'" << eom;
733 throw 0;
734 }
735
736 if(value.is_not_nil())
737 {
738 if(cpp_is_pod(new_symbol->type))
739 {
740 new_symbol->value.swap(value);
742 }
743 else
744 {
746
748 ops.push_back(value);
750 CHECK_RETURN(defcode.has_value());
751
752 new_symbol->value.swap(defcode.value());
753 }
754 }
755 }
756
757 // array members must have fixed size
759
761
762 components.push_back(component);
763}
764
767{
768 if(type.id()==ID_array)
769 {
771
772 if(array_type.size().is_not_nil())
773 {
774 if(array_type.size().id() == ID_symbol)
775 {
776 const symbol_exprt &s = to_symbol_expr(array_type.size());
777 const symbolt &symbol = lookup(s.get_identifier());
778
779 if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
780 array_type.size() = symbol.value;
781 }
782
784 }
785
786 // recursive call for multi-dimensional arrays
787 check_fixed_size_array(array_type.element_type());
788 }
789}
790
792 const struct_union_typet::componentt &compound)
793{
794 const irep_idt &base_name=compound.get_base_name();
795 const irep_idt &name=compound.get_name();
796
797 // nothing to do if no base_name (e.g., an anonymous bitfield)
798 if(base_name.empty())
799 return;
800
801 if(compound.type().id()==ID_code)
802 {
803 // put the symbol into scope
804 cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
807 id.identifier=name;
808 id.class_identifier=cpp_scopes.current_scope().identifier;
809 id.is_member=true;
810 id.is_constructor =
811 to_code_type(compound.type()).return_type().id() == ID_constructor;
812 id.is_method=true;
813 id.is_static_member=compound.get_bool(ID_is_static);
814
815 // create function block-scope in the scope
818 irep_idt(std::string("$block:") + base_name.c_str()));
819
821 id_block.identifier=name;
822 id_block.class_identifier=cpp_scopes.current_scope().identifier;
823 id_block.is_method=true;
824 id_block.is_static_member=compound.get_bool(ID_is_static);
825
826 id_block.is_scope=true;
827 id_block.prefix = compound.get_string(ID_prefix);
828 cpp_scopes.id_map[id.identifier]=&id_block;
829 }
830 else
831 {
832 // check if it's already there
833 const auto id_set =
835
836 for(const auto &id_it : id_set)
837 {
838 const cpp_idt &id=*id_it;
839
840 // the name is already in the scope
841 // this is ok if they belong to different categories
842 if(!id.is_class() && !id.is_enum())
843 {
845 error() << "'" << base_name << "' already in compound scope" << eom;
846 throw 0;
847 }
848 }
849
850 // put into the scope
851 cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
852 id.id_class=compound.get_bool(ID_is_type)?
855 id.identifier=name;
856 id.class_identifier=cpp_scopes.current_scope().identifier;
857 id.is_member=true;
858 id.is_method=false;
859 id.is_static_member=compound.get_bool(ID_is_static);
860 }
861}
862
864 symbolt &symbol,
865 cpp_declarationt &declaration)
866{
867 // A friend of a class can be a function/method,
868 // or a struct/class/union type.
869
870 if(declaration.is_template())
871 {
872 error().source_location=declaration.type().source_location();
873 error() << "friend template not supported" << eom;
874 throw 0;
875 }
876
877 // we distinguish these whether there is a declarator
878 if(declaration.declarators().empty())
879 {
880 typet &ftype=declaration.type();
881
882 // must be struct or union
883 if(ftype.id()!=ID_struct && ftype.id()!=ID_union)
884 {
885 error().source_location=declaration.type().source_location();
886 error() << "unexpected friend" << eom;
887 throw 0;
888 }
889
890 if(ftype.find(ID_body).is_not_nil())
891 {
892 error().source_location=declaration.type().source_location();
893 error() << "friend declaration must not have compound body" << eom;
894 throw 0;
895 }
896
897 cpp_save_scopet saved_scope(cpp_scopes);
901
902 return;
903 }
904
905 // It should be a friend function.
906 // Do the declarators.
907
908#ifdef DEBUG
909 std::cout << "friend declaration: " << declaration.pretty() << '\n';
910#endif
911
912 for(auto &sub_it : declaration.declarators())
913 {
914#ifdef DEBUG
915 std::cout << "decl: " << sub_it.pretty() << "\n with value "
916 << sub_it.value().pretty() << '\n';
917 std::cout << " scope: " << cpp_scopes.current_scope().prefix << '\n';
918#endif
919
920 if(sub_it.value().is_not_nil())
921 declaration.member_spec().set_inline(true);
922
924 cpp_declarator_converter.is_friend = true;
926 declaration.type(),
927 declaration.storage_spec(),
928 declaration.member_spec(),
929 sub_it);
932 }
933}
934
936{
937 cpp_save_scopet saved_scope(cpp_scopes);
938
939 // enter scope of compound
940 cpp_scopes.set_scope(symbol.name);
941
942 PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union);
943
944 struct_union_typet &type=
946
947 // pull the base types in
948 if(!type.find(ID_bases).get_sub().empty())
949 {
950 if(type.id()==ID_union)
951 {
953 error() << "union types must not have bases" << eom;
954 throw 0;
955 }
956
958 }
959
960 exprt &body=static_cast<exprt &>(type.add(ID_body));
962
963 symbol.type.set(ID_name, symbol.name);
964
965 // default access
967
968 bool found_ctor=false;
969 bool found_dtor=false;
970
971 // we first do everything _but_ the constructors
972
973 Forall_operands(it, body)
974 {
975 if(it->id()==ID_cpp_declaration)
976 {
977 cpp_declarationt &declaration=
979
980 if(declaration.member_spec().is_friend())
981 {
982 typecheck_friend_declaration(symbol, declaration);
983 continue; // done
984 }
985
986 if(declaration.is_template())
987 {
988 // remember access mode
989 declaration.set(ID_C_access, access);
990 convert_template_declaration(declaration);
991 continue;
992 }
993
994 if(declaration.type().id().empty())
995 continue;
996
997 bool is_typedef=declaration.is_typedef();
998
999 // is it tag-only?
1000 if(declaration.type().id()==ID_struct ||
1001 declaration.type().id()==ID_union ||
1002 declaration.type().id()==ID_c_enum)
1003 if(declaration.declarators().empty())
1004 declaration.type().set(ID_C_tag_only_declaration, true);
1005
1006 declaration.name_anon_struct_union();
1007 typecheck_type(declaration.type());
1008
1009 bool is_static=declaration.storage_spec().is_static();
1010 bool is_mutable=declaration.storage_spec().is_mutable();
1011
1012 if(declaration.storage_spec().is_extern() ||
1013 declaration.storage_spec().is_auto() ||
1014 declaration.storage_spec().is_register())
1015 {
1016 error().source_location=declaration.storage_spec().location();
1017 error() << "invalid storage class specified for field" << eom;
1018 throw 0;
1019 }
1020
1021 // anonymous member?
1022 if(
1023 declaration.declarators().empty() &&
1024 ((declaration.type().id() == ID_struct_tag &&
1025 follow_tag(to_struct_tag_type(declaration.type()))
1026 .get_bool(ID_C_is_anonymous)) ||
1027 (declaration.type().id() == ID_union_tag &&
1028 follow_tag(to_union_tag_type(declaration.type()))
1029 .get_bool(ID_C_is_anonymous)) ||
1030 declaration.type().get_bool(ID_C_is_anonymous)))
1031 {
1032 // we only allow this on struct/union types
1033 if(
1034 declaration.type().id() != ID_union_tag &&
1035 declaration.type().id() != ID_struct_tag)
1036 {
1037 error().source_location=declaration.type().source_location();
1038 error() << "member declaration does not declare anything"
1039 << eom;
1040 throw 0;
1041 }
1042
1044 declaration, access, components);
1045
1046 continue;
1047 }
1048
1049 // declarators
1050 for(auto &declarator : declaration.declarators())
1051 {
1052 // Skip the constructors until all the data members
1053 // are discovered
1054 if(declaration.is_destructor())
1055 found_dtor=true;
1056
1057 if(declaration.is_constructor())
1058 {
1059 found_ctor=true;
1060 continue;
1061 }
1062
1064 symbol,
1065 declaration, declarator, components,
1066 access, is_static, is_typedef, is_mutable);
1067 }
1068 }
1069 else if(it->id()=="cpp-public")
1071 else if(it->id()=="cpp-private")
1073 else if(it->id()=="cpp-protected")
1075 else
1076 {
1077 }
1078 }
1079
1080 // Add the default dtor, if needed
1081 // (we have to do the destructor before building the virtual tables,
1082 // as the destructor may be virtual!)
1083
1084 if((found_ctor || !cpp_is_pod(symbol.type)) && !found_dtor)
1085 {
1086 // build declaration
1088 default_dtor(symbol, dtor);
1089
1091 symbol,
1092 dtor, dtor.declarators()[0], components,
1093 ID_public, false, false, false);
1094 }
1095
1096 // set up virtual tables before doing the constructors
1097 if(symbol.type.id()==ID_struct)
1098 do_virtual_table(symbol);
1099
1100 if(!found_ctor && !cpp_is_pod(symbol.type))
1101 {
1102 // it's public!
1103 exprt cpp_public("cpp-public");
1104 body.add_to_operands(std::move(cpp_public));
1105
1106 // build declaration
1108 default_ctor(symbol.type.source_location(), symbol.base_name, ctor);
1109 body.add_to_operands(std::move(ctor));
1110 }
1111
1112 // Reset the access type
1113 access = type.default_access();
1114
1115 // All the data members are now known.
1116 // We now deal with the constructors that we are given.
1117 Forall_operands(it, body)
1118 {
1119 if(it->id()==ID_cpp_declaration)
1120 {
1121 cpp_declarationt &declaration=
1122 to_cpp_declaration(*it);
1123
1124 if(!declaration.is_constructor())
1125 continue;
1126
1127 for(auto &declarator : declaration.declarators())
1128 {
1129 #if 0
1131 declarator.name().get_base_name();
1132 #endif
1133
1134 if(declarator.value().is_not_nil()) // body?
1135 {
1136 if(declarator.find(ID_member_initializers).is_nil())
1138
1139 if(type.id() == ID_union)
1140 {
1142 {}, type.components(), declarator.member_initializers());
1143 }
1144 else
1145 {
1147 to_struct_type(type).bases(),
1148 type.components(),
1149 declarator.member_initializers());
1150 }
1151
1153 type,
1154 declarator.member_initializers());
1155 }
1156
1157 // Finally, we typecheck the constructor with the
1158 // full member-initialization list
1159 // Shall all be false
1160 bool is_static=declaration.storage_spec().is_static();
1161 bool is_mutable=declaration.storage_spec().is_mutable();
1162 bool is_typedef=declaration.is_typedef();
1163
1165 symbol,
1166 declaration, declarator, components,
1167 access, is_static, is_typedef, is_mutable);
1168 }
1169 }
1170 else if(it->id()=="cpp-public")
1172 else if(it->id()=="cpp-private")
1174 else if(it->id()=="cpp-protected")
1176 else
1177 {
1178 }
1179 }
1180
1181 if(!cpp_is_pod(symbol.type))
1182 {
1183 // Add the default copy constructor
1185
1186 if(!find_cpctor(symbol))
1187 {
1188 // build declaration
1190 default_cpctor(symbol, cpctor);
1191 CHECK_RETURN(cpctor.declarators().size() == 1);
1192
1194 value.copy_to_operands(cpctor.declarators()[0].value());
1195 cpctor.declarators()[0].value()=value;
1196
1198 symbol,
1199 cpctor, cpctor.declarators()[0], components,
1200 ID_public, false, false, false);
1201 }
1202
1203 // Add the default assignment operator
1204 if(!find_assignop(symbol))
1205 {
1206 // build declaration
1208 default_assignop(symbol, assignop);
1209 CHECK_RETURN(assignop.declarators().size() == 1);
1210
1211 // The value will be typechecked only if the operator
1212 // is actually used
1213 cpp_declaratort declarator;
1214 assignop.declarators().push_back(declarator);
1215 assignop.declarators()[0].value() = exprt(ID_cpp_not_typechecked);
1216
1218 symbol,
1219 assignop, assignop.declarators()[0], components,
1220 ID_public, false, false, false);
1221 }
1222 }
1223
1224 // clean up!
1225 symbol.type.remove(ID_body);
1226}
1227
1230 const code_typet &type,
1231 exprt &value)
1232{
1233 // see if we have initializers
1234 if(!initializers.get_sub().empty())
1235 {
1236 const source_locationt &location=
1237 static_cast<const source_locationt &>(
1239
1240 if(type.return_type().id() != ID_constructor)
1241 {
1242 error().source_location=location;
1243 error() << "only constructors are allowed to "
1244 << "have member initializers" << eom;
1245 throw 0;
1246 }
1247
1248 if(value.is_nil())
1249 {
1250 error().source_location=location;
1251 error() << "only constructors with body are allowed to "
1252 << "have member initializers" << eom;
1253 throw 0;
1254 }
1255
1256 if(to_code(value).get_statement() != ID_block)
1257 value = code_blockt{{to_code(value)}};
1258
1259 exprt::operandst::iterator o_it=value.operands().begin();
1260 for(const auto &initializer : initializers.get_sub())
1261 {
1262 o_it =
1263 value.operands().insert(o_it, static_cast<const exprt &>(initializer));
1264 o_it++;
1265 }
1266 }
1267}
1268
1270 const symbolt &compound_symbol,
1273 const typet &method_qualifier,
1274 exprt &value)
1275{
1276 code_typet &type = to_code_type(component.type());
1277
1278 if(component.get_bool(ID_is_static))
1279 {
1280 if(!method_qualifier.id().empty())
1281 {
1282 error().source_location=component.source_location();
1283 error() << "method is static -- no qualifiers allowed" << eom;
1284 throw 0;
1285 }
1286 }
1287 else
1288 {
1289 add_this_to_method_type(compound_symbol, type, method_qualifier);
1290 }
1291
1292 if(value.id() == ID_cpp_not_typechecked && value.has_operands())
1293 {
1295 initializers, type, to_multi_ary_expr(value).op0());
1296 }
1297 else
1299
1300 irep_idt f_id=
1302
1303 const irep_idt identifier=
1305 id2string(component.get_base_name())+
1306 id2string(f_id);
1307
1308 component.set_name(identifier);
1309 component.set(ID_prefix, id2string(identifier) + "::");
1310
1311 if(value.is_not_nil())
1312 to_code_type(type).set_inlined(true);
1313
1314 symbolt symbol{identifier, type, compound_symbol.mode};
1315 symbol.base_name=component.get_base_name();
1316 symbol.value.swap(value);
1317 symbol.module=module;
1318 symbol.location=component.source_location();
1319
1320 // move early, it must be visible before doing any value
1321 symbolt *new_symbol;
1322
1323 const bool symbol_exists = symbol_table.move(symbol, new_symbol);
1324 if(symbol_exists && new_symbol->is_weak)
1325 {
1326 // there might have been an earlier friend declaration
1327 *new_symbol = std::move(symbol);
1328 }
1329 else if(symbol_exists)
1330 {
1331 error().source_location=symbol.location;
1332 error() << "failed to insert new method symbol: " << symbol.name << '\n'
1333 << "name of previous symbol: " << new_symbol->name << '\n'
1334 << "location of previous symbol: " << new_symbol->location << eom;
1335
1336 throw 0;
1337 }
1338
1339 // Is this in a class template?
1340 // If so, we defer typechecking until used.
1342 deferred_typechecking.insert(new_symbol->name);
1343 else // remember for later typechecking of body
1344 add_method_body(new_symbol);
1345}
1346
1348 const symbolt &compound_symbol,
1349 code_typet &type,
1350 const typet &method_qualifier)
1351{
1352 typet subtype;
1353
1354 if(compound_symbol.type.id() == ID_union)
1355 subtype = union_tag_typet(compound_symbol.name);
1356 else
1357 subtype = struct_tag_typet(compound_symbol.name);
1358
1359 if(has_const(method_qualifier))
1360 subtype.set(ID_C_constant, true);
1361
1362 if(has_volatile(method_qualifier))
1363 subtype.set(ID_C_volatile, true);
1364
1366 parameter.set_identifier(ID_this);
1367 parameter.set_base_name(ID_this);
1368 parameter.set_this();
1371
1372 code_typet::parameterst &parameters = type.parameters();
1373 parameters.insert(parameters.begin(), parameter);
1374}
1375
1378{
1381
1383 struct_union_type.components();
1384
1385 // do scoping -- the members of the struct/union
1386 // should be visible in the containing struct/union,
1387 // and that recursively!
1388
1389 for(const auto &comp : struct_union_components)
1390 {
1391 if(comp.type().id()==ID_code)
1392 {
1393 error().source_location=struct_union_symbol.type.source_location();
1394 error() << "anonymous struct/union member '"
1395 << struct_union_symbol.base_name
1396 << "' shall not have function members" << eom;
1397 throw 0;
1398 }
1399
1400 if(comp.get_anonymous())
1401 {
1402 const symbolt &symbol=lookup(comp.type().get(ID_identifier));
1403 // recursive call
1405 }
1406 else
1407 {
1408 const irep_idt &base_name=comp.get_base_name();
1409
1410 if(cpp_scopes.current_scope().contains(base_name))
1411 {
1412 error().source_location=comp.source_location();
1413 error() << "'" << base_name << "' already in scope" << eom;
1414 throw 0;
1415 }
1416
1417 cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
1419 id.identifier=comp.get_name();
1420 id.class_identifier=struct_union_symbol.name;
1421 id.is_member=true;
1422 }
1423 }
1424}
1425
1427 const cpp_declarationt &declaration,
1428 const irep_idt &access,
1429 struct_typet::componentst &components)
1430{
1431 const struct_union_typet &final_type =
1432 declaration.type().id() == ID_struct_tag
1433 ? static_cast<const struct_union_typet &>(
1434 follow_tag(to_struct_tag_type(declaration.type())))
1435 : static_cast<const struct_union_typet &>(
1436 follow_tag(to_union_tag_type(declaration.type())));
1439
1440 if(declaration.storage_spec().is_static() ||
1441 declaration.storage_spec().is_mutable())
1442 {
1443 error().source_location=struct_union_symbol.type.source_location();
1444 error() << "storage class is not allowed here" << eom;
1445 throw 0;
1446 }
1447
1449 {
1450 error().source_location=struct_union_symbol.type.source_location();
1451 error() << "anonymous struct/union member is not POD" << eom;
1452 throw 0;
1453 }
1454
1455 // produce an anonymous member
1456 irep_idt base_name="#anon_member"+std::to_string(components.size());
1457
1458 irep_idt identifier=
1460 base_name.c_str();
1461
1462 typet compound_type;
1463
1464 if(struct_union_symbol.type.id() == ID_union)
1465 compound_type = union_tag_typet(struct_union_symbol.name);
1466 else
1467 compound_type = struct_tag_typet(struct_union_symbol.name);
1468
1469 struct_typet::componentt component(identifier, compound_type);
1470 component.set_access(access);
1471 component.set_base_name(base_name);
1472 component.set_pretty_name(base_name);
1473 component.set_anonymous(true);
1474 component.add_source_location()=declaration.source_location();
1475
1476 components.push_back(component);
1477
1479
1481
1482 struct_union_symbol.type.set(ID_C_unnamed_object, base_name);
1483}
1484
1486 const source_locationt &source_location,
1487 const exprt &object,
1488 const irep_idt &component_name,
1489 exprt &member)
1490{
1492 object.type().id() == ID_struct_tag || object.type().id() == ID_union_tag);
1493
1494 struct_union_typet final_type =
1495 object.type().id() == ID_struct_tag
1496 ? static_cast<const struct_union_typet &>(
1497 follow_tag(to_struct_tag_type(object.type())))
1498 : static_cast<const struct_union_typet &>(
1499 follow_tag(to_union_tag_type(object.type())));
1500
1501 const struct_union_typet::componentst &components=
1502 final_type.components();
1503
1504 for(const auto &component : components)
1505 {
1506 member_exprt tmp(object, component.get_name(), component.type());
1507 tmp.add_source_location()=source_location;
1508
1509 if(component.get_name()==component_name)
1510 {
1511 member.swap(tmp);
1512
1513 bool not_ok=check_component_access(component, final_type);
1514 if(not_ok)
1515 {
1517 {
1518 member.set(ID_C_not_accessible, true);
1519 member.set(ID_C_access, component.get(ID_access));
1520 }
1521 else
1522 {
1523 error().source_location=source_location;
1524 error() << "member '" << component_name << "' is not accessible ("
1525 << component.get(ID_access) << ")" << eom;
1526 throw 0;
1527 }
1528 }
1529
1530 if(object.get_bool(ID_C_lvalue))
1531 member.set(ID_C_lvalue, true);
1532
1533 if(
1534 object.type().get_bool(ID_C_constant) &&
1535 !component.get_bool(ID_is_mutable))
1536 {
1537 member.type().set(ID_C_constant, true);
1538 }
1539
1540 member.add_source_location()=source_location;
1541
1542 return true; // component found
1543 }
1544 else if(
1545 (component.type().id() == ID_struct_tag &&
1547 .find(ID_C_unnamed_object)
1548 .is_not_nil()) ||
1549 (component.type().id() == ID_union_tag &&
1551 .find(ID_C_unnamed_object)
1552 .is_not_nil()) ||
1553 component.type().find(ID_C_unnamed_object).is_not_nil())
1554 {
1555 // could be anonymous union or struct
1556
1557 if(
1558 component.type().id() == ID_union_tag ||
1559 component.type().id() == ID_struct_tag)
1560 {
1561 // recursive call!
1562 if(get_component(source_location, tmp, component_name, member))
1563 {
1564 if(check_component_access(component, final_type))
1565 {
1566 error().source_location=source_location;
1567 error() << "member '" << component_name << "' is not accessible"
1568 << eom;
1569 throw 0;
1570 }
1571
1572 if(object.get_bool(ID_C_lvalue))
1573 member.set(ID_C_lvalue, true);
1574
1575 if(
1576 object.get_bool(ID_C_constant) &&
1577 !component.get_bool(ID_is_mutable))
1578 {
1579 member.type().set(ID_C_constant, true);
1580 }
1581
1582 member.add_source_location()=source_location;
1583 return true; // component found
1584 }
1585 }
1586 }
1587 }
1588
1589 return false; // component not found
1590}
1591
1595{
1596 const irep_idt &access=component.get(ID_access);
1597
1598 if(access == ID_noaccess)
1599 return true; // not ok
1600
1601 if(access==ID_public)
1602 return false; // ok
1603
1605
1608
1610 !(pscope->is_root_scope());
1611 pscope = &(pscope->get_parent()))
1612 {
1613 if(pscope->is_class())
1614 {
1615 if(pscope->identifier==struct_identifier)
1616 return false; // ok
1617
1619 to_struct_type(lookup(pscope->identifier).type);
1620
1623 return false; // ok
1624
1625 else break;
1626 }
1627 }
1628
1629 // check friendship
1630 const irept::subt &friends = struct_union_type.find(ID_C_friends).get_sub();
1631
1632 for(const auto &friend_symb : friends)
1633 {
1634 const cpp_scopet &friend_scope =
1636
1638 !(pscope->is_root_scope());
1639 pscope = &(pscope->get_parent()))
1640 {
1641 if(friend_scope.identifier==pscope->identifier)
1642 return false; // ok
1643
1644 if(pscope->is_class())
1645 break;
1646 }
1647 }
1648
1649 return true; // not ok
1650}
1651
1653 const struct_typet &type,
1654 std::set<irep_idt> &set_bases) const
1655{
1656 for(const auto &b : type.bases())
1657 {
1658 DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
1659
1660 const struct_typet &base = to_struct_type(lookup(b.type()).type);
1661
1662 set_bases.insert(base.get(ID_name));
1663 get_bases(base, set_bases);
1664 }
1665}
1666
1668 const struct_typet &type,
1669 std::list<irep_idt> &vbases) const
1670{
1671 if(std::find(vbases.begin(), vbases.end(), type.get(ID_name))!=vbases.end())
1672 return;
1673
1674 for(const auto &b : type.bases())
1675 {
1676 DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
1677
1678 const struct_typet &base = to_struct_type(lookup(b.type()).type);
1679
1680 if(b.get_bool(ID_virtual))
1681 vbases.push_back(base.get(ID_name));
1682
1684 }
1685}
1686
1688 const struct_typet &from,
1689 const struct_typet &to) const
1690{
1691 if(from.get(ID_name)==to.get(ID_name))
1692 return true;
1693
1694 std::set<irep_idt> bases;
1695
1696 get_bases(from, bases);
1697
1698 return bases.find(to.get(ID_name))!=bases.end();
1699}
1700
1702 exprt &expr,
1703 const pointer_typet &dest_type)
1704{
1705 typet src_type=expr.type();
1706
1708
1709 const struct_typet &src_struct =
1711
1712 const struct_typet &dest_struct =
1714
1718
1719 expr = typecast_exprt(expr, dest_type);
1720}
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Arrays with given size.
Definition std_types.h:807
symbol_table_baset & symbol_table
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
Definition std_code.h:130
codet representation of an expression statement.
Definition std_code.h:1394
codet representation of a "return from a function" statement.
Definition std_code.h:893
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
const declaratorst & declarators() const
bool is_destructor() const
const cpp_member_spect & member_spec() const
const cpp_storage_spect & storage_spec() const
bool is_template() const
bool is_constructor() const
bool is_typedef() const
irept & member_initializers()
typet merge_type(const typet &declaration_type) const
cpp_namet & name()
irep_idt identifier
Definition cpp_id.h:72
std::string prefix
Definition cpp_id.h:79
id_classt id_class
Definition cpp_id.h:45
bool is_template_scope() const
Definition cpp_id.h:67
std::string suffix
Definition cpp_id.h:79
const source_locationt & source_location() const
Definition cpp_name.h:73
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
id_mapt id_map
Definition cpp_scopes.h:68
cpp_scopet & get_global_scope()
Definition cpp_scopes.h:115
cpp_scopet & get_scope(const irep_idt &identifier)
Definition cpp_scopes.h:80
cpp_scopet & set_scope(const irep_idt &identifier)
Definition cpp_scopes.h:87
void go_to_global_scope()
Definition cpp_scopes.h:110
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
cpp_scopet & get_parent() const
Definition cpp_scope.h:88
cpp_idt & insert(const irep_idt &_base_name)
Definition cpp_scope.h:52
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition cpp_scope.h:32
bool contains(const irep_idt &base_name_to_lookup)
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void typecheck_compound_body(symbolt &symbol)
void do_virtual_table(const symbolt &symbol)
void put_compound_into_scope(const struct_union_typet::componentt &component)
void typecheck_type(typet &) override
void convert_anon_struct_union_member(const cpp_declarationt &declaration, const irep_idt &access, struct_typet::componentst &components)
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
static bool has_const(const typet &type)
dynamic_initializationst dynamic_initializations
void convert_template_declaration(cpp_declarationt &declaration)
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
unsigned anon_counter
bool check_component_access(const struct_union_typet::componentt &component, const struct_union_typet &struct_union_type)
void typecheck_member_function(const symbolt &compound_symbol, struct_typet::componentt &component, irept &initializers, const typet &method_qualifier, exprt &value)
bool cpp_is_pod(const typet &type) const
void check_fixed_size_array(typet &type)
check that an array has fixed size
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool find_assignop(const symbolt &symbol) const
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
void typecheck_compound_type(struct_union_typet &) override
void add_anonymous_members_to_scope(const symbolt &struct_union_symbol)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
std::unordered_set< irep_idt > deferred_typechecking
void add_method_body(symbolt *_method_symbol)
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_compound_bases(struct_typet &type)
void elaborate_class_template(const typet &type)
elaborate class template instances
static bool has_auto(const typet &type)
static bool has_volatile(const typet &type)
irep_idt function_identifier(const typet &type)
for function overloading
void typecheck_friend_declaration(symbolt &symbol, cpp_declarationt &cpp_declaration)
void add_this_to_method_type(const symbolt &compound_symbol, code_typet &method_type, const typet &method_qualifier)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
void convert_parameter(const irep_idt &current_mode, code_typet::parametert &parameter)
bool find_cpctor(const symbolt &symbol) const
void move_member_initializers(irept &initializers, const code_typet &type, exprt &value)
bool disable_access_control
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
cpp_scopest cpp_scopes
void get_bases(const struct_typet &type, std::set< irep_idt > &set_bases) const
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
const char * c_str() const
Definition dstring.h:116
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:163
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
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
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
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
subt & get_sub()
Definition irep.h:448
void make_nil()
Definition irep.h:446
void move_to_sub(irept &irep)
Definition irep.cpp:35
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
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Extract member of struct or union.
Definition std_expr.h:2971
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
const basest & bases() const
Get the collection of base classes/structs.
Definition std_types.h:262
const irep_idt & get_base_name() const
Definition std_types.h:89
const irep_idt & get_name() const
Definition std_types.h:79
Base type for structs and unions.
Definition std_types.h:62
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition std_types.h:179
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
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:150
const irep_idt & get_identifier() const
Definition std_expr.h:160
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:78
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
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
irep_idt mode
Language mode.
Definition symbol.h:49
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
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
typet & add_subtype()
Definition type.h:53
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition cpp_name.h:148
std::string cpp_type2name(const typet &type)
C++ Language Module.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
static bool symbol_exists(const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available)
Returns true iff the given symbol exists and satisfies requirements.
#define Forall_operands(it, expr)
Definition expr.h:27
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static bool is_constructor(const irep_idt &method_name)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#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 codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Pre-defined types.
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 bool failed(bool error_indicator)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252
dstringt irep_idt