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