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/std_code.h>
16 #include <util/std_expr.h>
17 
18 #include <util/c_types.h>
19 
20 #include "cpp_util.h"
21 
27 static void copy_parent(
28  const source_locationt &source_location,
29  const irep_idt &parent_base_name,
30  const irep_idt &arg_name,
31  exprt &block)
32 {
33  exprt op0(
34  "explicit-typecast",
35  pointer_type(cpp_namet(parent_base_name, source_location).as_type()));
36  op0.copy_to_operands(exprt("cpp-this"));
37  op0.add_source_location()=source_location;
38 
39  exprt op1(
40  "explicit-typecast",
41  pointer_type(cpp_namet(parent_base_name, source_location).as_type()));
42  op1.type().set(ID_C_reference, true);
43  op1.type().subtype().set(ID_C_constant, true);
44  op1.get_sub().push_back(cpp_namet(arg_name, source_location));
45  op1.add_source_location()=source_location;
46 
47  code_assignt code(dereference_exprt(op0), op1);
48  code.add_source_location() = source_location;
49 
50  block.operands().push_back(code);
51 }
52 
58 static void copy_member(
59  const source_locationt &source_location,
60  const irep_idt &member_base_name,
61  const irep_idt &arg_name,
62  exprt &block)
63 {
64  cpp_namet op0(member_base_name, source_location);
65 
66  exprt op1(ID_member);
67  op1.add(ID_component_cpp_name, cpp_namet(member_base_name, source_location));
68  op1.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());
69  op1.add_source_location()=source_location;
70 
71  side_effect_expr_assignt assign(op0.as_expr(), op1, typet(), source_location);
72  assign.lhs().add_source_location() = source_location;
73 
74  code_expressiont code(assign);
75  code.add_source_location() = source_location;
76 
77  block.operands().push_back(code);
78 }
79 
86 static void copy_array(
87  const source_locationt &source_location,
88  const irep_idt &member_base_name,
89  mp_integer i,
90  const irep_idt &arg_name,
91  exprt &block)
92 {
93  // Build the index expression
94  const exprt constant = from_integer(i, index_type());
95 
96  const cpp_namet array(member_base_name, source_location);
97 
98  exprt member(ID_member);
99  member.add(
100  ID_component_cpp_name, cpp_namet(member_base_name, source_location));
101  member.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());
102 
104  index_exprt(array.as_expr(), constant),
105  index_exprt(member, constant),
106  typet(),
107  source_location);
108 
109  assign.lhs().add_source_location() = source_location;
110  assign.rhs().add_source_location() = source_location;
111 
112  code_expressiont code(assign);
113  code.add_source_location() = source_location;
114 
115  block.operands().push_back(code);
116 }
117 
120  const source_locationt &source_location,
121  const irep_idt &base_name,
122  cpp_declarationt &ctor) const
123 {
124  cpp_declaratort decl;
125  decl.name() = cpp_namet(base_name, source_location);
126  decl.type()=typet(ID_function_type);
127  decl.type().subtype().make_nil();
128  decl.add_source_location()=source_location;
129 
130  decl.value() = code_blockt();
131  decl.add(ID_cv).make_nil();
132  decl.add(ID_throw_decl).make_nil();
133 
134  ctor.type().id(ID_constructor);
135  ctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
136  ctor.add_to_operands(std::move(decl));
137  ctor.add_source_location()=source_location;
138 }
139 
142  const symbolt &symbol,
143  cpp_declarationt &cpctor) const
144 {
145  source_locationt source_location=symbol.type.source_location();
146 
147  source_location.set_function(
148  id2string(symbol.base_name)+
149  "::"+id2string(symbol.base_name)+
150  "(const "+id2string(symbol.base_name)+" &)");
151 
152  // Produce default constructor first
153  default_ctor(source_location, symbol.base_name, cpctor);
154  cpp_declaratort &decl0=cpctor.declarators()[0];
155 
156  std::string param_identifier("ref");
157 
158  // Compound name
159  const cpp_namet cppcomp(symbol.base_name, source_location);
160 
161  // Parameter name
162  const cpp_namet cpp_parameter(param_identifier, source_location);
163 
164  // Parameter declarator
165  cpp_declaratort parameter_tor;
166  parameter_tor.add(ID_value).make_nil();
167  parameter_tor.set(ID_name, cpp_parameter);
168  parameter_tor.type() = reference_type(uninitialized_typet{});
169  parameter_tor.add_source_location()=source_location;
170 
171  // Parameter declaration
172  cpp_declarationt parameter_decl;
173  parameter_decl.set(ID_type, ID_merged_type);
174  auto &sub = to_type_with_subtypes(parameter_decl.type()).subtypes();
175  sub.push_back(cppcomp.as_type());
176  irept constnd(ID_const);
177  sub.push_back(static_cast<const typet &>(constnd));
178  parameter_decl.add_to_operands(std::move(parameter_tor));
179  parameter_decl.add_source_location()=source_location;
180 
181  // Add parameter to function type
182  decl0.add(ID_type).add(ID_parameters).get_sub().push_back(parameter_decl);
183  decl0.add_source_location()=source_location;
184 
185  irept &initializers=decl0.add(ID_member_initializers);
186  initializers.id(ID_member_initializers);
187 
188  cpp_declaratort &declarator =
189  static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());
190  exprt &block=declarator.value();
191 
192  // First, we need to call the parent copy constructors
193  for(const auto &b : to_struct_type(symbol.type).bases())
194  {
195  DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
196 
197  const symbolt &parsymb = lookup(b.type());
198 
199  if(cpp_is_pod(parsymb.type))
200  copy_parent(source_location, parsymb.base_name, param_identifier, block);
201  else
202  {
203  irep_idt ctor_name=parsymb.base_name;
204 
205  // Call the parent default copy constructor
206  const cpp_namet cppname(ctor_name, source_location);
207 
208  codet mem_init(ID_member_initializer);
209  mem_init.add_source_location()=source_location;
210  mem_init.set(ID_member, cppname);
211  mem_init.copy_to_operands(cpp_parameter.as_expr());
212  initializers.move_to_sub(mem_init);
213  }
214  }
215 
216  // Then, we add the member initializers
217  const struct_typet::componentst &components=
218  to_struct_type(symbol.type).components();
219 
220  for(const auto &mem_c : components)
221  {
222  // Take care of virtual tables
223  if(mem_c.get_bool(ID_is_vtptr))
224  {
225  const cpp_namet cppname(mem_c.get_base_name(), source_location);
226 
227  const symbolt &virtual_table_symbol_type =
228  lookup(mem_c.type().subtype().get(ID_identifier));
229 
230  const symbolt &virtual_table_symbol_var = lookup(
231  id2string(virtual_table_symbol_type.name) + "@" +
232  id2string(symbol.name));
233 
234  exprt var=virtual_table_symbol_var.symbol_expr();
235  address_of_exprt address(var);
236  assert(address.type() == mem_c.type());
237 
239 
240  exprt ptrmember(ID_ptrmember);
241  ptrmember.set(ID_component_name, mem_c.get_name());
242  ptrmember.operands().push_back(exprt("cpp-this"));
243 
244  code_assignt assign(ptrmember, address);
245  initializers.move_to_sub(assign);
246  continue;
247  }
248 
249  if(
250  mem_c.get_bool(ID_from_base) || mem_c.get_bool(ID_is_type) ||
251  mem_c.get_bool(ID_is_static) || mem_c.type().id() == ID_code)
252  {
253  continue;
254  }
255 
256  const irep_idt &mem_name = mem_c.get_base_name();
257 
258  const cpp_namet cppname(mem_name, source_location);
259 
260  codet mem_init(ID_member_initializer);
261  mem_init.set(ID_member, cppname);
262  mem_init.add_source_location()=source_location;
263 
264  exprt memberexpr(ID_member);
265  memberexpr.set(ID_component_cpp_name, cppname);
266  memberexpr.copy_to_operands(cpp_parameter.as_expr());
267  memberexpr.add_source_location()=source_location;
268 
269  if(mem_c.type().id() == ID_array)
270  memberexpr.set(ID_C_array_ini, true);
271 
272  mem_init.add_to_operands(std::move(memberexpr));
273  initializers.move_to_sub(mem_init);
274  }
275 }
276 
279  const symbolt &symbol,
280  cpp_declarationt &cpctor)
281 {
282  source_locationt source_location=symbol.type.source_location();
283 
284  source_location.set_function(
285  id2string(symbol.base_name)
286  + "& "+
287  id2string(symbol.base_name)+
288  "::operator=( const "+id2string(symbol.base_name)+"&)");
289 
290  std::string arg_name("ref");
291 
292  cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
293  cpctor.type().id(ID_struct_tag);
294  cpctor.type().add(ID_identifier).id(symbol.name);
295  cpctor.operands().push_back(exprt(ID_cpp_declarator));
296  cpctor.add_source_location()=source_location;
297 
298  cpp_declaratort &declarator =
299  static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());
300  declarator.add_source_location()=source_location;
301 
302  cpp_namet &declarator_name=declarator.name();
303  typet &declarator_type=declarator.type();
304 
305  declarator_type.add_source_location()=source_location;
306 
307  declarator_name.id(ID_cpp_name);
308  declarator_name.get_sub().push_back(irept(ID_operator));
309  declarator_name.get_sub().push_back(irept("="));
310 
311  declarator_type.id(ID_function_type);
312  declarator_type.subtype() = reference_type(uninitialized_typet{});
313  declarator_type.subtype().add(ID_C_qualifier).make_nil();
314 
315  exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));
316  args.add_source_location()=source_location;
317 
318  args.get_sub().push_back(irept(ID_cpp_declaration));
319 
320  cpp_declarationt &args_decl=
321  static_cast<cpp_declarationt&>(args.get_sub().back());
322 
323  auto &args_decl_type_sub = to_type_with_subtypes(args_decl.type()).subtypes();
324 
325  args_decl.type().id(ID_merged_type);
326  args_decl_type_sub.push_back(
327  cpp_namet(symbol.base_name, source_location).as_type());
328 
329  args_decl_type_sub.push_back(typet(ID_const));
330  args_decl.operands().push_back(exprt(ID_cpp_declarator));
331  args_decl.add_source_location()=source_location;
332 
333  cpp_declaratort &args_decl_declor=
334  static_cast<cpp_declaratort&>(args_decl.operands().back());
335 
336  args_decl_declor.name() = cpp_namet(arg_name, source_location);
337  args_decl_declor.add_source_location()=source_location;
338 
339  args_decl_declor.type() = pointer_type(uninitialized_typet{});
340  args_decl_declor.type().set(ID_C_reference, true);
341  args_decl_declor.value().make_nil();
342 }
343 
346  const symbolt &symbol,
347  cpp_declaratort &declarator)
348 {
349  // save source location
350  source_locationt source_location=declarator.source_location();
351  declarator.make_nil();
352 
353  code_blockt block;
354 
355  std::string arg_name("ref");
356 
357  // First, we copy the parents
358  for(const auto &b : to_struct_type(symbol.type).bases())
359  {
360  DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
361 
362  const symbolt &symb = lookup(b.type());
363 
364  copy_parent(source_location, symb.base_name, arg_name, block);
365  }
366 
367  // Then, we copy the members
368  for(const auto &c : to_struct_type(symbol.type).components())
369  {
370  if(
371  c.get_bool(ID_from_base) || c.get_bool(ID_is_type) ||
372  c.get_bool(ID_is_static) || c.get_bool(ID_is_vtptr) ||
373  c.type().id() == ID_code)
374  {
375  continue;
376  }
377 
378  const irep_idt &mem_name = c.get_base_name();
379 
380  if(c.type().id() == ID_array)
381  {
382  const exprt &size_expr = to_array_type(c.type()).size();
383 
384  if(size_expr.id()==ID_infinity)
385  {
386  // error().source_location=object);
387  // err << "cannot copy array of infinite size\n";
388  // throw 0;
389  continue;
390  }
391 
392  const auto size = numeric_cast<mp_integer>(size_expr);
393  CHECK_RETURN(!size.has_value());
394  CHECK_RETURN(*size >= 0);
395 
396  for(mp_integer i = 0; i < *size; ++i)
397  copy_array(source_location, mem_name, i, arg_name, block);
398  }
399  else
400  copy_member(source_location, mem_name, arg_name, block);
401  }
402 
403  // Finally we add the return statement
404  block.add(
406 
407  declarator.value() = std::move(block);
408  declarator.value().add_source_location() = source_location;
409 }
410 
419  const struct_typet::basest &bases,
420  const struct_typet::componentst &components,
421  const irept &initializers)
422 {
423  assert(initializers.id()==ID_member_initializers);
424 
425  forall_irep(init_it, initializers.get_sub())
426  {
427  const irept &initializer=*init_it;
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  forall_irep(m_it, initializers.get_sub())
604  {
605  irept initializer=*m_it;
606 
607  const cpp_namet &member_name=
608  to_cpp_name(initializer.find(ID_member));
609 
610  bool has_template_args=member_name.has_template_args();
611 
612  if(!has_template_args)
613  {
614  irep_idt base_name=member_name.get_base_name();
615 
616  // check if the initializer is a data
617  bool is_data=false;
618 
619  for(const auto &c : components)
620  {
621  if(
622  c.get_base_name() == base_name && c.type().id() != ID_code &&
623  !c.get_bool(ID_is_type))
624  {
625  is_data=true;
626  break;
627  }
628  }
629 
630  if(is_data)
631  continue;
632  }
633 
634  typet member_type=
635  static_cast<const typet&>(initializer.find(ID_member));
636 
637  typecheck_type(member_type);
638 
639  if(member_type.id() != ID_struct_tag)
640  break;
641 
642  if(
643  to_struct_tag_type(b.type()).get_identifier() ==
644  to_struct_tag_type(member_type).get_identifier())
645  {
646  final_initializers.move_to_sub(initializer);
647  found=true;
648  break;
649  }
650  }
651 
652  // Call the parent default constructor
653  if(!found)
654  {
655  const cpp_namet cppname(ctor_name);
656 
657  codet mem_init(ID_member_initializer);
658  mem_init.set(ID_member, cppname);
659  final_initializers.move_to_sub(mem_init);
660  }
661 
662  if(b.get_bool(ID_virtual))
663  {
664  codet tmp(ID_member_initializer);
665  tmp.swap(final_initializers.get_sub().back());
666 
667  code_ifthenelset cond(
668  cpp_namet("@most_derived").as_expr(), std::move(tmp));
669 
670  final_initializers.get_sub().back().swap(cond);
671  }
672  }
673  }
674 
675  // Then, we add the member initializers
676  for(const auto &c : components)
677  {
678  // Take care of virtual tables
679  if(c.get_bool(ID_is_vtptr))
680  {
681  const cpp_namet cppname(c.get_base_name(), c.source_location());
682 
683  const symbolt &virtual_table_symbol_type =
684  lookup(c.type().subtype().get(ID_identifier));
685 
686  const symbolt &virtual_table_symbol_var =
687  lookup(id2string(virtual_table_symbol_type.name) + "@" +
688  id2string(struct_union_type.get(ID_name)));
689 
690  exprt var=virtual_table_symbol_var.symbol_expr();
691  address_of_exprt address(var);
692  assert(address.type() == c.type());
693 
695 
696  exprt ptrmember(ID_ptrmember);
697  ptrmember.set(ID_component_name, c.get_name());
698  ptrmember.operands().push_back(exprt("cpp-this"));
699 
700  code_assignt assign(ptrmember, address);
701  final_initializers.move_to_sub(assign);
702  continue;
703  }
704 
705  if(
706  c.get_bool(ID_from_base) || c.type().id() == ID_code ||
707  c.get_bool(ID_is_type) || c.get_bool(ID_is_static))
708  {
709  continue;
710  }
711 
712  const irep_idt &mem_name = c.get_base_name();
713 
714  // Check if the initialization list of the constructor
715  // explicitly initializes the data member
716  bool found=false;
717  Forall_irep(m_it, initializers.get_sub())
718  {
719  irept &initializer=*m_it;
720 
721  if(initializer.get(ID_member)!=ID_cpp_name)
722  continue;
723  cpp_namet &member_name=(cpp_namet&) initializer.add(ID_member);
724 
725  if(member_name.has_template_args())
726  continue; // base-type initializer
727 
728  irep_idt base_name=member_name.get_base_name();
729 
730  if(mem_name==base_name)
731  {
732  final_initializers.move_to_sub(initializer);
733  found=true;
734  break;
735  }
736  }
737 
738  // If the data member is a reference, it must be explicitly
739  // initialized
740  if(
741  !found && c.type().id() == ID_pointer &&
742  c.type().get_bool(ID_C_reference))
743  {
744  error().source_location = c.source_location();
745  error() << "reference must be explicitly initialized" << eom;
746  throw 0;
747  }
748 
749  // If the data member is not POD and is not explicitly initialized,
750  // then its default constructor is called.
751  if(!found && !cpp_is_pod(c.type()))
752  {
753  cpp_namet cppname(mem_name);
754 
755  codet mem_init(ID_member_initializer);
756  mem_init.set(ID_member, cppname);
757  final_initializers.move_to_sub(mem_init);
758  }
759  }
760 
761  initializers.swap(final_initializers);
762 }
763 
766 bool cpp_typecheckt::find_cpctor(const symbolt &symbol) const
767 {
768  for(const auto &component : to_struct_type(symbol.type).components())
769  {
770  // Skip non-ctor
771  if(component.type().id()!=ID_code ||
772  to_code_type(component.type()).return_type().id() !=ID_constructor)
773  continue;
774 
775  // Skip inherited constructor
776  if(component.get_bool(ID_from_base))
777  continue;
778 
779  const code_typet &code_type=to_code_type(component.type());
780 
781  const code_typet::parameterst &parameters=code_type.parameters();
782 
783  // First parameter is the 'this' pointer. Therefore, copy
784  // constructors have at least two parameters
785  if(parameters.size() < 2)
786  continue;
787 
788  const code_typet::parametert &parameter1=parameters[1];
789 
790  const typet &parameter1_type=parameter1.type();
791 
792  if(!is_reference(parameter1_type))
793  continue;
794 
795  if(parameter1_type.subtype().get(ID_identifier)!=symbol.name)
796  continue;
797 
798  bool defargs=true;
799  for(std::size_t i=2; i<parameters.size(); i++)
800  {
801  if(parameters[i].default_value().is_nil())
802  {
803  defargs=false;
804  break;
805  }
806  }
807 
808  if(defargs)
809  return true;
810  }
811 
812  return false;
813 }
814 
815 bool cpp_typecheckt::find_assignop(const symbolt &symbol) const
816 {
817  const struct_typet &struct_type=to_struct_type(symbol.type);
818  const struct_typet::componentst &components=struct_type.components();
819 
820  for(const auto &component : components)
821  {
822  if(component.get_base_name() != "operator=")
823  continue;
824 
825  if(component.get_bool(ID_is_static))
826  continue;
827 
828  if(component.get_bool(ID_from_base))
829  continue;
830 
831  const code_typet &code_type=to_code_type(component.type());
832 
833  const code_typet::parameterst &args=code_type.parameters();
834 
835  if(args.size()!=2)
836  continue;
837 
838  const code_typet::parametert &arg1=args[1];
839 
840  const typet &arg1_type=arg1.type();
841 
842  if(!is_reference(arg1_type))
843  continue;
844 
845  if(arg1_type.subtype().get(ID_identifier)!=symbol.name)
846  continue;
847 
848  return true;
849  }
850 
851  return false;
852 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
irept::move_to_sub
void move_to_sub(irept &irep)
Definition: irep.cpp:42
irept::make_nil
void make_nil()
Definition: irep.h:475
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:206
cpp_typecheckt::default_assignop_value
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
Definition: cpp_typecheck_constructor.cpp:345
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
messaget::eom
static eomt eom
Definition: message.h:297
type_with_subtypest::subtypes
subtypest & subtypes()
Definition: type.h:191
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
Forall_irep
#define Forall_irep(it, irep)
Definition: irep.h:66
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
array_typet::size
const exprt & size() const
Definition: std_types.h:973
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
cpp_typecheckt::default_ctor
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
Definition: cpp_typecheck_constructor.cpp:119
copy_parent
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.
Definition: cpp_typecheck_constructor.cpp:27
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_typecheckt::get_virtual_bases
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
Definition: cpp_typecheck_compound_type.cpp:1646
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:289
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
cpp_util.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
cpp_typecheckt::check_member_initializers
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
Definition: cpp_typecheck_constructor.cpp:418
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
side_effect_expr_assignt::lhs
exprt & lhs()
Definition: std_code.h:2016
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1990
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::swap
void swap(irept &irep)
Definition: irep.h:463
code_typet
Base type of functions.
Definition: std_types.h:736
cpp_declarationt
Definition: cpp_declaration.h:24
side_effect_expr_assignt::rhs
exprt & rhs()
Definition: std_code.h:2026
irept::id
const irep_idt & id() const
Definition: irep.h:418
struct_typet::basest
std::vector< baset > basest
Definition: std_types.h:254
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
copy_array
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.
Definition: cpp_typecheck_constructor.cpp:86
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
std_code.h
cpp_typecheck.h
C++ Language Type Checking.
source_locationt
Definition: source_location.h:20
cpp_typecheckt::full_member_initialization
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
Definition: cpp_typecheck_constructor.cpp:545
copy_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.
Definition: cpp_typecheck_constructor.cpp:58
reference_type
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
forall_irep
#define forall_irep(it, irep)
Definition: irep.h:62
cpp_namet::has_template_args
bool has_template_args() const
Definition: cpp_name.h:122
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
cpp_namet::source_location
const source_locationt & source_location() const
Definition: cpp_name.h:73
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
cpp_namet::as_expr
const exprt & as_expr() const
Definition: cpp_name.h:133
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
irept::get_sub
subt & get_sub()
Definition: irep.h:477
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::parametert
Definition: std_types.h:753
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
cpp_declaratort::value
exprt & value()
Definition: cpp_declarator.h:42
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
cpp_typecheckt::find_assignop
bool find_assignop(const symbolt &symbol) const
Definition: cpp_typecheck_constructor.cpp:815
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
uninitialized_typet
Definition: cpp_parse_tree.h:32
cpp_namet::get_base_name
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
cpp_typecheckt::find_cpctor
bool find_cpctor(const symbolt &symbol) const
Definition: cpp_typecheck_constructor.cpp:766
cpp_typecheckt::default_assignop
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
Definition: cpp_typecheck_constructor.cpp:278
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
cpp_typecheckt::default_cpctor
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
Definition: cpp_typecheck_constructor.cpp:141
std_expr.h
API to expression classes.
cpp_namet
Definition: cpp_name.h:17
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_namet::to_string
std::string to_string() const
Definition: cpp_name.cpp:76
cpp_declaratort
Definition: cpp_declarator.h:20
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
cpp_namet::as_type
const typet & as_type() const
Definition: cpp_name.h:138
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35