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