cprover
Loading...
Searching...
No Matches
cpp_typecheck_constructor.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
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/pointer_expr.h>
19#include <util/std_code.h>
20
26static void copy_parent(
27 const source_locationt &source_location,
28 const irep_idt &parent_base_name,
29 const irep_idt &arg_name,
30 exprt &block)
31{
32 exprt op0(
33 "explicit-typecast",
34 pointer_type(cpp_namet(parent_base_name, source_location).as_type()));
35 op0.copy_to_operands(exprt("cpp-this"));
36 op0.add_source_location()=source_location;
37
38 exprt op1(
39 "explicit-typecast",
40 pointer_type(cpp_namet(parent_base_name, source_location).as_type()));
41 op1.type().set(ID_C_reference, true);
42 op1.type().subtype().set(ID_C_constant, true);
43 op1.get_sub().push_back(cpp_namet(arg_name, source_location));
44 op1.add_source_location()=source_location;
45
47 code.add_source_location() = source_location;
48
49 block.operands().push_back(code);
50}
51
57static void copy_member(
58 const source_locationt &source_location,
59 const irep_idt &member_base_name,
60 const irep_idt &arg_name,
61 exprt &block)
62{
63 cpp_namet op0(member_base_name, source_location);
64
65 exprt op1(ID_member);
66 op1.add(ID_component_cpp_name, cpp_namet(member_base_name, source_location));
67 op1.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());
68 op1.add_source_location()=source_location;
69
70 side_effect_expr_assignt assign(op0.as_expr(), op1, typet(), source_location);
71 assign.lhs().add_source_location() = source_location;
72
73 code_expressiont code(assign);
74 code.add_source_location() = source_location;
75
76 block.operands().push_back(code);
77}
78
85static void copy_array(
86 const source_locationt &source_location,
87 const irep_idt &member_base_name,
88 mp_integer i,
89 const irep_idt &arg_name,
90 exprt &block)
91{
92 // Build the index expression
93 const exprt constant = from_integer(i, c_index_type());
94
95 const cpp_namet array(member_base_name, source_location);
96
97 exprt member(ID_member);
98 member.add(
99 ID_component_cpp_name, cpp_namet(member_base_name, source_location));
100 member.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());
101
103 index_exprt(array.as_expr(), constant),
104 index_exprt(member, constant),
105 typet(),
106 source_location);
107
108 assign.lhs().add_source_location() = source_location;
109 assign.rhs().add_source_location() = source_location;
110
111 code_expressiont code(assign);
112 code.add_source_location() = source_location;
113
114 block.operands().push_back(code);
115}
116
119 const source_locationt &source_location,
120 const irep_idt &base_name,
121 cpp_declarationt &ctor) const
122{
123 cpp_declaratort decl;
124 decl.name() = cpp_namet(base_name, source_location);
125 decl.type()=typet(ID_function_type);
126 decl.type().subtype().make_nil();
127 decl.add_source_location()=source_location;
128
129 decl.value() = code_blockt();
130 decl.add(ID_cv).make_nil();
131 decl.add(ID_throw_decl).make_nil();
132
133 ctor.type().id(ID_constructor);
134 ctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
135 ctor.add_to_operands(std::move(decl));
136 ctor.add_source_location()=source_location;
137}
138
141 const symbolt &symbol,
142 cpp_declarationt &cpctor) const
143{
144 source_locationt source_location=symbol.type.source_location();
145
146 source_location.set_function(
147 id2string(symbol.base_name)+
148 "::"+id2string(symbol.base_name)+
149 "(const "+id2string(symbol.base_name)+" &)");
150
151 // Produce default constructor first
152 default_ctor(source_location, symbol.base_name, cpctor);
153 cpp_declaratort &decl0=cpctor.declarators()[0];
154
155 std::string param_identifier("ref");
156
157 // Compound name
158 const cpp_namet cppcomp(symbol.base_name, source_location);
159
160 // Parameter name
161 const cpp_namet cpp_parameter(param_identifier, source_location);
162
163 // Parameter declarator
164 cpp_declaratort parameter_tor;
165 parameter_tor.add(ID_value).make_nil();
166 parameter_tor.set(ID_name, cpp_parameter);
167 parameter_tor.type() = reference_type(uninitialized_typet{});
168 parameter_tor.add_source_location()=source_location;
169
170 // Parameter declaration
171 cpp_declarationt parameter_decl;
172 parameter_decl.set(ID_type, ID_merged_type);
173 auto &sub = to_type_with_subtypes(parameter_decl.type()).subtypes();
174 sub.push_back(cppcomp.as_type());
175 irept constnd(ID_const);
176 sub.push_back(static_cast<const typet &>(constnd));
177 parameter_decl.add_to_operands(std::move(parameter_tor));
178 parameter_decl.add_source_location()=source_location;
179
180 // Add parameter to function type
181 decl0.add(ID_type).add(ID_parameters).get_sub().push_back(parameter_decl);
182 decl0.add_source_location()=source_location;
183
184 irept &initializers=decl0.add(ID_member_initializers);
185 initializers.id(ID_member_initializers);
186
187 cpp_declaratort &declarator =
188 static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());
189 exprt &block=declarator.value();
190
191 // First, we need to call the parent copy constructors
192 for(const auto &b : to_struct_type(symbol.type).bases())
193 {
194 DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
195
196 const symbolt &parsymb = lookup(b.type());
197
198 if(cpp_is_pod(parsymb.type))
199 copy_parent(source_location, parsymb.base_name, param_identifier, block);
200 else
201 {
202 irep_idt ctor_name=parsymb.base_name;
203
204 // Call the parent default copy constructor
205 const cpp_namet cppname(ctor_name, source_location);
206
207 codet mem_init(ID_member_initializer);
208 mem_init.add_source_location()=source_location;
209 mem_init.set(ID_member, cppname);
210 mem_init.copy_to_operands(cpp_parameter.as_expr());
211 initializers.move_to_sub(mem_init);
212 }
213 }
214
215 // Then, we add the member initializers
216 const struct_typet::componentst &components=
218
219 for(const auto &mem_c : components)
220 {
221 // Take care of virtual tables
222 if(mem_c.get_bool(ID_is_vtptr))
223 {
224 const cpp_namet cppname(mem_c.get_base_name(), source_location);
225
226 const symbolt &virtual_table_symbol_type =
227 lookup(to_pointer_type(mem_c.type()).base_type().get(ID_identifier));
228
229 const symbolt &virtual_table_symbol_var = lookup(
230 id2string(virtual_table_symbol_type.name) + "@" +
231 id2string(symbol.name));
232
233 exprt var=virtual_table_symbol_var.symbol_expr();
234 address_of_exprt address(var);
235 assert(address.type() == mem_c.type());
236
238
239 exprt ptrmember(ID_ptrmember);
240 ptrmember.set(ID_component_name, mem_c.get_name());
241 ptrmember.operands().push_back(exprt("cpp-this"));
242
243 code_frontend_assignt assign(ptrmember, address);
244 initializers.move_to_sub(assign);
245 continue;
246 }
247
248 if(
249 mem_c.get_bool(ID_from_base) || mem_c.get_bool(ID_is_type) ||
250 mem_c.get_bool(ID_is_static) || mem_c.type().id() == ID_code)
251 {
252 continue;
253 }
254
255 const irep_idt &mem_name = mem_c.get_base_name();
256
257 const cpp_namet cppname(mem_name, source_location);
258
259 codet mem_init(ID_member_initializer);
260 mem_init.set(ID_member, cppname);
261 mem_init.add_source_location()=source_location;
262
263 exprt memberexpr(ID_member);
264 memberexpr.set(ID_component_cpp_name, cppname);
265 memberexpr.copy_to_operands(cpp_parameter.as_expr());
266 memberexpr.add_source_location()=source_location;
267
268 if(mem_c.type().id() == ID_array)
269 memberexpr.set(ID_C_array_ini, true);
270
271 mem_init.add_to_operands(std::move(memberexpr));
272 initializers.move_to_sub(mem_init);
273 }
274}
275
278 const symbolt &symbol,
279 cpp_declarationt &cpctor)
280{
281 source_locationt source_location=symbol.type.source_location();
282
283 source_location.set_function(
284 id2string(symbol.base_name)
285 + "& "+
286 id2string(symbol.base_name)+
287 "::operator=( const "+id2string(symbol.base_name)+"&)");
288
289 std::string arg_name("ref");
290
291 cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
292 cpctor.type().id(ID_struct_tag);
293 cpctor.type().add(ID_identifier).id(symbol.name);
294 cpctor.operands().push_back(exprt(ID_cpp_declarator));
295 cpctor.add_source_location()=source_location;
296
297 cpp_declaratort &declarator =
298 static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());
299 declarator.add_source_location()=source_location;
300
301 cpp_namet &declarator_name=declarator.name();
302 typet &declarator_type=declarator.type();
303
304 declarator_type.add_source_location()=source_location;
305
306 declarator_name.id(ID_cpp_name);
307 declarator_name.get_sub().push_back(irept(ID_operator));
308 declarator_name.get_sub().push_back(irept("="));
309
310 declarator_type.id(ID_function_type);
311 declarator_type.subtype() = reference_type(uninitialized_typet{});
312 declarator_type.subtype().add(ID_C_qualifier).make_nil();
313
314 exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));
315 args.add_source_location()=source_location;
316
317 args.get_sub().push_back(irept(ID_cpp_declaration));
318
319 cpp_declarationt &args_decl=
320 static_cast<cpp_declarationt&>(args.get_sub().back());
321
322 auto &args_decl_type_sub = to_type_with_subtypes(args_decl.type()).subtypes();
323
324 args_decl.type().id(ID_merged_type);
325 args_decl_type_sub.push_back(
326 cpp_namet(symbol.base_name, source_location).as_type());
327
328 args_decl_type_sub.push_back(typet(ID_const));
329 args_decl.operands().push_back(exprt(ID_cpp_declarator));
330 args_decl.add_source_location()=source_location;
331
332 cpp_declaratort &args_decl_declor=
333 static_cast<cpp_declaratort&>(args_decl.operands().back());
334
335 args_decl_declor.name() = cpp_namet(arg_name, source_location);
336 args_decl_declor.add_source_location()=source_location;
337
338 args_decl_declor.type() = pointer_type(uninitialized_typet{});
339 args_decl_declor.type().set(ID_C_reference, true);
340 args_decl_declor.value().make_nil();
341}
342
345 const symbolt &symbol,
346 cpp_declaratort &declarator)
347{
348 // save source location
349 source_locationt source_location=declarator.source_location();
350 declarator.make_nil();
351
352 code_blockt block;
353
354 std::string arg_name("ref");
355
356 // First, we copy the parents
357 for(const auto &b : to_struct_type(symbol.type).bases())
358 {
359 DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
360
361 const symbolt &symb = lookup(b.type());
362
363 copy_parent(source_location, symb.base_name, arg_name, block);
364 }
365
366 // Then, we copy the members
367 for(const auto &c : to_struct_type(symbol.type).components())
368 {
369 if(
370 c.get_bool(ID_from_base) || c.get_bool(ID_is_type) ||
371 c.get_bool(ID_is_static) || c.get_bool(ID_is_vtptr) ||
372 c.type().id() == ID_code)
373 {
374 continue;
375 }
376
377 const irep_idt &mem_name = c.get_base_name();
378
379 if(c.type().id() == ID_array)
380 {
381 const exprt &size_expr = to_array_type(c.type()).size();
382
383 if(size_expr.id()==ID_infinity)
384 {
385 // error().source_location=object);
386 // err << "cannot copy array of infinite size\n";
387 // throw 0;
388 continue;
389 }
390
391 const auto size = numeric_cast<mp_integer>(size_expr);
392 CHECK_RETURN(!size.has_value());
393 CHECK_RETURN(*size >= 0);
394
395 for(mp_integer i = 0; i < *size; ++i)
396 copy_array(source_location, mem_name, i, arg_name, block);
397 }
398 else
399 copy_member(source_location, mem_name, arg_name, block);
400 }
401
402 // Finally we add the return statement
403 block.add(
405
406 declarator.value() = std::move(block);
407 declarator.value().add_source_location() = source_location;
408}
409
418 const struct_typet::basest &bases,
419 const struct_typet::componentst &components,
420 const irept &initializers)
421{
422 assert(initializers.id()==ID_member_initializers);
423
424 for(const auto &initializer : initializers.get_sub())
425 {
426 assert(initializer.is_not_nil());
427
428 const cpp_namet &member_name=
429 to_cpp_name(initializer.find(ID_member));
430
431 bool has_template_args=member_name.has_template_args();
432
433 if(has_template_args)
434 {
435 // it has to be a parent constructor
436 typet member_type=(typet&) initializer.find(ID_member);
437 typecheck_type(member_type);
438
439 // check for a direct parent
440 bool ok=false;
441 for(const auto &b : bases)
442 {
443 if(
444 to_struct_tag_type(member_type).get_identifier() ==
446 {
447 ok=true;
448 break;
449 }
450 }
451
452 if(!ok)
453 {
454 error().source_location=member_name.source_location();
455 error() << "invalid initializer '" << member_name.to_string() << "'"
456 << eom;
457 throw 0;
458 }
459 return;
460 }
461
462 irep_idt base_name=member_name.get_base_name();
463 bool ok=false;
464
465 for(const auto &c : components)
466 {
467 if(c.get_base_name() != base_name)
468 continue;
469
470 // Data member
471 if(
472 !c.get_bool(ID_from_base) && !c.get_bool(ID_is_static) &&
473 c.type().id() != ID_code)
474 {
475 ok=true;
476 break;
477 }
478
479 // Maybe it is a parent constructor?
480 if(c.get_bool(ID_is_type))
481 {
482 if(c.type().id() != ID_struct_tag)
483 continue;
484
485 const symbolt &symb =
487 if(symb.type.id()!=ID_struct)
488 break;
489
490 // check for a direct parent
491 for(const auto &b : bases)
492 {
493 if(symb.name == to_struct_tag_type(b.type()).get_identifier())
494 {
495 ok=true;
496 break;
497 }
498 }
499 continue;
500 }
501
502 // Parent constructor
503 if(
504 c.get_bool(ID_from_base) && !c.get_bool(ID_is_type) &&
505 !c.get_bool(ID_is_static) && c.type().id() == ID_code &&
506 to_code_type(c.type()).return_type().id() == ID_constructor)
507 {
508 typet member_type=(typet&) initializer.find(ID_member);
509 typecheck_type(member_type);
510
511 // check for a direct parent
512 for(const auto &b : bases)
513 {
514 if(
515 member_type.get(ID_identifier) ==
517 {
518 ok=true;
519 break;
520 }
521 }
522 break;
523 }
524 }
525
526 if(!ok)
527 {
528 error().source_location=member_name.source_location();
529 error() << "invalid initializer '" << base_name << "'" << eom;
530 throw 0;
531 }
532 }
533}
534
543 const struct_union_typet &struct_union_type,
544 irept &initializers)
545{
546 const struct_union_typet::componentst &components=
547 struct_union_type.components();
548
549 assert(initializers.id()==ID_member_initializers);
550
551 irept final_initializers(ID_member_initializers);
552
553 if(struct_union_type.id()==ID_struct)
554 {
555 // First, if we are the most-derived object, then
556 // we need to construct the virtual bases
557 std::list<irep_idt> vbases;
558 get_virtual_bases(to_struct_type(struct_union_type), vbases);
559
560 if(!vbases.empty())
561 {
562 code_blockt block;
563
564 while(!vbases.empty())
565 {
566 const symbolt &symb=lookup(vbases.front());
567 if(!cpp_is_pod(symb.type))
568 {
569 // default initializer
570 const cpp_namet cppname(symb.base_name);
571
572 codet mem_init(ID_member_initializer);
573 mem_init.set(ID_member, cppname);
574 block.move_to_sub(mem_init);
575 }
576 vbases.pop_front();
577 }
578
579 code_ifthenelset cond(
580 cpp_namet("@most_derived").as_expr(), std::move(block));
581 final_initializers.move_to_sub(cond);
582 }
583
584 // Subsequently, we need to call the non-POD parent constructors
585 for(const auto &b : to_struct_type(struct_union_type).bases())
586 {
587 DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
588
589 const symbolt &ctorsymb = lookup(b.type());
590
591 if(cpp_is_pod(ctorsymb.type))
592 continue;
593
594 irep_idt ctor_name=ctorsymb.base_name;
595
596 // Check if the initialization list of the constructor
597 // explicitly calls the parent constructor.
598 bool found=false;
599
600 for(irept initializer : initializers.get_sub())
601 {
602 const cpp_namet &member_name=
603 to_cpp_name(initializer.find(ID_member));
604
605 bool has_template_args=member_name.has_template_args();
606
607 if(!has_template_args)
608 {
609 irep_idt base_name=member_name.get_base_name();
610
611 // check if the initializer is a data
612 bool is_data=false;
613
614 for(const auto &c : components)
615 {
616 if(
617 c.get_base_name() == base_name && c.type().id() != ID_code &&
618 !c.get_bool(ID_is_type))
619 {
620 is_data=true;
621 break;
622 }
623 }
624
625 if(is_data)
626 continue;
627 }
628
629 typet member_type=
630 static_cast<const typet&>(initializer.find(ID_member));
631
632 typecheck_type(member_type);
633
634 if(member_type.id() != ID_struct_tag)
635 break;
636
637 if(
639 to_struct_tag_type(member_type).get_identifier())
640 {
641 final_initializers.move_to_sub(initializer);
642 found=true;
643 break;
644 }
645 }
646
647 // Call the parent default constructor
648 if(!found)
649 {
650 const cpp_namet cppname(ctor_name);
651
652 codet mem_init(ID_member_initializer);
653 mem_init.set(ID_member, cppname);
654 final_initializers.move_to_sub(mem_init);
655 }
656
657 if(b.get_bool(ID_virtual))
658 {
659 codet tmp(ID_member_initializer);
660 tmp.swap(final_initializers.get_sub().back());
661
662 code_ifthenelset cond(
663 cpp_namet("@most_derived").as_expr(), std::move(tmp));
664
665 final_initializers.get_sub().back().swap(cond);
666 }
667 }
668 }
669
670 // Then, we add the member initializers
671 for(const auto &c : components)
672 {
673 // Take care of virtual tables
674 if(c.get_bool(ID_is_vtptr))
675 {
676 const cpp_namet cppname(c.get_base_name(), c.source_location());
677
678 const symbolt &virtual_table_symbol_type =
679 lookup(to_pointer_type(c.type()).base_type().get(ID_identifier));
680
681 const symbolt &virtual_table_symbol_var =
682 lookup(id2string(virtual_table_symbol_type.name) + "@" +
683 id2string(struct_union_type.get(ID_name)));
684
685 exprt var=virtual_table_symbol_var.symbol_expr();
686 address_of_exprt address(var);
687 assert(address.type() == c.type());
688
690
691 exprt ptrmember(ID_ptrmember);
692 ptrmember.set(ID_component_name, c.get_name());
693 ptrmember.operands().push_back(exprt("cpp-this"));
694
695 code_frontend_assignt assign(ptrmember, address);
696 final_initializers.move_to_sub(assign);
697 continue;
698 }
699
700 if(
701 c.get_bool(ID_from_base) || c.type().id() == ID_code ||
702 c.get_bool(ID_is_type) || c.get_bool(ID_is_static))
703 {
704 continue;
705 }
706
707 const irep_idt &mem_name = c.get_base_name();
708
709 // Check if the initialization list of the constructor
710 // explicitly initializes the data member
711 bool found=false;
712 for(auto &initializer : initializers.get_sub())
713 {
714 if(initializer.get(ID_member)!=ID_cpp_name)
715 continue;
716 cpp_namet &member_name=(cpp_namet&) initializer.add(ID_member);
717
718 if(member_name.has_template_args())
719 continue; // base-type initializer
720
721 irep_idt base_name=member_name.get_base_name();
722
723 if(mem_name==base_name)
724 {
725 final_initializers.move_to_sub(initializer);
726 found=true;
727 break;
728 }
729 }
730
731 // If the data member is a reference, it must be explicitly
732 // initialized
733 if(
734 !found && c.type().id() == ID_pointer &&
735 c.type().get_bool(ID_C_reference))
736 {
737 error().source_location = c.source_location();
738 error() << "reference must be explicitly initialized" << eom;
739 throw 0;
740 }
741
742 // If the data member is not POD and is not explicitly initialized,
743 // then its default constructor is called.
744 if(!found && !cpp_is_pod(c.type()))
745 {
746 cpp_namet cppname(mem_name);
747
748 codet mem_init(ID_member_initializer);
749 mem_init.set(ID_member, cppname);
750 final_initializers.move_to_sub(mem_init);
751 }
752 }
753
754 initializers.swap(final_initializers);
755}
756
759bool cpp_typecheckt::find_cpctor(const symbolt &symbol) const
760{
761 for(const auto &component : to_struct_type(symbol.type).components())
762 {
763 // Skip non-ctor
764 if(component.type().id()!=ID_code ||
765 to_code_type(component.type()).return_type().id() !=ID_constructor)
766 continue;
767
768 // Skip inherited constructor
769 if(component.get_bool(ID_from_base))
770 continue;
771
772 const code_typet &code_type=to_code_type(component.type());
773
774 const code_typet::parameterst &parameters=code_type.parameters();
775
776 // First parameter is the 'this' pointer. Therefore, copy
777 // constructors have at least two parameters
778 if(parameters.size() < 2)
779 continue;
780
781 const code_typet::parametert &parameter1=parameters[1];
782
783 const typet &parameter1_type=parameter1.type();
784
785 if(!is_reference(parameter1_type))
786 continue;
787
788 if(
789 to_reference_type(parameter1_type).base_type().get(ID_identifier) !=
790 symbol.name)
791 {
792 continue;
793 }
794
795 bool defargs=true;
796 for(std::size_t i=2; i<parameters.size(); i++)
797 {
798 if(parameters[i].default_value().is_nil())
799 {
800 defargs=false;
801 break;
802 }
803 }
804
805 if(defargs)
806 return true;
807 }
808
809 return false;
810}
811
812bool cpp_typecheckt::find_assignop(const symbolt &symbol) const
813{
814 const struct_typet &struct_type=to_struct_type(symbol.type);
815 const struct_typet::componentst &components=struct_type.components();
816
817 for(const auto &component : components)
818 {
819 if(component.get_base_name() != "operator=")
820 continue;
821
822 if(component.get_bool(ID_is_static))
823 continue;
824
825 if(component.get_bool(ID_from_base))
826 continue;
827
828 const code_typet &code_type=to_code_type(component.type());
829
830 const code_typet::parameterst &args=code_type.parameters();
831
832 if(args.size()!=2)
833 continue;
834
835 const code_typet::parametert &arg1=args[1];
836
837 const typet &arg1_type=arg1.type();
838
839 if(!is_reference(arg1_type))
840 continue;
841
842 if(
843 to_reference_type(arg1_type).base_type().get(ID_identifier) !=
844 symbol.name)
845 continue;
846
847 return true;
848 }
849
850 return false;
851}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:258
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:361
static void make_already_typechecked(exprt &expr)
const exprt & size() const
Definition: std_types.h:790
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
codet representation of an expression statement.
Definition: std_code.h:1394
A codet representing an assignment in the program.
Definition: std_code.h:24
codet representation of an if-then-else statement.
Definition: std_code.h:460
codet representation of a "return from a function" statement.
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const declaratorst & declarators() const
cpp_namet & name()
const exprt & as_expr() const
Definition: cpp_name.h:137
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
bool has_template_args() const
Definition: cpp_name.h:124
std::string to_string() const
Definition: cpp_name.cpp:75
const source_locationt & source_location() const
Definition: cpp_name.h:73
const typet & as_type() const
Definition: cpp_name.h:142
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void typecheck_type(typet &) override
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool find_assignop(const symbolt &symbol) const
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
bool find_cpctor(const symbolt &symbol) const
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
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
Array index operator.
Definition: std_expr.h:1328
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
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 set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
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
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
exprt & op0()
Definition: std_expr.h:844
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1565
void set_function(const irep_idt &function)
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
std::vector< baset > basest
Definition: std_types.h:259
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
const irep_idt & get_identifier() const
Definition: std_types.h:410
subtypest & subtypes()
Definition: type.h:206
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
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
C++ Language Type Checking.
static void copy_array(const source_locationt &source_location, const irep_idt &member_base_name, mp_integer i, const irep_idt &arg_name, exprt &block)
Generate code to copy the member.
static void copy_member(const source_locationt &source_location, const irep_idt &member_base_name, const irep_idt &arg_name, exprt &block)
Generate code to copy the member.
static void copy_parent(const source_locationt &source_location, const irep_idt &parent_base_name, const irep_idt &arg_name, exprt &block)
Generate code to copy the parent.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:137
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:148
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
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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:221