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