CBMC
cpp_typecheck_compound_type.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 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/arith_tools.h>
19 #include <util/c_types.h>
20 #include <util/std_types.h>
21 #include <util/symbol_table_base.h>
22 
23 #include <ansi-c/c_qualifiers.h>
24 
26 #include "cpp_name.h"
27 #include "cpp_type2name.h"
28 #include "cpp_util.h"
29 
30 #include <algorithm>
31 
33 {
34  if(type.id()==ID_const)
35  return true;
36  else if(type.id()==ID_merged_type)
37  {
38  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
39  {
40  if(has_const(subtype))
41  return true;
42  }
43 
44  return false;
45  }
46  else
47  return false;
48 }
49 
51 {
52  if(type.id()==ID_volatile)
53  return true;
54  else if(type.id()==ID_merged_type)
55  {
56  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
57  {
58  if(has_volatile(subtype))
59  return true;
60  }
61 
62  return false;
63  }
64  else
65  return false;
66 }
67 
69 {
70  if(type.id() == ID_auto)
71  return true;
72  else if(
73  type.id() == ID_merged_type || type.id() == ID_frontend_pointer ||
74  type.id() == ID_pointer)
75  {
76  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
77  {
78  if(has_auto(subtype))
79  return true;
80  }
81 
82  return false;
83  }
84  else
85  return false;
86 }
87 
89  const irep_idt &base_name,
90  bool has_body,
91  bool tag_only_declaration)
92 {
93  // The scope of a compound identifier is difficult,
94  // and is different from C.
95  //
96  // For instance:
97  // class A { class B {} } --> A::B
98  // class A { class B; } --> A::B
99  // class A { class B *p; } --> ::B
100  // class B { }; class A { class B *p; } --> ::B
101  // class B { }; class A { class B; class B *p; } --> A::B
102 
103  // If there is a body, or it's a tag-only declaration,
104  // it's always in the current scope, even if we already have
105  // it in an upwards scope.
106 
107  if(has_body || tag_only_declaration)
108  return cpp_scopes.current_scope();
109 
110  // No body. Not a tag-only-declaration.
111  // Check if we have it already. If so, take it.
112 
113  // we should only look for tags, but we don't
114  const auto id_set =
116 
117  for(const auto &id : id_set)
118  if(id->is_class())
119  return static_cast<cpp_scopet &>(id->get_parent());
120 
121  // Tags without body that we don't have already
122  // and that are not a tag-only declaration go into
123  // the global scope of the namespace.
124  return cpp_scopes.get_global_scope();
125 }
126 
128  struct_union_typet &type)
129 {
130  // first save qualifiers
131  c_qualifierst qualifiers(type);
132 
133  // now clear them from the type
134  type.remove(ID_C_constant);
135  type.remove(ID_C_volatile);
136  type.remove(ID_C_restricted);
137 
138  // get the tag name
139  bool has_tag=type.find(ID_tag).is_not_nil();
140  irep_idt base_name;
141  cpp_scopet *dest_scope=nullptr;
142  bool has_body=type.find(ID_body).is_not_nil();
143  bool tag_only_declaration=type.get_bool(ID_C_tag_only_declaration);
144  bool is_union = type.id() == ID_union;
145 
146  if(!has_tag)
147  {
148  // most of these should be named by now; see
149  // cpp_declarationt::name_anon_struct_union()
150 
151  base_name=std::string("#anon_")+std::to_string(++anon_counter);
152  type.set(ID_C_is_anonymous, true);
153  dest_scope=&cpp_scopes.current_scope();
154  }
155  else
156  {
157  const cpp_namet &cpp_name=
158  to_cpp_name(type.find(ID_tag));
159 
160  // scope given?
161  if(cpp_name.is_simple_name())
162  {
163  base_name=cpp_name.get_base_name();
164 
165  // anonymous structs always go into the current scope
166  if(type.get_bool(ID_C_is_anonymous))
167  dest_scope=&cpp_scopes.current_scope();
168  else
169  dest_scope=&tag_scope(base_name, has_body, tag_only_declaration);
170  }
171  else
172  {
173  cpp_save_scopet cpp_save_scope(cpp_scopes);
174  cpp_typecheck_resolvet cpp_typecheck_resolve(*this);
176  dest_scope=
177  &cpp_typecheck_resolve.resolve_scope(cpp_name, base_name, t_args);
178  }
179  }
180 
181  // The identifier 'tag-X' matches what the C front-end does!
182  // The hyphen is deliberate to avoid collisions with other
183  // identifiers.
184  const irep_idt symbol_name=
185  dest_scope->prefix+
186  "tag-"+id2string(base_name)+
187  dest_scope->suffix;
188 
189  // check if we have it already
190 
191  if(const auto maybe_symbol=symbol_table.lookup(symbol_name))
192  {
193  // we do!
194  const symbolt &symbol=*maybe_symbol;
195 
196  if(has_body)
197  {
198  if(
199  symbol.type.id() == type.id() &&
201  {
202  // a previously incomplete struct/union becomes complete
203  symbolt &writeable_symbol = symbol_table.get_writeable_ref(symbol_name);
204  writeable_symbol.type.swap(type);
205  typecheck_compound_body(writeable_symbol);
206  }
207  else if(symbol.type.get_bool(ID_C_is_anonymous))
208  {
209  // we silently ignore
210  }
211  else
212  {
214  error() << "compound tag '" << base_name << "' declared previously\n"
215  << "location of previous definition: " << symbol.location
216  << eom;
217  throw 0;
218  }
219  }
220  else if(symbol.type.id() != type.id())
221  {
223  error() << "redefinition of '" << symbol.pretty_name << "'"
224  << " as different kind of tag" << eom;
225  throw 0;
226  }
227  }
228  else
229  {
230  // produce new symbol
231  type_symbolt symbol{symbol_name, type, ID_cpp};
232  symbol.base_name=base_name;
233  symbol.location=type.source_location();
234  symbol.module=module;
235  symbol.pretty_name=
237  id2string(symbol.base_name)+
239  symbol.type.set(
240  ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
241 
242  // move early, must be visible before doing body
243  symbolt *new_symbol;
244 
245  if(symbol_table.move(symbol, new_symbol))
246  {
247  error().source_location=symbol.location;
248  error() << "cpp_typecheckt::typecheck_compound_type: "
249  << "symbol_table.move() failed" << eom;
250  throw 0;
251  }
252 
253  // put into dest_scope
254  cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol, *dest_scope);
255 
257  id.is_scope=true;
258  id.prefix=cpp_scopes.current_scope().prefix+
259  id2string(new_symbol->base_name)+
261  id.class_identifier=new_symbol->name;
262  id.id_class=cpp_idt::id_classt::CLASS;
263 
264  if(has_body)
265  typecheck_compound_body(*new_symbol);
266  else
267  {
268  struct_union_typet new_type(new_symbol->type.id());
269  new_type.set(ID_tag, new_symbol->base_name);
270  new_type.make_incomplete();
271  new_type.add_source_location() = type.source_location();
272  new_symbol->type.swap(new_type);
273  }
274  }
275 
276  if(is_union)
277  {
278  // create union tag
279  union_tag_typet tag_type(symbol_name);
280  qualifiers.write(tag_type);
281  type.swap(tag_type);
282  }
283  else
284  {
285  // create struct tag
286  struct_tag_typet tag_type(symbol_name);
287  qualifiers.write(tag_type);
288  type.swap(tag_type);
289  }
290 }
291 
293  const symbolt &symbol,
294  const cpp_declarationt &declaration,
295  cpp_declaratort &declarator,
296  struct_typet::componentst &components,
297  const irep_idt &access,
298  bool is_static,
299  bool is_typedef,
300  bool is_mutable)
301 {
302  bool is_cast_operator=
303  declaration.type().id()=="cpp-cast-operator";
304 
305  if(is_cast_operator)
306  {
307  PRECONDITION(
308  declarator.name().get_sub().size() == 2 &&
309  declarator.name().get_sub().front().id() == ID_operator);
310 
311  typet type=static_cast<typet &>(declarator.name().get_sub()[1]);
312  declarator.type().add_subtype() = type;
313 
314  cpp_namet::namet name("(" + cpp_type2name(type) + ")");
315  declarator.name().get_sub().back().swap(name);
316  }
317 
318  typet final_type=
319  declarator.merge_type(declaration.type());
320 
321  // this triggers template elaboration
322  elaborate_class_template(final_type);
323 
324  typecheck_type(final_type);
325 
326  if(final_type.id() == ID_empty)
327  {
328  error().source_location = declaration.type().source_location();
329  error() << "void-typed member not permitted" << eom;
330  throw 0;
331  }
332 
333  cpp_namet cpp_name;
334  cpp_name.swap(declarator.name());
335 
336  irep_idt base_name;
337 
338  if(cpp_name.is_nil())
339  {
340  // Yes, there can be members without name.
341  base_name=irep_idt();
342  }
343  else if(cpp_name.is_simple_name())
344  {
345  base_name=cpp_name.get_base_name();
346  }
347  else
348  {
350  error() << "declarator in compound needs to be simple name"
351  << eom;
352  throw 0;
353  }
354 
355  bool is_method=!is_typedef && final_type.id()==ID_code;
356  bool is_constructor=declaration.is_constructor();
357  bool is_destructor=declaration.is_destructor();
358  bool is_virtual=declaration.member_spec().is_virtual();
359  bool is_explicit=declaration.member_spec().is_explicit();
360  bool is_inline=declaration.member_spec().is_inline();
361 
362  final_type.set(ID_C_member_name, symbol.name);
363 
364  // first do some sanity checks
365 
366  if(is_virtual && !is_method)
367  {
369  error() << "only methods can be virtual" << eom;
370  throw 0;
371  }
372 
373  if(is_inline && !is_method)
374  {
376  error() << "only methods can be inlined" << eom;
377  throw 0;
378  }
379 
380  if(is_virtual && is_static)
381  {
383  error() << "static methods cannot be virtual" << eom;
384  throw 0;
385  }
386 
387  if(is_cast_operator && is_static)
388  {
390  error() << "cast operators cannot be static" << eom;
391  throw 0;
392  }
393 
394  if(is_constructor && is_virtual)
395  {
397  error() << "constructors cannot be virtual" << eom;
398  throw 0;
399  }
400 
401  if(!is_constructor && is_explicit)
402  {
404  error() << "only constructors can be explicit" << eom;
405  throw 0;
406  }
407 
408  if(is_constructor && base_name != symbol.base_name)
409  {
411  error() << "member function must return a value or void" << eom;
412  throw 0;
413  }
414 
415  if(is_destructor &&
416  base_name!="~"+id2string(symbol.base_name))
417  {
419  error() << "destructor with wrong name" << eom;
420  throw 0;
421  }
422 
423  // now do actual work
424 
425  irep_idt identifier;
426 
427  // the below is a temporary hack
428  // if(is_method || is_static)
429  if(id2string(cpp_scopes.current_scope().prefix).find("#anon")==
430  std::string::npos ||
431  is_method || is_static)
432  {
433  // Identifiers for methods include the scope prefix.
434  // Identifiers for static members include the scope prefix.
435  identifier=
437  id2string(base_name);
438  }
439  else
440  {
441  // otherwise, we keep them simple
442  identifier=base_name;
443  }
444 
445  struct_typet::componentt component(identifier, final_type);
446  component.set(ID_access, access);
447  component.set_base_name(base_name);
448  component.set_pretty_name(base_name);
449  component.add_source_location()=cpp_name.source_location();
450 
451  if(cpp_name.is_operator())
452  {
453  component.set(ID_is_operator, true);
454  component.type().set(ID_C_is_operator, true);
455  }
456 
457  if(is_cast_operator)
458  component.set(ID_is_cast_operator, true);
459 
460  if(declaration.member_spec().is_explicit())
461  component.set(ID_is_explicit, true);
462 
463  // either blank, const, volatile, or const volatile
464  const typet &method_qualifier=
465  static_cast<const typet &>(declarator.add(ID_method_qualifier));
466 
467  if(is_static)
468  {
469  component.set(ID_is_static, true);
470  component.type().set(ID_C_is_static, true);
471  }
472 
473  if(is_typedef)
474  component.set(ID_is_type, true);
475 
476  if(is_mutable)
477  component.set(ID_is_mutable, true);
478 
479  exprt &value=declarator.value();
480  irept &initializers=declarator.member_initializers();
481 
482  if(is_method)
483  {
484  if(
485  value.id() == ID_code &&
486  to_code(value).get_statement() == ID_cpp_delete)
487  {
488  value.make_nil();
489  component.set(ID_access, ID_noaccess);
490  }
491 
492  component.set(ID_is_inline, declaration.member_spec().is_inline());
493 
494  // the 'virtual' name of the function
495  std::string virtual_name = id2string(component.get_base_name()) +
497 
498  if(has_const(method_qualifier))
499  virtual_name+="$const";
500 
501  if(has_volatile(method_qualifier))
502  virtual_name += "$volatile";
503 
504  if(to_code_type(component.type()).return_type().id() == ID_destructor)
505  virtual_name="@dtor";
506 
507  // The method may be virtual implicitly.
508  std::set<irep_idt> virtual_bases;
509 
510  for(const auto &comp : components)
511  {
512  if(comp.get_bool(ID_is_virtual))
513  {
514  if(comp.get(ID_virtual_name) == virtual_name)
515  {
516  is_virtual=true;
517  const code_typet &code_type=to_code_type(comp.type());
519  !code_type.parameters().empty(), "must have parameters");
520  const typet &pointer_type=code_type.parameters()[0].type();
522  pointer_type.id() == ID_pointer, "this must be pointer");
523  virtual_bases.insert(
524  to_pointer_type(pointer_type).base_type().get(ID_identifier));
525  }
526  }
527  }
528 
529  if(!is_virtual)
530  {
532  symbol, component, initializers,
533  method_qualifier, value);
534 
535  if(!value.is_nil() && !is_static)
536  {
538  error() << "no initialization allowed here" << eom;
539  throw 0;
540  }
541  }
542  else // virtual
543  {
544  component.type().set(ID_C_is_virtual, true);
545  component.type().set(ID_C_virtual_name, virtual_name);
546 
547  // Check if it is a pure virtual method
548  if(value.is_not_nil() && value.is_constant())
549  {
550  mp_integer i;
551  to_integer(to_constant_expr(value), i);
552  if(i!=0)
553  {
554  error().source_location = declarator.name().source_location();
555  error() << "expected 0 to mark pure virtual method, got " << i << eom;
556  throw 0;
557  }
558  component.set(ID_is_pure_virtual, true);
559  value.make_nil();
560  }
561 
563  symbol,
564  component,
565  initializers,
566  method_qualifier,
567  value);
568 
569  // get the virtual-table symbol type
570  irep_idt vt_name="virtual_table::"+id2string(symbol.name);
571 
572  if(!symbol_table.has_symbol(vt_name))
573  {
574  // first time: create a virtual-table symbol type
575  type_symbolt vt_symb_type{vt_name, struct_typet(), ID_cpp};
576  vt_symb_type.base_name="virtual_table::"+id2string(symbol.base_name);
577  vt_symb_type.pretty_name=vt_symb_type.base_name;
578  vt_symb_type.module=module;
579  vt_symb_type.location=symbol.location;
580  vt_symb_type.type.set(ID_name, vt_symb_type.name);
581 
582  const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
584 
585  // add a virtual-table pointer
587  id2string(symbol.name) + "::@vtable_pointer",
588  pointer_type(struct_tag_typet(vt_name)));
589  compo.set_base_name("@vtable_pointer");
590  compo.set_pretty_name(id2string(symbol.base_name) + "@vtable_pointer");
591  compo.set(ID_is_vtptr, true);
592  compo.set(ID_access, ID_public);
593  components.push_back(compo);
595  }
596 
598  INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");
599  struct_typet &virtual_table=to_struct_type(vt);
600 
601  component.set(ID_virtual_name, virtual_name);
602  component.set(ID_is_virtual, is_virtual);
603 
604  // add an entry to the virtual table
605  struct_typet::componentt vt_entry(
606  id2string(vt_name) + "::" + virtual_name,
607  pointer_type(component.type()));
608  vt_entry.set_base_name(virtual_name);
609  vt_entry.set_pretty_name(virtual_name);
610  vt_entry.set(ID_access, ID_public);
611  vt_entry.add_source_location()=symbol.location;
612  virtual_table.components().push_back(vt_entry);
613 
614  // take care of overloading
615  while(!virtual_bases.empty())
616  {
617  irep_idt virtual_base=*virtual_bases.begin();
618 
619  // a new function that does 'late casting' of the 'this' parameter
620  symbolt func_symb{
621  id2string(component.get_name()) + "::" + id2string(virtual_base),
622  component.type(),
623  symbol.mode};
624  func_symb.base_name = component.get_base_name();
625  func_symb.pretty_name = component.get_base_name();
626  func_symb.module=module;
627  func_symb.location=component.source_location();
628 
629  // change the type of the 'this' pointer
630  code_typet &code_type=to_code_type(func_symb.type);
631  code_typet::parametert &this_parameter = code_type.parameters().front();
632  to_pointer_type(this_parameter.type())
633  .base_type()
634  .set(ID_identifier, virtual_base);
635 
636  // create symbols for the parameters
637  code_typet::parameterst &args=code_type.parameters();
638  std::size_t i=0;
639  for(auto &arg : args)
640  {
641  irep_idt param_base_name = arg.get_base_name();
642 
643  if(param_base_name.empty())
644  param_base_name = "arg" + std::to_string(i++);
645 
646  symbolt arg_symb{
647  id2string(func_symb.name) + "::" + id2string(param_base_name),
648  arg.type(),
649  symbol.mode};
650  arg_symb.base_name = param_base_name;
651  arg_symb.pretty_name = param_base_name;
652  arg_symb.location=func_symb.location;
653 
654  arg.set_identifier(arg_symb.name);
655 
656  // add the parameter to the symbol table
657  const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
659  }
660 
661  // do the body of the function
662  typecast_exprt late_cast(
663  lookup(args[0].get_identifier()).symbol_expr(),
664  to_code_type(component.type()).parameters()[0].type());
665 
667  symbol_exprt(component.get_name(), component.type()),
668  {late_cast},
670  source_locationt{});
671  expr_call.arguments().reserve(args.size());
672 
673  for(const auto &arg : args)
674  {
675  expr_call.arguments().push_back(
676  lookup(arg.get_identifier()).symbol_expr());
677  }
678 
679  if(code_type.return_type().id()!=ID_empty &&
680  code_type.return_type().id()!=ID_destructor)
681  {
682  expr_call.type()=to_code_type(component.type()).return_type();
683 
684  func_symb.value = code_blockt{{code_frontend_returnt(
685  already_typechecked_exprt{std::move(expr_call)})}};
686  }
687  else
688  {
689  func_symb.value = code_blockt{{code_expressiont(
690  already_typechecked_exprt{std::move(expr_call)})}};
691  }
692 
693  // add this new function to the list of components
694 
696  new_compo.type()=func_symb.type;
697  new_compo.set_name(func_symb.name);
698  components.push_back(new_compo);
699 
700  // add the function to the symbol table
701  {
702  const bool failed=!symbol_table.insert(std::move(func_symb)).second;
704  }
705 
706  put_compound_into_scope(new_compo);
707 
708  // next base
709  virtual_bases.erase(virtual_bases.begin());
710  }
711  }
712  }
713 
714  if(is_static && !is_method) // static non-method member
715  {
716  // add as global variable to symbol_table
717  symbolt static_symbol{identifier, component.type(), symbol.mode};
718  static_symbol.base_name = component.get_base_name();
719  static_symbol.is_lvalue=true;
720  static_symbol.is_static_lifetime=true;
721  static_symbol.location=cpp_name.source_location();
722  static_symbol.is_extern=true;
723 
724  // TODO: not sure about this: should be defined separately!
725  dynamic_initializations.push_back(static_symbol.name);
726 
727  symbolt *new_symbol;
728  if(symbol_table.move(static_symbol, new_symbol))
729  {
731  error() << "redeclaration of static member '" << static_symbol.base_name
732  << "'" << eom;
733  throw 0;
734  }
735 
736  if(value.is_not_nil())
737  {
738  if(cpp_is_pod(new_symbol->type))
739  {
740  new_symbol->value.swap(value);
742  }
743  else
744  {
745  symbol_exprt symexpr = symbol_exprt::typeless(new_symbol->name);
746 
747  exprt::operandst ops;
748  ops.push_back(value);
749  auto defcode = cpp_constructor(source_locationt(), symexpr, ops);
750  CHECK_RETURN(defcode.has_value());
751 
752  new_symbol->value.swap(defcode.value());
753  }
754  }
755  }
756 
757  // array members must have fixed size
759 
761 
762  components.push_back(component);
763 }
764 
767 {
768  if(type.id()==ID_array)
769  {
770  array_typet &array_type=to_array_type(type);
771 
772  if(array_type.size().is_not_nil())
773  {
774  if(array_type.size().id() == ID_symbol)
775  {
776  const symbol_exprt &s = to_symbol_expr(array_type.size());
777  const symbolt &symbol = lookup(s.get_identifier());
778 
779  if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
780  array_type.size() = symbol.value;
781  }
782 
783  make_constant_index(array_type.size());
784  }
785 
786  // recursive call for multi-dimensional arrays
787  check_fixed_size_array(array_type.element_type());
788  }
789 }
790 
792  const struct_union_typet::componentt &compound)
793 {
794  const irep_idt &base_name=compound.get_base_name();
795  const irep_idt &name=compound.get_name();
796 
797  // nothing to do if no base_name (e.g., an anonymous bitfield)
798  if(base_name.empty())
799  return;
800 
801  if(compound.type().id()==ID_code)
802  {
803  // put the symbol into scope
804  cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
805  id.id_class = compound.get_bool(ID_is_type) ? cpp_idt::id_classt::TYPEDEF
807  id.identifier=name;
808  id.class_identifier=cpp_scopes.current_scope().identifier;
809  id.is_member=true;
810  id.is_constructor =
811  to_code_type(compound.type()).return_type().id() == ID_constructor;
812  id.is_method=true;
813  id.is_static_member=compound.get_bool(ID_is_static);
814 
815  // create function block-scope in the scope
816  cpp_idt &id_block=
818  irep_idt(std::string("$block:") + base_name.c_str()));
819 
821  id_block.identifier=name;
823  id_block.is_method=true;
824  id_block.is_static_member=compound.get_bool(ID_is_static);
825 
826  id_block.is_scope=true;
827  id_block.prefix = compound.get_string(ID_prefix);
828  cpp_scopes.id_map[id.identifier]=&id_block;
829  }
830  else
831  {
832  // check if it's already there
833  const auto id_set =
835 
836  for(const auto &id_it : id_set)
837  {
838  const cpp_idt &id=*id_it;
839 
840  // the name is already in the scope
841  // this is ok if they belong to different categories
842  if(!id.is_class() && !id.is_enum())
843  {
845  error() << "'" << base_name << "' already in compound scope" << eom;
846  throw 0;
847  }
848  }
849 
850  // put into the scope
851  cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
852  id.id_class=compound.get_bool(ID_is_type)?
855  id.identifier=name;
856  id.class_identifier=cpp_scopes.current_scope().identifier;
857  id.is_member=true;
858  id.is_method=false;
859  id.is_static_member=compound.get_bool(ID_is_static);
860  }
861 }
862 
864  symbolt &symbol,
865  cpp_declarationt &declaration)
866 {
867  // A friend of a class can be a function/method,
868  // or a struct/class/union type.
869 
870  if(declaration.is_template())
871  {
872  error().source_location=declaration.type().source_location();
873  error() << "friend template not supported" << eom;
874  throw 0;
875  }
876 
877  // we distinguish these whether there is a declarator
878  if(declaration.declarators().empty())
879  {
880  typet &ftype=declaration.type();
881 
882  // must be struct or union
883  if(ftype.id()!=ID_struct && ftype.id()!=ID_union)
884  {
885  error().source_location=declaration.type().source_location();
886  error() << "unexpected friend" << eom;
887  throw 0;
888  }
889 
890  if(ftype.find(ID_body).is_not_nil())
891  {
892  error().source_location=declaration.type().source_location();
893  error() << "friend declaration must not have compound body" << eom;
894  throw 0;
895  }
896 
897  cpp_save_scopet saved_scope(cpp_scopes);
899  typecheck_type(ftype);
900  symbol.type.add(ID_C_friends).move_to_sub(ftype);
901 
902  return;
903  }
904 
905  // It should be a friend function.
906  // Do the declarators.
907 
908 #ifdef DEBUG
909  std::cout << "friend declaration: " << declaration.pretty() << '\n';
910 #endif
911 
912  for(auto &sub_it : declaration.declarators())
913  {
914 #ifdef DEBUG
915  std::cout << "decl: " << sub_it.pretty() << "\n with value "
916  << sub_it.value().pretty() << '\n';
917  std::cout << " scope: " << cpp_scopes.current_scope().prefix << '\n';
918 #endif
919 
920  if(sub_it.value().is_not_nil())
921  declaration.member_spec().set_inline(true);
922 
923  cpp_declarator_convertert cpp_declarator_converter(*this);
924  cpp_declarator_converter.is_friend = true;
925  const symbolt &conv_symb = cpp_declarator_converter.convert(
926  declaration.type(),
927  declaration.storage_spec(),
928  declaration.member_spec(),
929  sub_it);
930  exprt symb_expr = cpp_symbol_expr(conv_symb);
931  symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
932  }
933 }
934 
936 {
937  cpp_save_scopet saved_scope(cpp_scopes);
938 
939  // enter scope of compound
940  cpp_scopes.set_scope(symbol.name);
941 
942  PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union);
943 
944  struct_union_typet &type=
945  to_struct_union_type(symbol.type);
946 
947  // pull the base types in
948  if(!type.find(ID_bases).get_sub().empty())
949  {
950  if(type.id()==ID_union)
951  {
952  error().source_location=symbol.location;
953  error() << "union types must not have bases" << eom;
954  throw 0;
955  }
956 
958  }
959 
960  exprt &body=static_cast<exprt &>(type.add(ID_body));
961  struct_union_typet::componentst &components=type.components();
962 
963  symbol.type.set(ID_name, symbol.name);
964 
965  // default access
966  irep_idt access = type.default_access();
967 
968  bool found_ctor=false;
969  bool found_dtor=false;
970 
971  // we first do everything _but_ the constructors
972 
973  Forall_operands(it, body)
974  {
975  if(it->id()==ID_cpp_declaration)
976  {
977  cpp_declarationt &declaration=
978  to_cpp_declaration(*it);
979 
980  if(declaration.member_spec().is_friend())
981  {
982  typecheck_friend_declaration(symbol, declaration);
983  continue; // done
984  }
985 
986  if(declaration.is_template())
987  {
988  // remember access mode
989  declaration.set(ID_C_access, access);
990  convert_template_declaration(declaration);
991  continue;
992  }
993 
994  if(declaration.type().id().empty())
995  continue;
996 
997  bool is_typedef=declaration.is_typedef();
998 
999  // is it tag-only?
1000  if(declaration.type().id()==ID_struct ||
1001  declaration.type().id()==ID_union ||
1002  declaration.type().id()==ID_c_enum)
1003  if(declaration.declarators().empty())
1004  declaration.type().set(ID_C_tag_only_declaration, true);
1005 
1006  declaration.name_anon_struct_union();
1007  typecheck_type(declaration.type());
1008 
1009  bool is_static=declaration.storage_spec().is_static();
1010  bool is_mutable=declaration.storage_spec().is_mutable();
1011 
1012  if(declaration.storage_spec().is_extern() ||
1013  declaration.storage_spec().is_auto() ||
1014  declaration.storage_spec().is_register())
1015  {
1016  error().source_location=declaration.storage_spec().location();
1017  error() << "invalid storage class specified for field" << eom;
1018  throw 0;
1019  }
1020 
1021  // anonymous member?
1022  if(
1023  declaration.declarators().empty() &&
1024  ((declaration.type().id() == ID_struct_tag &&
1025  follow_tag(to_struct_tag_type(declaration.type()))
1026  .get_bool(ID_C_is_anonymous)) ||
1027  (declaration.type().id() == ID_union_tag &&
1028  follow_tag(to_union_tag_type(declaration.type()))
1029  .get_bool(ID_C_is_anonymous)) ||
1030  declaration.type().get_bool(ID_C_is_anonymous)))
1031  {
1032  // we only allow this on struct/union types
1033  if(
1034  declaration.type().id() != ID_union_tag &&
1035  declaration.type().id() != ID_struct_tag)
1036  {
1037  error().source_location=declaration.type().source_location();
1038  error() << "member declaration does not declare anything"
1039  << eom;
1040  throw 0;
1041  }
1042 
1044  declaration, access, components);
1045 
1046  continue;
1047  }
1048 
1049  // declarators
1050  for(auto &declarator : declaration.declarators())
1051  {
1052  // Skip the constructors until all the data members
1053  // are discovered
1054  if(declaration.is_destructor())
1055  found_dtor=true;
1056 
1057  if(declaration.is_constructor())
1058  {
1059  found_ctor=true;
1060  continue;
1061  }
1062 
1064  symbol,
1065  declaration, declarator, components,
1066  access, is_static, is_typedef, is_mutable);
1067  }
1068  }
1069  else if(it->id()=="cpp-public")
1070  access=ID_public;
1071  else if(it->id()=="cpp-private")
1072  access=ID_private;
1073  else if(it->id()=="cpp-protected")
1074  access=ID_protected;
1075  else
1076  {
1077  }
1078  }
1079 
1080  // Add the default dtor, if needed
1081  // (we have to do the destructor before building the virtual tables,
1082  // as the destructor may be virtual!)
1083 
1084  if((found_ctor || !cpp_is_pod(symbol.type)) && !found_dtor)
1085  {
1086  // build declaration
1088  default_dtor(symbol, dtor);
1089 
1091  symbol,
1092  dtor, dtor.declarators()[0], components,
1093  ID_public, false, false, false);
1094  }
1095 
1096  // set up virtual tables before doing the constructors
1097  if(symbol.type.id()==ID_struct)
1098  do_virtual_table(symbol);
1099 
1100  if(!found_ctor && !cpp_is_pod(symbol.type))
1101  {
1102  // it's public!
1103  exprt cpp_public("cpp-public");
1104  body.add_to_operands(std::move(cpp_public));
1105 
1106  // build declaration
1107  cpp_declarationt ctor;
1108  default_ctor(symbol.type.source_location(), symbol.base_name, ctor);
1109  body.add_to_operands(std::move(ctor));
1110  }
1111 
1112  // Reset the access type
1113  access = type.default_access();
1114 
1115  // All the data members are now known.
1116  // We now deal with the constructors that we are given.
1117  Forall_operands(it, body)
1118  {
1119  if(it->id()==ID_cpp_declaration)
1120  {
1121  cpp_declarationt &declaration=
1122  to_cpp_declaration(*it);
1123 
1124  if(!declaration.is_constructor())
1125  continue;
1126 
1127  for(auto &declarator : declaration.declarators())
1128  {
1129  #if 0
1130  irep_idt ctor_base_name=
1131  declarator.name().get_base_name();
1132  #endif
1133 
1134  if(declarator.value().is_not_nil()) // body?
1135  {
1136  if(declarator.find(ID_member_initializers).is_nil())
1137  declarator.set(ID_member_initializers, ID_member_initializers);
1138 
1139  if(type.id() == ID_union)
1140  {
1142  {}, type.components(), declarator.member_initializers());
1143  }
1144  else
1145  {
1147  to_struct_type(type).bases(),
1148  type.components(),
1149  declarator.member_initializers());
1150  }
1151 
1153  type,
1154  declarator.member_initializers());
1155  }
1156 
1157  // Finally, we typecheck the constructor with the
1158  // full member-initialization list
1159  // Shall all be false
1160  bool is_static=declaration.storage_spec().is_static();
1161  bool is_mutable=declaration.storage_spec().is_mutable();
1162  bool is_typedef=declaration.is_typedef();
1163 
1165  symbol,
1166  declaration, declarator, components,
1167  access, is_static, is_typedef, is_mutable);
1168  }
1169  }
1170  else if(it->id()=="cpp-public")
1171  access=ID_public;
1172  else if(it->id()=="cpp-private")
1173  access=ID_private;
1174  else if(it->id()=="cpp-protected")
1175  access=ID_protected;
1176  else
1177  {
1178  }
1179  }
1180 
1181  if(!cpp_is_pod(symbol.type))
1182  {
1183  // Add the default copy constructor
1185 
1186  if(!find_cpctor(symbol))
1187  {
1188  // build declaration
1189  cpp_declarationt cpctor;
1190  default_cpctor(symbol, cpctor);
1191  CHECK_RETURN(cpctor.declarators().size() == 1);
1192 
1193  exprt value(ID_cpp_not_typechecked);
1194  value.copy_to_operands(cpctor.declarators()[0].value());
1195  cpctor.declarators()[0].value()=value;
1196 
1198  symbol,
1199  cpctor, cpctor.declarators()[0], components,
1200  ID_public, false, false, false);
1201  }
1202 
1203  // Add the default assignment operator
1204  if(!find_assignop(symbol))
1205  {
1206  // build declaration
1207  cpp_declarationt assignop;
1208  default_assignop(symbol, assignop);
1209  CHECK_RETURN(assignop.declarators().size() == 1);
1210 
1211  // The value will be typechecked only if the operator
1212  // is actually used
1213  cpp_declaratort declarator;
1214  assignop.declarators().push_back(declarator);
1215  assignop.declarators()[0].value() = exprt(ID_cpp_not_typechecked);
1216 
1218  symbol,
1219  assignop, assignop.declarators()[0], components,
1220  ID_public, false, false, false);
1221  }
1222  }
1223 
1224  // clean up!
1225  symbol.type.remove(ID_body);
1226 }
1227 
1229  irept &initializers,
1230  const code_typet &type,
1231  exprt &value)
1232 {
1233  // see if we have initializers
1234  if(!initializers.get_sub().empty())
1235  {
1236  const source_locationt &location=
1237  static_cast<const source_locationt &>(
1238  initializers.find(ID_C_source_location));
1239 
1240  if(type.return_type().id() != ID_constructor)
1241  {
1242  error().source_location=location;
1243  error() << "only constructors are allowed to "
1244  << "have member initializers" << eom;
1245  throw 0;
1246  }
1247 
1248  if(value.is_nil())
1249  {
1250  error().source_location=location;
1251  error() << "only constructors with body are allowed to "
1252  << "have member initializers" << eom;
1253  throw 0;
1254  }
1255 
1256  if(to_code(value).get_statement() != ID_block)
1257  value = code_blockt{{to_code(value)}};
1258 
1259  exprt::operandst::iterator o_it=value.operands().begin();
1260  for(const auto &initializer : initializers.get_sub())
1261  {
1262  o_it =
1263  value.operands().insert(o_it, static_cast<const exprt &>(initializer));
1264  o_it++;
1265  }
1266  }
1267 }
1268 
1270  const symbolt &compound_symbol,
1272  irept &initializers,
1273  const typet &method_qualifier,
1274  exprt &value)
1275 {
1276  code_typet &type = to_code_type(component.type());
1277 
1278  if(component.get_bool(ID_is_static))
1279  {
1280  if(!method_qualifier.id().empty())
1281  {
1282  error().source_location=component.source_location();
1283  error() << "method is static -- no qualifiers allowed" << eom;
1284  throw 0;
1285  }
1286  }
1287  else
1288  {
1289  add_this_to_method_type(compound_symbol, type, method_qualifier);
1290  }
1291 
1292  if(value.id() == ID_cpp_not_typechecked && value.has_operands())
1293  {
1295  initializers, type, to_multi_ary_expr(value).op0());
1296  }
1297  else
1298  move_member_initializers(initializers, type, value);
1299 
1300  irep_idt f_id=
1302 
1303  const irep_idt identifier=
1305  id2string(component.get_base_name())+
1306  id2string(f_id);
1307 
1308  component.set_name(identifier);
1309  component.set(ID_prefix, id2string(identifier) + "::");
1310 
1311  if(value.is_not_nil())
1312  to_code_type(type).set_inlined(true);
1313 
1314  symbolt symbol{identifier, type, compound_symbol.mode};
1315  symbol.base_name=component.get_base_name();
1316  symbol.value.swap(value);
1317  symbol.module=module;
1318  symbol.location=component.source_location();
1319 
1320  // move early, it must be visible before doing any value
1321  symbolt *new_symbol;
1322 
1323  const bool symbol_exists = symbol_table.move(symbol, new_symbol);
1324  if(symbol_exists && new_symbol->is_weak)
1325  {
1326  // there might have been an earlier friend declaration
1327  *new_symbol = std::move(symbol);
1328  }
1329  else if(symbol_exists)
1330  {
1331  error().source_location=symbol.location;
1332  error() << "failed to insert new method symbol: " << symbol.name << '\n'
1333  << "name of previous symbol: " << new_symbol->name << '\n'
1334  << "location of previous symbol: " << new_symbol->location << eom;
1335 
1336  throw 0;
1337  }
1338 
1339  // Is this in a class template?
1340  // If so, we defer typechecking until used.
1342  deferred_typechecking.insert(new_symbol->name);
1343  else // remember for later typechecking of body
1344  add_method_body(new_symbol);
1345 }
1346 
1348  const symbolt &compound_symbol,
1349  code_typet &type,
1350  const typet &method_qualifier)
1351 {
1352  typet subtype;
1353 
1354  if(compound_symbol.type.id() == ID_union)
1355  subtype = union_tag_typet(compound_symbol.name);
1356  else
1357  subtype = struct_tag_typet(compound_symbol.name);
1358 
1359  if(has_const(method_qualifier))
1360  subtype.set(ID_C_constant, true);
1361 
1362  if(has_volatile(method_qualifier))
1363  subtype.set(ID_C_volatile, true);
1364 
1365  code_typet::parametert parameter(pointer_type(subtype));
1366  parameter.set_identifier(ID_this);
1367  parameter.set_base_name(ID_this);
1368  parameter.set_this();
1370  convert_parameter(compound_symbol.mode, parameter);
1371 
1372  code_typet::parameterst &parameters = type.parameters();
1373  parameters.insert(parameters.begin(), parameter);
1374 }
1375 
1377  const symbolt &struct_union_symbol)
1378 {
1379  const struct_union_typet &struct_union_type=
1380  to_struct_union_type(struct_union_symbol.type);
1381 
1382  const struct_union_typet::componentst &struct_union_components=
1383  struct_union_type.components();
1384 
1385  // do scoping -- the members of the struct/union
1386  // should be visible in the containing struct/union,
1387  // and that recursively!
1388 
1389  for(const auto &comp : struct_union_components)
1390  {
1391  if(comp.type().id()==ID_code)
1392  {
1393  error().source_location=struct_union_symbol.type.source_location();
1394  error() << "anonymous struct/union member '"
1395  << struct_union_symbol.base_name
1396  << "' shall not have function members" << eom;
1397  throw 0;
1398  }
1399 
1400  if(comp.get_anonymous())
1401  {
1402  const symbolt &symbol=lookup(comp.type().get(ID_identifier));
1403  // recursive call
1405  }
1406  else
1407  {
1408  const irep_idt &base_name=comp.get_base_name();
1409 
1410  if(cpp_scopes.current_scope().contains(base_name))
1411  {
1412  error().source_location=comp.source_location();
1413  error() << "'" << base_name << "' already in scope" << eom;
1414  throw 0;
1415  }
1416 
1417  cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
1419  id.identifier=comp.get_name();
1420  id.class_identifier=struct_union_symbol.name;
1421  id.is_member=true;
1422  }
1423  }
1424 }
1425 
1427  const cpp_declarationt &declaration,
1428  const irep_idt &access,
1429  struct_typet::componentst &components)
1430 {
1431  const struct_union_typet &final_type =
1432  declaration.type().id() == ID_struct_tag
1433  ? static_cast<const struct_union_typet &>(
1434  follow_tag(to_struct_tag_type(declaration.type())))
1435  : static_cast<const struct_union_typet &>(
1436  follow_tag(to_union_tag_type(declaration.type())));
1437  symbolt &struct_union_symbol =
1438  symbol_table.get_writeable_ref(final_type.get(ID_name));
1439 
1440  if(declaration.storage_spec().is_static() ||
1441  declaration.storage_spec().is_mutable())
1442  {
1443  error().source_location=struct_union_symbol.type.source_location();
1444  error() << "storage class is not allowed here" << eom;
1445  throw 0;
1446  }
1447 
1448  if(!cpp_is_pod(struct_union_symbol.type))
1449  {
1450  error().source_location=struct_union_symbol.type.source_location();
1451  error() << "anonymous struct/union member is not POD" << eom;
1452  throw 0;
1453  }
1454 
1455  // produce an anonymous member
1456  irep_idt base_name="#anon_member"+std::to_string(components.size());
1457 
1458  irep_idt identifier=
1460  base_name.c_str();
1461 
1462  typet compound_type;
1463 
1464  if(struct_union_symbol.type.id() == ID_union)
1465  compound_type = union_tag_typet(struct_union_symbol.name);
1466  else
1467  compound_type = struct_tag_typet(struct_union_symbol.name);
1468 
1469  struct_typet::componentt component(identifier, compound_type);
1470  component.set_access(access);
1471  component.set_base_name(base_name);
1472  component.set_pretty_name(base_name);
1473  component.set_anonymous(true);
1474  component.add_source_location()=declaration.source_location();
1475 
1476  components.push_back(component);
1477 
1478  add_anonymous_members_to_scope(struct_union_symbol);
1479 
1481 
1482  struct_union_symbol.type.set(ID_C_unnamed_object, base_name);
1483 }
1484 
1486  const source_locationt &source_location,
1487  const exprt &object,
1488  const irep_idt &component_name,
1489  exprt &member)
1490 {
1491  PRECONDITION(
1492  object.type().id() == ID_struct_tag || object.type().id() == ID_union_tag);
1493 
1494  struct_union_typet final_type =
1495  object.type().id() == ID_struct_tag
1496  ? static_cast<const struct_union_typet &>(
1497  follow_tag(to_struct_tag_type(object.type())))
1498  : static_cast<const struct_union_typet &>(
1499  follow_tag(to_union_tag_type(object.type())));
1500 
1501  const struct_union_typet::componentst &components=
1502  final_type.components();
1503 
1504  for(const auto &component : components)
1505  {
1506  member_exprt tmp(object, component.get_name(), component.type());
1507  tmp.add_source_location()=source_location;
1508 
1509  if(component.get_name()==component_name)
1510  {
1511  member.swap(tmp);
1512 
1513  bool not_ok=check_component_access(component, final_type);
1514  if(not_ok)
1515  {
1517  {
1518  member.set(ID_C_not_accessible, true);
1519  member.set(ID_C_access, component.get(ID_access));
1520  }
1521  else
1522  {
1523  error().source_location=source_location;
1524  error() << "member '" << component_name << "' is not accessible ("
1525  << component.get(ID_access) << ")" << eom;
1526  throw 0;
1527  }
1528  }
1529 
1530  if(object.get_bool(ID_C_lvalue))
1531  member.set(ID_C_lvalue, true);
1532 
1533  if(
1534  object.type().get_bool(ID_C_constant) &&
1535  !component.get_bool(ID_is_mutable))
1536  {
1537  member.type().set(ID_C_constant, true);
1538  }
1539 
1540  member.add_source_location()=source_location;
1541 
1542  return true; // component found
1543  }
1544  else if(
1545  (component.type().id() == ID_struct_tag &&
1547  .find(ID_C_unnamed_object)
1548  .is_not_nil()) ||
1549  (component.type().id() == ID_union_tag &&
1551  .find(ID_C_unnamed_object)
1552  .is_not_nil()) ||
1553  component.type().find(ID_C_unnamed_object).is_not_nil())
1554  {
1555  // could be anonymous union or struct
1556 
1557  if(
1558  component.type().id() == ID_union_tag ||
1559  component.type().id() == ID_struct_tag)
1560  {
1561  // recursive call!
1562  if(get_component(source_location, tmp, component_name, member))
1563  {
1564  if(check_component_access(component, final_type))
1565  {
1566  error().source_location=source_location;
1567  error() << "member '" << component_name << "' is not accessible"
1568  << eom;
1569  throw 0;
1570  }
1571 
1572  if(object.get_bool(ID_C_lvalue))
1573  member.set(ID_C_lvalue, true);
1574 
1575  if(
1576  object.get_bool(ID_C_constant) &&
1577  !component.get_bool(ID_is_mutable))
1578  {
1579  member.type().set(ID_C_constant, true);
1580  }
1581 
1582  member.add_source_location()=source_location;
1583  return true; // component found
1584  }
1585  }
1586  }
1587  }
1588 
1589  return false; // component not found
1590 }
1591 
1594  const struct_union_typet &struct_union_type)
1595 {
1596  const irep_idt &access=component.get(ID_access);
1597 
1598  if(access == ID_noaccess)
1599  return true; // not ok
1600 
1601  if(access==ID_public)
1602  return false; // ok
1603 
1604  PRECONDITION(access == ID_private || access == ID_protected);
1605 
1606  const irep_idt &struct_identifier=
1607  struct_union_type.get(ID_name);
1608 
1609  for(cpp_scopet *pscope = &(cpp_scopes.current_scope());
1610  !(pscope->is_root_scope());
1611  pscope = &(pscope->get_parent()))
1612  {
1613  if(pscope->is_class())
1614  {
1615  if(pscope->identifier==struct_identifier)
1616  return false; // ok
1617 
1618  const struct_typet &scope_struct=
1619  to_struct_type(lookup(pscope->identifier).type);
1620 
1621  if(subtype_typecast(
1622  to_struct_type(struct_union_type), scope_struct))
1623  return false; // ok
1624 
1625  else break;
1626  }
1627  }
1628 
1629  // check friendship
1630  const irept::subt &friends = struct_union_type.find(ID_C_friends).get_sub();
1631 
1632  for(const auto &friend_symb : friends)
1633  {
1634  const cpp_scopet &friend_scope =
1635  cpp_scopes.get_scope(friend_symb.get(ID_identifier));
1636 
1637  for(cpp_scopet *pscope = &(cpp_scopes.current_scope());
1638  !(pscope->is_root_scope());
1639  pscope = &(pscope->get_parent()))
1640  {
1641  if(friend_scope.identifier==pscope->identifier)
1642  return false; // ok
1643 
1644  if(pscope->is_class())
1645  break;
1646  }
1647  }
1648 
1649  return true; // not ok
1650 }
1651 
1653  const struct_typet &type,
1654  std::set<irep_idt> &set_bases) const
1655 {
1656  for(const auto &b : type.bases())
1657  {
1658  DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
1659 
1660  const struct_typet &base = to_struct_type(lookup(b.type()).type);
1661 
1662  set_bases.insert(base.get(ID_name));
1663  get_bases(base, set_bases);
1664  }
1665 }
1666 
1668  const struct_typet &type,
1669  std::list<irep_idt> &vbases) const
1670 {
1671  if(std::find(vbases.begin(), vbases.end(), type.get(ID_name))!=vbases.end())
1672  return;
1673 
1674  for(const auto &b : type.bases())
1675  {
1676  DATA_INVARIANT(b.id() == ID_base, "base class expression expected");
1677 
1678  const struct_typet &base = to_struct_type(lookup(b.type()).type);
1679 
1680  if(b.get_bool(ID_virtual))
1681  vbases.push_back(base.get(ID_name));
1682 
1683  get_virtual_bases(base, vbases);
1684  }
1685 }
1686 
1688  const struct_typet &from,
1689  const struct_typet &to) const
1690 {
1691  if(from.get(ID_name)==to.get(ID_name))
1692  return true;
1693 
1694  std::set<irep_idt> bases;
1695 
1696  get_bases(from, bases);
1697 
1698  return bases.find(to.get(ID_name))!=bases.end();
1699 }
1700 
1702  exprt &expr,
1703  const pointer_typet &dest_type)
1704 {
1705  typet src_type=expr.type();
1706 
1707  PRECONDITION(src_type.id() == ID_pointer);
1708 
1709  const struct_typet &src_struct =
1710  follow_tag(to_struct_tag_type(to_pointer_type(src_type).base_type()));
1711 
1712  const struct_typet &dest_struct =
1713  follow_tag(to_struct_tag_type(dest_type.base_type()));
1714 
1715  PRECONDITION(
1716  subtype_typecast(src_struct, dest_struct) ||
1717  subtype_typecast(dest_struct, src_struct));
1718 
1719  expr = typecast_exprt(expr, dest_type);
1720 }
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
virtual void write(typet &src) const
symbol_table_baset & symbol_table
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
const irep_idt module
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of an expression statement.
Definition: std_code.h:1394
codet representation of a "return from a function" statement.
Definition: std_code.h:893
void set_base_name(const irep_idt &name)
Definition: std_types.h:629
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:624
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
void set_inlined(bool value)
Definition: std_types.h:714
const parameterst & parameters() const
Definition: std_types.h:699
const irep_idt & get_statement() const
Definition: std_code_base.h:65
bool is_destructor() const
const declaratorst & declarators() const
bool is_template() const
const cpp_storage_spect & storage_spec() const
const cpp_member_spect & member_spec() const
bool is_constructor() const
bool is_typedef() const
void name_anon_struct_union()
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
irept & member_initializers()
cpp_namet & name()
typet merge_type(const typet &declaration_type) const
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
std::string prefix
Definition: cpp_id.h:79
bool is_scope
Definition: cpp_id.h:43
id_classt id_class
Definition: cpp_id.h:45
bool is_method
Definition: cpp_id.h:42
bool is_template_scope() const
Definition: cpp_id.h:67
bool is_static_member
Definition: cpp_id.h:42
irep_idt class_identifier
Definition: cpp_id.h:75
std::string suffix
Definition: cpp_id.h:79
void set_inline(bool value)
bool is_inline() const
bool is_friend() const
bool is_virtual() const
bool is_explicit() const
bool is_operator() const
Definition: cpp_name.h:97
irep_idt get_base_name() const
Definition: cpp_name.cpp:14
const source_locationt & source_location() const
Definition: cpp_name.h:73
bool is_simple_name() const
Definition: cpp_name.h:89
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:87
cpp_scopet & get_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:80
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
id_mapt id_map
Definition: cpp_scopes.h:68
void go_to_global_scope()
Definition: cpp_scopes.h:110
cpp_scopet & get_global_scope()
Definition: cpp_scopes.h:115
cpp_scopet & get_parent() const
Definition: cpp_scope.h:88
@ SCOPE_ONLY
Definition: cpp_scope.h:30
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
bool contains(const irep_idt &base_name_to_lookup)
Definition: cpp_scope.cpp:201
source_locationt & location()
bool is_register() const
bool is_static() const
bool is_auto() const
bool is_mutable() const
bool is_extern() const
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void typecheck_compound_body(symbolt &symbol)
void do_virtual_table(const symbolt &symbol)
void put_compound_into_scope(const struct_union_typet::componentt &component)
void typecheck_type(typet &) override
void convert_anon_struct_union_member(const cpp_declarationt &declaration, const irep_idt &access, struct_typet::componentst &components)
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
static bool has_const(const typet &type)
dynamic_initializationst dynamic_initializations
void convert_template_declaration(cpp_declarationt &declaration)
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
unsigned anon_counter
bool check_component_access(const struct_union_typet::componentt &component, const struct_union_typet &struct_union_type)
void typecheck_member_function(const symbolt &compound_symbol, struct_typet::componentt &component, irept &initializers, const typet &method_qualifier, exprt &value)
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void check_fixed_size_array(typet &type)
check that an array has fixed size
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool find_assignop(const symbolt &symbol) const
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
void typecheck_compound_type(struct_union_typet &) override
void add_anonymous_members_to_scope(const symbolt &struct_union_symbol)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
std::unordered_set< irep_idt > deferred_typechecking
void add_method_body(symbolt *_method_symbol)
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_compound_bases(struct_typet &type)
void elaborate_class_template(const typet &type)
elaborate class template instances
static bool has_auto(const typet &type)
static bool has_volatile(const typet &type)
irep_idt function_identifier(const typet &type)
for function overloading
void typecheck_friend_declaration(symbolt &symbol, cpp_declarationt &cpp_declaration)
void add_this_to_method_type(const symbolt &compound_symbol, code_typet &method_type, const typet &method_qualifier)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
void convert_parameter(const irep_idt &current_mode, code_typet::parametert &parameter)
bool find_cpctor(const symbolt &symbol) const
void move_member_initializers(irept &initializers, const code_typet &type, exprt &value)
bool disable_access_control
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
void get_bases(const struct_typet &type, std::set< irep_idt > &set_bases) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
const char * c_str() const
Definition: dstring.h:116
std::string::const_iterator begin() const
Definition: dstring.h:193
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void remove(const irep_idt &name)
Definition: irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
void move_to_sub(irept &irep)
Definition: irep.cpp:35
void swap(irept &irep)
Definition: irep.h:434
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:401
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:368
Extract member of struct or union.
Definition: std_expr.h:2844
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
static eomt eom
Definition: message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
exprt::operandst & arguments()
Definition: std_code.h:1718
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
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
const irep_idt & get_name() const
Definition: std_types.h:79
const irep_idt & get_base_name() const
Definition: std_types.h:89
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:114
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:94
void set_name(const irep_idt &name)
Definition: std_types.h:84
Base type for structs and unions.
Definition: std_types.h:62
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition: std_types.h:179
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
const componentst & components() const
Definition: std_types.h:147
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:191
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:131
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:150
const irep_idt & get_identifier() const
Definition: std_expr.h:160
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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
bool is_weak
Definition: symbol.h:78
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:139
Semantic type conversion.
Definition: std_expr.h:2068
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
typet & add_subtype()
Definition: type.h:53
source_locationt & add_source_location()
Definition: type.h:77
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:199
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
std::string cpp_type2name(const typet &type)
C++ Language Module.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
static bool symbol_exists(const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available)
Returns true iff the given symbol exists and satisfies requirements.
Definition: dfcc_utils.cpp:33
#define Forall_operands(it, expr)
Definition: expr.h:27
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
static bool is_constructor(const irep_idt &method_name)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
BigInt mp_integer
Definition: smt_terms.h:17
#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:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
Pre-defined types.
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:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Author: Diffblue Ltd.
static bool failed(bool error_indicator)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:252
dstringt irep_idt