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