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