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