cprover
cpp_typecheck_expr.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/config.h>
21 #include <util/expr_initializer.h>
23 #include <util/pointer_expr.h>
25 
26 #include <ansi-c/c_qualifiers.h>
27 
28 #include "cpp_exception_id.h"
29 #include "cpp_type2name.h"
30 #include "cpp_typecheck_fargs.h"
31 #include "cpp_util.h"
32 #include "expr2cpp.h"
33 
35  const symbolt &symb,
36  const irep_idt &base_name,
37  irep_idt &identifier)
38 {
39  for(const auto &b : to_struct_type(symb.type).bases())
40  {
41  const irep_idt &id = b.type().get_identifier();
42  if(lookup(id).base_name == base_name)
43  {
44  identifier = id;
45  return true;
46  }
47  }
48 
49  return false;
50 }
51 
54 {
55  if(expr.id()==ID_cpp_name)
57  else if(expr.id()=="cpp-this")
58  typecheck_expr_this(expr);
59  else if(expr.id() == ID_pointer_to_member)
60  convert_pmop(expr);
61  else if(expr.id() == ID_new_object)
62  {
63  }
64  else if(operator_is_overloaded(expr))
65  {
66  }
67  else if(expr.id()=="explicit-typecast")
69  else if(expr.id()=="explicit-constructor-call")
71  else if(expr.id()==ID_code)
72  {
73 #ifdef DEBUG
74  std::cerr << "E: " << expr.pretty() << '\n';
75  std::cerr << "cpp_typecheckt::typecheck_expr_main got code\n";
76 #endif
78  }
79  else if(expr.id()==ID_symbol)
80  {
81  // ignore here
82 #ifdef DEBUG
83  std::cerr << "E: " << expr.pretty() << '\n';
84  std::cerr << "cpp_typecheckt::typecheck_expr_main got symbol\n";
85 #endif
86  }
87  else if(expr.id()=="__is_base_of")
88  {
89  // an MS extension
90  // http://msdn.microsoft.com/en-us/library/ms177194(v=vs.80).aspx
91 
92  typet base=static_cast<const typet &>(expr.find("type_arg1"));
93  typet deriv=static_cast<const typet &>(expr.find("type_arg2"));
94 
95  typecheck_type(base);
96  typecheck_type(deriv);
97 
98  base = follow(base);
99  deriv = follow(deriv);
100 
101  if(base.id()!=ID_struct || deriv.id()!=ID_struct)
102  expr=false_exprt();
103  else
104  {
105  irep_idt base_name=base.get(ID_name);
106  const class_typet &class_type=to_class_type(deriv);
107 
108  if(class_type.has_base(base_name))
109  expr=true_exprt();
110  else
111  expr=false_exprt();
112  }
113  }
114  else if(expr.id()==ID_msc_uuidof)
115  {
116  // these appear to have type "struct _GUID"
117  // and they are lvalues!
118  expr.type() = struct_tag_typet("tag-_GUID");
119  expr.set(ID_C_lvalue, true);
120  }
121  else if(expr.id()==ID_noexcept)
122  {
123  // TODO
124  expr=false_exprt();
125  }
126  else if(expr.id()==ID_initializer_list)
127  {
128  expr.type().id(ID_initializer_list);
129  }
130  else
132 }
133 
135 {
136  assert(expr.operands().size()==3);
137 
138  implicit_typecast(expr.op0(), bool_typet());
139 
140  if(expr.op1().type().id()==ID_empty ||
141  expr.op1().type().id()==ID_empty)
142  {
143  if(expr.op1().get_bool(ID_C_lvalue))
144  {
145  exprt e1(expr.op1());
147  {
149  error() << "error: lvalue to rvalue conversion" << eom;
150  throw 0;
151  }
152  }
153 
154  if(expr.op1().type().id()==ID_array)
155  {
156  exprt e1(expr.op1());
158  {
160  error() << "error: array to pointer conversion" << eom;
161  throw 0;
162  }
163  }
164 
165  if(expr.op1().type().id()==ID_code)
166  {
167  exprt e1(expr.op1());
169  {
171  error() << "error: function to pointer conversion" << eom;
172  throw 0;
173  }
174  }
175 
176  if(expr.op2().get_bool(ID_C_lvalue))
177  {
178  exprt e2(expr.op2());
180  {
182  error() << "error: lvalue to rvalue conversion" << eom;
183  throw 0;
184  }
185  }
186 
187  if(expr.op2().type().id()==ID_array)
188  {
189  exprt e2(expr.op2());
191  {
193  error() << "error: array to pointer conversion" << eom;
194  throw 0;
195  }
196  }
197 
198  if(expr.op2().type().id()==ID_code)
199  {
200  exprt e2(expr.op2());
202  {
204  error() << "error: function to pointer conversion" << eom;
205  throw 0;
206  }
207  }
208 
209  if(expr.op1().get(ID_statement)==ID_throw &&
210  expr.op2().get(ID_statement)!=ID_throw)
211  expr.type()=expr.op2().type();
212  else if(expr.op2().get(ID_statement)==ID_throw &&
213  expr.op1().get(ID_statement)!=ID_throw)
214  expr.type()=expr.op1().type();
215  else if(expr.op1().type().id()==ID_empty &&
216  expr.op2().type().id()==ID_empty)
217  expr.type() = void_type();
218  else
219  {
221  error() << "error: bad types for operands" << eom;
222  throw 0;
223  }
224  return;
225  }
226 
227  if(expr.op1().type() == expr.op2().type())
228  {
229  c_qualifierst qual1, qual2;
230  qual1.read(expr.op1().type());
231  qual2.read(expr.op2().type());
232 
233  if(qual1.is_subset_of(qual2))
234  expr.type()=expr.op1().type();
235  else
236  expr.type()=expr.op2().type();
237  }
238  else
239  {
240  exprt e1=expr.op1();
241  exprt e2=expr.op2();
242 
243  if(implicit_conversion_sequence(expr.op1(), expr.op2().type(), e1))
244  {
245  expr.type()=e1.type();
246  expr.op1().swap(e1);
247  }
248  else if(implicit_conversion_sequence(expr.op2(), expr.op1().type(), e2))
249  {
250  expr.type()=e2.type();
251  expr.op2().swap(e2);
252  }
253  else if(expr.op1().type().id()==ID_array &&
254  expr.op2().type().id()==ID_array &&
255  expr.op1().type().subtype() == expr.op2().type().subtype())
256  {
257  // array-to-pointer conversion
258 
259  index_exprt index1(expr.op1(), from_integer(0, index_type()));
260 
261  index_exprt index2(expr.op2(), from_integer(0, index_type()));
262 
263  address_of_exprt addr1(index1);
264  address_of_exprt addr2(index2);
265 
266  expr.op1()=addr1;
267  expr.op2()=addr2;
268  expr.type()=addr1.type();
269  return;
270  }
271  else
272  {
274  error() << "error: types are incompatible.\n"
275  << "I got '" << type2cpp(expr.op1().type(), *this) << "' and '"
276  << type2cpp(expr.op2().type(), *this) << "'." << eom;
277  throw 0;
278  }
279  }
280 
281  if(expr.op1().get_bool(ID_C_lvalue) &&
282  expr.op2().get_bool(ID_C_lvalue))
283  expr.set(ID_C_lvalue, true);
284 
285  return;
286 }
287 
289 {
291  expr,
293 }
294 
296 {
297  // We need to overload, "sizeof-expression" can be mis-parsed
298  // as a type.
299 
300  if(expr.operands().empty())
301  {
302  const typet &type=
303  static_cast<const typet &>(expr.find(ID_type_arg));
304 
305  if(type.id()==ID_cpp_name)
306  {
307  // sizeof(X) may be ambiguous -- X can be either a type or
308  // an expression.
309 
310  cpp_typecheck_fargst fargs;
311 
312  exprt symbol_expr=resolve(
313  to_cpp_name(static_cast<const irept &>(type)),
315  fargs);
316 
317  if(symbol_expr.id()!=ID_type)
318  {
319  expr.copy_to_operands(symbol_expr);
320  expr.remove(ID_type_arg);
321  }
322  }
323  else if(type.id()==ID_array)
324  {
325  // sizeof(expr[index]) can be parsed as an array type!
326 
327  if(type.subtype().id()==ID_cpp_name)
328  {
329  cpp_typecheck_fargst fargs;
330 
331  exprt symbol_expr=resolve(
332  to_cpp_name(static_cast<const irept &>(type.subtype())),
334  fargs);
335 
336  if(symbol_expr.id()!=ID_type)
337  {
338  // _NOT_ a type
339  index_exprt index_expr(symbol_expr, to_array_type(type).size());
340  expr.copy_to_operands(index_expr);
341  expr.remove(ID_type_arg);
342  }
343  }
344  }
345  }
346 
348 }
349 
351 {
353 }
354 
356  exprt &expr,
357  const cpp_typecheck_fargst &fargs)
358 {
359  if(expr.id()==ID_cpp_name)
360  typecheck_expr_cpp_name(expr, fargs);
361  else if(expr.id()==ID_member)
362  {
364  typecheck_expr_member(expr, fargs);
365  }
366  else if(expr.id()==ID_ptrmember)
367  {
370 
371  // is operator-> overloaded?
372  if(to_unary_expr(expr).op().type().id() != ID_pointer)
373  {
374  std::string op_name="operator->";
375 
376  // turn this into a function call
377  // first do function/operator
378  const cpp_namet cpp_name(op_name, expr.source_location());
379 
380  side_effect_expr_function_callt function_call(
381  cpp_name.as_expr(),
382  {to_unary_expr(expr).op()},
384  expr.source_location());
385  function_call.arguments().reserve(expr.operands().size());
386 
388 
390 
391  to_unary_expr(expr).op().swap(function_call);
392  typecheck_function_expr(expr, fargs);
393  return;
394  }
395 
396  typecheck_expr_ptrmember(expr, fargs);
397  }
398  else
399  typecheck_expr(expr);
400 }
401 
403 {
404  // at least one argument must have class or enumerated type
405 
406  forall_operands(it, expr)
407  {
408  typet t = it->type();
409 
410  if(is_reference(t))
411  t=t.subtype();
412 
413  if(
414  t.id() == ID_struct || t.id() == ID_union || t.id() == ID_c_enum ||
415  t.id() == ID_c_enum_tag || t.id() == ID_struct_tag ||
416  t.id() == ID_union_tag)
417  {
418  return true;
419  }
420  }
421 
422  return false;
423 }
424 
426 {
427  const irep_idt id;
428  const char *op_name;
429 } const operators[] =
430 {
431  { ID_plus, "+" },
432  { ID_minus, "-" },
433  { ID_mult, "*" },
434  { ID_div, "/" },
435  { ID_bitnot, "~" },
436  { ID_bitand, "&" },
437  { ID_bitor, "|" },
438  { ID_bitxor, "^" },
439  { ID_not, "!" },
440  { ID_unary_minus, "-" },
441  { ID_and, "&&" },
442  { ID_or, "||" },
443  { ID_not, "!" },
444  { ID_index, "[]" },
445  { ID_equal, "==" },
446  { ID_lt, "<"},
447  { ID_le, "<="},
448  { ID_gt, ">"},
449  { ID_ge, ">="},
450  { ID_shl, "<<"},
451  { ID_shr, ">>"},
452  { ID_notequal, "!=" },
453  { ID_dereference, "*" },
454  { ID_ptrmember, "->" },
455  { irep_idt(), nullptr }
456 };
457 
459 {
460  // Check argument types first.
461  // At least one struct/enum operand is required.
462 
463  if(!overloadable(expr))
464  return false;
465  else if(expr.id()==ID_dereference &&
466  expr.get_bool(ID_C_implicit))
467  return false;
468 
469  assert(expr.operands().size()>=1);
470 
471  if(expr.id()=="explicit-typecast")
472  {
473  // the cast operator can be overloaded
474 
475  typet t=expr.type();
476  typecheck_type(t);
477  std::string op_name=std::string("operator")+"("+cpp_type2name(t)+")";
478 
479  // turn this into a function call
480  const cpp_namet cpp_name(op_name, expr.source_location());
481 
482  // See if the struct declares the cast operator as a member
483  bool found_in_struct=false;
484  assert(!expr.operands().empty());
485  typet t0(follow(to_unary_expr(expr).op().type()));
486 
487  if(t0.id()==ID_struct)
488  {
489  for(const auto &c : to_struct_type(t0).components())
490  {
491  if(!c.get_bool(ID_from_base) && c.get_base_name() == op_name)
492  {
493  found_in_struct=true;
494  break;
495  }
496  }
497  }
498 
499  if(!found_in_struct)
500  return false;
501 
502  exprt member(ID_member);
503  member.add(ID_component_cpp_name) = cpp_name;
504 
505  member.copy_to_operands(
507 
508  side_effect_expr_function_callt function_call(
509  std::move(member), {}, uninitialized_typet{}, expr.source_location());
510  function_call.arguments().reserve(expr.operands().size());
511 
512  if(expr.operands().size()>1)
513  {
514  for(exprt::operandst::const_iterator
515  it=(expr.operands().begin()+1);
516  it!=(expr).operands().end();
517  it++)
518  function_call.arguments().push_back(*it);
519  }
520 
522 
523  if(expr.id()==ID_ptrmember)
524  {
525  add_implicit_dereference(function_call);
527  to_unary_expr(expr).op().swap(function_call);
528  typecheck_expr(expr);
529  return true;
530  }
531 
532  expr.swap(function_call);
533  return true;
534  }
535 
536  for(const operator_entryt *e=operators;
537  !e->id.empty();
538  e++)
539  {
540  if(expr.id()==e->id)
541  {
542  if(expr.id()==ID_dereference)
543  assert(!expr.get_bool(ID_C_implicit));
544 
545  std::string op_name=std::string("operator")+e->op_name;
546 
547  // first do function/operator
548  const cpp_namet cpp_name(op_name, expr.source_location());
549 
550  // turn this into a function call
551  // There are two options to overload an operator:
552  //
553  // 1. In the scope of a as a.operator(b, ...)
554  // 2. Anywhere in scope as operator(a, b, ...)
555  //
556  // Using both is not allowed.
557  //
558  // We try and fail silently, maybe conversions will work
559  // instead.
560 
561  // TODO: need to resolve an incomplete struct (template) here
562  // go into scope of first operand
563  if(
564  to_multi_ary_expr(expr).op0().type().id() == ID_struct_tag &&
565  follow(to_multi_ary_expr(expr).op0().type()).id() == ID_struct)
566  {
567  const irep_idt &struct_identifier =
568  to_multi_ary_expr(expr).op0().type().get(ID_identifier);
569 
570  // get that scope
571  cpp_save_scopet save_scope(cpp_scopes);
572  cpp_scopes.set_scope(struct_identifier);
573 
574  // build fargs for resolver
575  cpp_typecheck_fargst fargs;
576  fargs.operands=expr.operands();
577  fargs.has_object=true;
578  fargs.in_use=true;
579 
580  // should really be a qualified search
581  exprt resolve_result=resolve(
582  cpp_name, cpp_typecheck_resolvet::wantt::VAR, fargs, false);
583 
584  if(resolve_result.is_not_nil())
585  {
586  // Found! We turn op(a, b, ...) into a.op(b, ...)
587  exprt member(ID_member);
588  member.add(ID_component_cpp_name) = cpp_name;
589 
590  member.copy_to_operands(
592 
593  side_effect_expr_function_callt function_call(
594  std::move(member),
595  {},
597  expr.source_location());
598  function_call.arguments().reserve(expr.operands().size());
599 
600  if(expr.operands().size()>1)
601  {
602  // skip first
603  for(exprt::operandst::const_iterator
604  it=expr.operands().begin()+1;
605  it!=expr.operands().end();
606  it++)
607  function_call.arguments().push_back(*it);
608  }
609 
611 
612  expr=function_call;
613 
614  return true;
615  }
616  }
617 
618  // 2nd option!
619  {
620  cpp_typecheck_fargst fargs;
621  fargs.operands=expr.operands();
622  fargs.has_object=false;
623  fargs.in_use=true;
624 
625  exprt resolve_result=resolve(
626  cpp_name, cpp_typecheck_resolvet::wantt::VAR, fargs, false);
627 
628  if(resolve_result.is_not_nil())
629  {
630  // found!
631  side_effect_expr_function_callt function_call(
632  cpp_name.as_expr(),
633  {},
635  expr.source_location());
636  function_call.arguments().reserve(expr.operands().size());
637 
638  // now do arguments
639  forall_operands(it, expr)
640  function_call.arguments().push_back(*it);
641 
643 
644  if(expr.id()==ID_ptrmember)
645  {
646  add_implicit_dereference(function_call);
648  to_multi_ary_expr(expr).op0() = function_call;
649  typecheck_expr(expr);
650  return true;
651  }
652 
653  expr=function_call;
654 
655  return true;
656  }
657  }
658  }
659  }
660 
661  return false;
662 }
663 
665 {
666  if(expr.operands().size()!=1)
667  {
669  error() << "address_of expects one operand" << eom;
670  throw 0;
671  }
672 
673  exprt &op = to_address_of_expr(expr).op();
674 
675  if(!op.get_bool(ID_C_lvalue) && expr.type().id()==ID_code)
676  {
678  error() << "expr not an lvalue" << eom;
679  throw 0;
680  }
681 
682  if(op.type().id() == ID_code)
683  {
684  // we take the address of the method.
685  DATA_INVARIANT(op.id() == ID_member, "address-of code must be a member");
686  exprt symb = cpp_symbol_expr(lookup(op.get(ID_component_name)));
687  address_of_exprt address(symb, pointer_type(symb.type()));
688  address.set(ID_C_implicit, true);
689  op.swap(address);
690  }
691 
692  if(op.id() == ID_address_of && op.get_bool(ID_C_implicit))
693  {
694  // must be the address of a function
695  code_typet &code_type=to_code_type(op.type().subtype());
696 
697  code_typet::parameterst &args=code_type.parameters();
698  if(!args.empty() && args.front().get_this())
699  {
700  // it's a pointer to member function
701  const struct_tag_typet symbol(code_type.get(ID_C_member_name));
702  op.type().add(ID_to_member) = symbol;
703 
704  if(code_type.get_bool(ID_C_is_virtual))
705  {
707  error() << "error: pointers to virtual methods"
708  << " are currently not implemented" << eom;
709  throw 0;
710  }
711  }
712  }
713  else if(op.id() == ID_ptrmember && to_unary_expr(op).op().id() == "cpp-this")
714  {
715  expr.type() = pointer_type(op.type());
716  expr.type().add(ID_to_member) = to_unary_expr(op).op().type().subtype();
717  return;
718  }
719 
720  // the C front end does not know about references
721  const bool is_ref=is_reference(expr.type());
723  if(is_ref)
724  expr.type()=reference_type(expr.type().subtype());
725 }
726 
728 {
729  expr.type() = void_type();
730 
731  assert(expr.operands().size()==1 ||
732  expr.operands().empty());
733 
734  if(expr.operands().size()==1)
735  {
736  // nothing really to do; one can throw _almost_ anything
737  const typet &exception_type = to_unary_expr(expr).op().type();
738 
739  if(exception_type.id() == ID_empty)
740  {
742  error() << "cannot throw void" << eom;
743  throw 0;
744  }
745 
746  // annotate the relevant exception IDs
747  expr.set(ID_exception_list,
748  cpp_exception_list(exception_type, *this));
749  }
750 }
751 
753 {
754  // next, find out if we do an array
755 
756  if(expr.type().id()==ID_array)
757  {
758  // first typecheck subtype
759  typecheck_type(expr.type().subtype());
760 
761  // typecheck the size
762  exprt &size=to_array_type(expr.type()).size();
763  typecheck_expr(size);
764 
765  bool size_is_unsigned=(size.type().id()==ID_unsignedbv);
766  bitvector_typet integer_type(
767  size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width);
768  implicit_typecast(size, integer_type);
769 
770  expr.set(ID_statement, ID_cpp_new_array);
771 
772  // save the size expression
773  expr.set(ID_size, to_array_type(expr.type()).size());
774 
775  // new actually returns a pointer, not an array
776  pointer_typet ptr_type=
777  pointer_type(expr.type().subtype());
778  expr.type().swap(ptr_type);
779  }
780  else
781  {
782  // first typecheck type
783  typecheck_type(expr.type());
784 
785  expr.set(ID_statement, ID_cpp_new);
786 
787  pointer_typet ptr_type=pointer_type(expr.type());
788  expr.type().swap(ptr_type);
789  }
790 
791  exprt object_expr(ID_new_object, expr.type().subtype());
792  object_expr.set(ID_C_lvalue, true);
793 
795 
796  // not yet typechecked-stuff
797  exprt &initializer=static_cast<exprt &>(expr.add(ID_initializer));
798 
799  // arrays must not have an initializer
800  if(!initializer.operands().empty() &&
801  expr.get(ID_statement)==ID_cpp_new_array)
802  {
805  error() << "new with array type must not use initializer" << eom;
806  throw 0;
807  }
808 
809  auto code = cpp_constructor(
810  expr.find_source_location(), object_expr, initializer.operands());
811 
812  if(code.has_value())
813  expr.add(ID_initializer).swap(code.value());
814  else
815  expr.add(ID_initializer) = nil_exprt();
816 
817  // we add the size of the object for convenience of the
818  // runtime library
819  auto size_of_opt = size_of_expr(expr.type().subtype(), *this);
820 
821  if(size_of_opt.has_value())
822  {
823  auto &sizeof_expr = static_cast<exprt &>(expr.add(ID_sizeof));
824  sizeof_expr = size_of_opt.value();
825  sizeof_expr.add(ID_C_c_sizeof_type) = expr.type().subtype();
826  }
827 }
828 
830 {
831  exprt result;
832 
833  if(src.id()==ID_comma)
834  {
835  assert(src.operands().size()==2);
836  result = collect_comma_expression(to_binary_expr(src).op0());
837  result.copy_to_operands(to_binary_expr(src).op1());
838  }
839  else
840  result.copy_to_operands(src);
841 
842  return result;
843 }
844 
846 {
847  // these can have 0 or 1 arguments
848 
849  if(expr.operands().empty())
850  {
851  // Default value, e.g., int()
852  typecheck_type(expr.type());
853  auto new_expr =
854  ::zero_initializer(expr.type(), expr.find_source_location(), *this);
855  if(!new_expr.has_value())
856  {
858  error() << "cannot zero-initialize '" << to_string(expr.type()) << "'"
859  << eom;
860  throw 0;
861  }
862 
863  new_expr->add_source_location() = expr.source_location();
864  expr = *new_expr;
865  }
866  else if(expr.operands().size()==1)
867  {
868  auto &op = to_unary_expr(expr).op();
869 
870  // Explicitly given value, e.g., int(1).
871  // There is an expr-vs-type ambiguity, as it is possible to write
872  // (f)(1), where 'f' is a function symbol and not a type.
873  // This also exists with a "comma expression", e.g.,
874  // (f)(1, 2, 3)
875 
876  if(expr.type().id()==ID_cpp_name)
877  {
878  // try to resolve as type
879  cpp_typecheck_fargst fargs;
880 
881  exprt symbol_expr=resolve(
882  to_cpp_name(static_cast<const irept &>(expr.type())),
884  fargs,
885  false); // fail silently
886 
887  if(symbol_expr.id()==ID_type)
888  expr.type()=symbol_expr.type();
889  else
890  {
891  // It's really a function call. Note that multiple arguments
892  // become a comma expression, and that these are already typechecked.
894  static_cast<const exprt &>(static_cast<const irept &>(expr.type())),
895  collect_comma_expression(op).operands(),
897  expr.source_location());
898 
900 
901  expr.swap(f_call);
902  return;
903  }
904  }
905  else
906  typecheck_type(expr.type());
907 
908  // We allow (TYPE){ initializer_list }
909  // This is called "compound literal", and is syntactic
910  // sugar for a (possibly local) declaration.
911  if(op.id() == ID_initializer_list)
912  {
913  // just do a normal initialization
914  do_initializer(op, expr.type(), false);
915 
916  // This produces a struct-expression,
917  // union-expression, array-expression,
918  // or an expression for a pointer or scalar.
919  // We produce a compound_literal expression.
920  exprt tmp(ID_compound_literal, expr.type());
921  tmp.add_to_operands(std::move(op));
922  expr=tmp;
923  expr.set(ID_C_lvalue, true); // these are l-values
924  return;
925  }
926 
927  exprt new_expr;
928 
929  if(
930  const_typecast(op, expr.type(), new_expr) ||
931  static_typecast(op, expr.type(), new_expr, false) ||
932  reinterpret_typecast(op, expr.type(), new_expr, false))
933  {
934  expr=new_expr;
936  }
937  else
938  {
940  error() << "invalid explicit cast:\n"
941  << "operand type: '" << to_string(op.type()) << "'\n"
942  << "casting to: '" << to_string(expr.type()) << "'" << eom;
943  throw 0;
944  }
945  }
946  else
947  {
949  error() << "explicit typecast expects 0 or 1 operands" << eom;
950  throw 0;
951  }
952 }
953 
955 {
956  typecheck_type(expr.type());
957 
958  if(cpp_is_pod(expr.type()))
959  {
960  expr.id("explicit-typecast");
961  typecheck_expr_main(expr);
962  }
963  else
964  {
965  assert(expr.type().id()==ID_struct);
966 
967  struct_tag_typet tag(expr.type().get(ID_name));
968  tag.add_source_location() = expr.source_location();
969 
970  exprt e=expr;
971  new_temporary(e.source_location(), tag, e.operands(), expr);
972  }
973 }
974 
976 {
978  {
980  error() << "`this' is not allowed here" << eom;
981  throw 0;
982  }
983 
984  const exprt &this_expr=cpp_scopes.current_scope().this_expr;
985  const source_locationt source_location=expr.find_source_location();
986 
987  assert(this_expr.is_not_nil());
988  assert(this_expr.type().id()==ID_pointer);
989 
990  expr=this_expr;
991  expr.add_source_location()=source_location;
992 }
993 
995 {
996  if(expr.operands().size()!=1)
997  {
999  error() << "delete expects one operand" << eom;
1000  throw 0;
1001  }
1002 
1003  const irep_idt statement=expr.get(ID_statement);
1004 
1005  if(statement==ID_cpp_delete)
1006  {
1007  }
1008  else if(statement==ID_cpp_delete_array)
1009  {
1010  }
1011  else
1012  UNREACHABLE;
1013 
1014  typet pointer_type = to_unary_expr(expr).op().type();
1015 
1016  if(pointer_type.id()!=ID_pointer)
1017  {
1019  error() << "delete takes a pointer type operand, but got '"
1020  << to_string(pointer_type) << "'" << eom;
1021  throw 0;
1022  }
1023 
1024  // remove any const-ness of the argument
1025  // (which would impair the call to the destructor)
1026  pointer_type.subtype().remove(ID_C_constant);
1027 
1028  // delete expressions are always void
1029  expr.type()=typet(ID_empty);
1030 
1031  // we provide the right destructor, for the convenience
1032  // of later stages
1033  exprt new_object(ID_new_object, pointer_type.subtype());
1034  new_object.add_source_location()=expr.source_location();
1035  new_object.set(ID_C_lvalue, true);
1036 
1038 
1039  auto destructor_code = cpp_destructor(expr.source_location(), new_object);
1040 
1041  if(destructor_code.has_value())
1042  {
1043  // this isn't typechecked yet
1044  typecheck_code(destructor_code.value());
1045  expr.set(ID_destructor, destructor_code.value());
1046  }
1047  else
1048  expr.set(ID_destructor, nil_exprt());
1049 }
1050 
1052 {
1053  // should not be called
1054  #if 0
1055  std::cout << "E: " << expr.pretty() << '\n';
1056  UNREACHABLE;
1057  #endif
1058 }
1059 
1061  exprt &expr,
1062  const cpp_typecheck_fargst &fargs)
1063 {
1064  if(expr.operands().size()!=1)
1065  {
1067  error() << "error: member operator expects one operand" << eom;
1068  throw 0;
1069  }
1070 
1071  exprt &op0 = to_unary_expr(expr).op();
1073 
1074  // The notation for explicit calls to destructors can be used regardless
1075  // of whether the type defines a destructor. This allows you to make such
1076  // explicit calls without knowing if a destructor is defined for the type.
1077  // An explicit call to a destructor where none is defined has no effect.
1078 
1079  if(
1080  expr.find(ID_component_cpp_name).is_not_nil() &&
1081  to_cpp_name(expr.find(ID_component_cpp_name)).is_destructor() &&
1082  op0.type().id() != ID_struct && op0.type().id() != ID_struct_tag)
1083  {
1084  exprt tmp(ID_cpp_dummy_destructor);
1085  tmp.add_source_location()=expr.source_location();
1086  expr.swap(tmp);
1087  return;
1088  }
1089 
1090  // The member operator will trigger template elaboration
1092 
1093  const typet &followed_op0_type=follow(op0.type());
1094 
1095  if(followed_op0_type.id()!=ID_struct &&
1096  followed_op0_type.id()!=ID_union)
1097  {
1099  error() << "error: member operator requires struct/union type "
1100  << "on left hand side but got '" << to_string(followed_op0_type)
1101  << "'" << eom;
1102  throw 0;
1103  }
1104 
1105  const struct_union_typet &type=
1106  to_struct_union_type(followed_op0_type);
1107 
1108  if(type.is_incomplete())
1109  {
1111  error() << "error: member operator got incomplete type "
1112  << "on left hand side" << eom;
1113  throw 0;
1114  }
1115 
1116  irep_idt struct_identifier=type.get(ID_name);
1117 
1118  if(expr.find(ID_component_cpp_name).is_not_nil())
1119  {
1120  cpp_namet component_cpp_name=
1121  to_cpp_name(expr.find(ID_component_cpp_name));
1122 
1123  // go to the scope of the struct/union
1124  cpp_save_scopet save_scope(cpp_scopes);
1125  cpp_scopes.set_scope(struct_identifier);
1126 
1127  // resolve the member name in this scope
1128  cpp_typecheck_fargst new_fargs(fargs);
1129  new_fargs.add_object(op0);
1130 
1131  exprt symbol_expr=resolve(
1132  component_cpp_name,
1134  new_fargs);
1135 
1136  if(symbol_expr.id()==ID_dereference)
1137  {
1138  assert(symbol_expr.get_bool(ID_C_implicit));
1139  exprt tmp = to_dereference_expr(symbol_expr).pointer();
1140  symbol_expr.swap(tmp);
1141  }
1142 
1143  assert(symbol_expr.id()==ID_symbol ||
1144  symbol_expr.id()==ID_member ||
1145  symbol_expr.id()==ID_constant);
1146 
1147  // If it is a symbol or a constant, just return it!
1148  // Note: the resolver returns a symbol if the member
1149  // is static or if it is a constructor.
1150 
1151  if(symbol_expr.id()==ID_symbol)
1152  {
1153  if(
1154  symbol_expr.type().id() == ID_code &&
1155  to_code_type(symbol_expr.type()).return_type().id() == ID_constructor)
1156  {
1158  error() << "error: member '"
1159  << lookup(symbol_expr.get(ID_identifier)).base_name
1160  << "' is a constructor" << eom;
1161  throw 0;
1162  }
1163  else
1164  {
1165  // it must be a static component
1166  const struct_typet::componentt &pcomp =
1167  type.get_component(to_symbol_expr(symbol_expr).get_identifier());
1168 
1169  if(pcomp.is_nil())
1170  {
1172  error() << "error: '" << symbol_expr.get(ID_identifier)
1173  << "' is not static member "
1174  << "of class '" << to_string(op0.type()) << "'" << eom;
1175  throw 0;
1176  }
1177  }
1178 
1179  expr=symbol_expr;
1180  return;
1181  }
1182  else if(symbol_expr.id()==ID_constant)
1183  {
1184  expr=symbol_expr;
1185  return;
1186  }
1187 
1188  const irep_idt component_name=symbol_expr.get(ID_component_name);
1189 
1190  expr.remove(ID_component_cpp_name);
1191  expr.set(ID_component_name, component_name);
1192  }
1193 
1194  const irep_idt &component_name=expr.get(ID_component_name);
1195  INVARIANT(!component_name.empty(), "component name should not be empty");
1196 
1197  exprt component;
1198  component.make_nil();
1199 
1200  PRECONDITION(
1201  op0.type().id() == ID_struct || op0.type().id() == ID_union ||
1202  op0.type().id() == ID_struct_tag || op0.type().id() == ID_union_tag);
1203 
1204  exprt member;
1205 
1206  if(get_component(expr.source_location(), op0, component_name, member))
1207  {
1208  // because of possible anonymous members
1209  expr.swap(member);
1210  }
1211  else
1212  {
1214  error() << "error: member '" << component_name << "' of '"
1215  << to_string(type) << "' not found" << eom;
1216  throw 0;
1217  }
1218 
1220 
1221  if(expr.type().id()==ID_code)
1222  {
1223  // Check if the function body has to be typechecked
1224  symbol_tablet::symbolst::const_iterator it=
1225  symbol_table.symbols.find(component_name);
1226 
1227  assert(it!=symbol_table.symbols.end());
1228 
1229  if(it->second.value.id() == ID_cpp_not_typechecked)
1230  symbol_table.get_writeable_ref(component_name)
1231  .value.set(ID_is_used, true);
1232  }
1233 }
1234 
1236  exprt &expr,
1237  const cpp_typecheck_fargst &fargs)
1238 {
1239  assert(expr.id()==ID_ptrmember);
1240 
1241  if(expr.operands().size()!=1)
1242  {
1244  error() << "error: ptrmember operator expects one operand" << eom;
1245  throw 0;
1246  }
1247 
1248  auto &op = to_unary_expr(expr).op();
1249 
1251 
1252  if(op.type().id() != ID_pointer)
1253  {
1255  error() << "error: ptrmember operator requires pointer type "
1256  << "on left hand side, but got '" << to_string(op.type()) << "'"
1257  << eom;
1258  throw 0;
1259  }
1260 
1261  exprt tmp;
1262  op.swap(tmp);
1263 
1264  op.id(ID_dereference);
1265  op.add_to_operands(std::move(tmp));
1266  op.add_source_location()=expr.source_location();
1268 
1269  expr.id(ID_member);
1270  typecheck_expr_member(expr, fargs);
1271 }
1272 
1274 {
1277 
1278  if(e.arguments().size() != 1)
1279  {
1281  error() << "cast expressions expect one operand" << eom;
1282  throw 0;
1283  }
1284 
1285  exprt &f_op=e.function();
1286  exprt &cast_op=e.arguments().front();
1287 
1288  add_implicit_dereference(cast_op);
1289 
1290  const irep_idt &id=
1291  f_op.get_sub().front().get(ID_identifier);
1292 
1293  if(f_op.get_sub().size()!=2 ||
1294  f_op.get_sub()[1].id()!=ID_template_args)
1295  {
1297  error() << id << " expects template argument" << eom;
1298  throw 0;
1299  }
1300 
1301  irept &template_arguments=f_op.get_sub()[1].add(ID_arguments);
1302 
1303  if(template_arguments.get_sub().size()!=1)
1304  {
1306  error() << id << " expects one template argument" << eom;
1307  throw 0;
1308  }
1309 
1310  irept &template_arg=template_arguments.get_sub().front();
1311 
1312  if(template_arg.id() != ID_type && template_arg.id() != ID_ambiguous)
1313  {
1315  error() << id << " expects a type as template argument" << eom;
1316  throw 0;
1317  }
1318 
1319  typet &type=static_cast<typet &>(
1320  template_arguments.get_sub().front().add(ID_type));
1321 
1322  typecheck_type(type);
1323 
1324  source_locationt source_location=expr.source_location();
1325 
1326  exprt new_expr;
1327  if(id==ID_const_cast)
1328  {
1329  if(!const_typecast(cast_op, type, new_expr))
1330  {
1332  error() << "type mismatch on const_cast:\n"
1333  << "operand type: '" << to_string(cast_op.type()) << "'\n"
1334  << "cast type: '" << to_string(type) << "'" << eom;
1335  throw 0;
1336  }
1337  }
1338  else if(id==ID_dynamic_cast)
1339  {
1340  if(!dynamic_typecast(cast_op, type, new_expr))
1341  {
1343  error() << "type mismatch on dynamic_cast:\n"
1344  << "operand type: '" << to_string(cast_op.type()) << "'\n"
1345  << "cast type: '" << to_string(type) << "'" << eom;
1346  throw 0;
1347  }
1348  }
1349  else if(id==ID_reinterpret_cast)
1350  {
1351  if(!reinterpret_typecast(cast_op, type, new_expr))
1352  {
1354  error() << "type mismatch on reinterpret_cast:\n"
1355  << "operand type: '" << to_string(cast_op.type()) << "'\n"
1356  << "cast type: '" << to_string(type) << "'" << eom;
1357  throw 0;
1358  }
1359  }
1360  else if(id==ID_static_cast)
1361  {
1362  if(!static_typecast(cast_op, type, new_expr))
1363  {
1365  error() << "type mismatch on static_cast:\n"
1366  << "operand type: '" << to_string(cast_op.type()) << "'\n"
1367  << "cast type: '" << to_string(type) << "'" << eom;
1368  throw 0;
1369  }
1370  }
1371  else
1372  UNREACHABLE;
1373 
1374  expr.swap(new_expr);
1375 }
1376 
1378  exprt &expr,
1379  const cpp_typecheck_fargst &fargs)
1380 {
1381  source_locationt source_location=
1382  to_cpp_name(expr).source_location();
1383 
1384  if(expr.get_sub().size()==1 &&
1385  expr.get_sub()[0].id()==ID_name)
1386  {
1387  const irep_idt identifier=expr.get_sub()[0].get(ID_identifier);
1388 
1389  if(
1390  auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
1391  identifier, fargs.operands, source_location))
1392  {
1393  expr = std::move(*gcc_polymorphic);
1394  return;
1395  }
1396  }
1397 
1398  for(std::size_t i=0; i<expr.get_sub().size(); i++)
1399  {
1400  if(expr.get_sub()[i].id()==ID_cpp_name)
1401  {
1402  typet &type=static_cast<typet &>(expr.get_sub()[i]);
1403  typecheck_type(type);
1404 
1405  std::string tmp="("+cpp_type2name(type)+")";
1406 
1407  typet name(ID_name);
1408  name.set(ID_identifier, tmp);
1409  name.add_source_location()=source_location;
1410 
1411  type=name;
1412  }
1413  }
1414 
1415  if(expr.get_sub().size()>=1 &&
1416  expr.get_sub().front().id()==ID_name)
1417  {
1418  const irep_idt &id=expr.get_sub().front().get(ID_identifier);
1419 
1420  if(id==ID_const_cast ||
1421  id==ID_dynamic_cast ||
1422  id==ID_reinterpret_cast ||
1423  id==ID_static_cast)
1424  {
1425  expr.id(ID_cast_expression);
1426  return;
1427  }
1428  }
1429 
1430  exprt symbol_expr=
1431  resolve(
1432  to_cpp_name(expr),
1434  fargs);
1435 
1436  // we want VAR
1437  assert(symbol_expr.id()!=ID_type);
1438 
1439  if(symbol_expr.id()==ID_member)
1440  {
1441  if(
1442  symbol_expr.operands().empty() ||
1443  to_multi_ary_expr(symbol_expr).op0().is_nil())
1444  {
1445  if(to_code_type(symbol_expr.type()).return_type().id() != ID_constructor)
1446  {
1448  {
1449  if(symbol_expr.type().id()!=ID_code)
1450  {
1451  error().source_location=source_location;
1452  error() << "object missing" << eom;
1453  throw 0;
1454  }
1455 
1456  // may still be good for address of
1457  }
1458  else
1459  {
1460  // Try again
1461  exprt ptrmem(ID_ptrmember);
1462  ptrmem.operands().push_back(
1464 
1465  ptrmem.add(ID_component_cpp_name)=expr;
1466 
1467  ptrmem.add_source_location()=source_location;
1468  typecheck_expr_ptrmember(ptrmem, fargs);
1469  symbol_expr.swap(ptrmem);
1470  }
1471  }
1472  }
1473  }
1474 
1475  symbol_expr.add_source_location()=source_location;
1476  expr=symbol_expr;
1477 
1478  if(expr.id()==ID_symbol)
1480 
1482 }
1483 
1485 {
1486  if(is_reference(expr.type()))
1487  {
1488  // add implicit dereference
1489  dereference_exprt tmp(expr);
1490  tmp.set(ID_C_implicit, true);
1491  tmp.add_source_location()=expr.source_location();
1492  tmp.set(ID_C_lvalue, true);
1493  expr.swap(tmp);
1494  }
1495 }
1496 
1499 {
1500  // For virtual functions, it is important to check whether
1501  // the function name is qualified. If it is qualified, then
1502  // the call is not virtual.
1503  bool is_qualified=false;
1504 
1505  if(expr.function().id()==ID_member ||
1506  expr.function().id()==ID_ptrmember)
1507  {
1508  if(expr.function().get(ID_component_cpp_name)==ID_cpp_name)
1509  {
1510  const cpp_namet &cpp_name=
1511  to_cpp_name(expr.function().find(ID_component_cpp_name));
1512  is_qualified=cpp_name.is_qualified();
1513  }
1514  }
1515  else if(expr.function().id()==ID_cpp_name)
1516  {
1517  const cpp_namet &cpp_name=to_cpp_name(expr.function());
1518  is_qualified=cpp_name.is_qualified();
1519  }
1520 
1521  // Backup of the original operand
1522  exprt op0=expr.function();
1523 
1524  // now do the function -- this has been postponed
1526 
1527  if(expr.function().id() == ID_pod_constructor)
1528  {
1529  assert(expr.function().type().id()==ID_code);
1530 
1531  // This must be a POD.
1532  const typet &pod=to_code_type(expr.function().type()).return_type();
1533  assert(cpp_is_pod(pod));
1534 
1535  // These aren't really function calls, but either conversions or
1536  // initializations.
1537  if(expr.arguments().size() <= 1)
1538  {
1539  exprt typecast("explicit-typecast");
1540  typecast.type()=pod;
1541  typecast.add_source_location()=expr.source_location();
1542  if(!expr.arguments().empty())
1543  typecast.copy_to_operands(expr.arguments().front());
1545  expr.swap(typecast);
1546  }
1547  else
1548  {
1550  error() << "zero or one argument expected" << eom;
1551  throw 0;
1552  }
1553 
1554  return;
1555  }
1556  else if(expr.function().id() == ID_cast_expression)
1557  {
1558  // These are not really function calls,
1559  // but usually just type adjustments.
1560  typecheck_cast_expr(expr);
1562  return;
1563  }
1564  else if(expr.function().id() == ID_cpp_dummy_destructor)
1565  {
1566  // these don't do anything, e.g., (char*)->~char()
1568  expr.swap(no_op);
1569  return;
1570  }
1571 
1572  // look at type of function
1573 
1574  expr.function().type() = follow(expr.function().type());
1575 
1576  if(expr.function().type().id()==ID_pointer)
1577  {
1578  if(expr.function().type().find(ID_to_member).is_not_nil())
1579  {
1580  const exprt &bound =
1581  static_cast<const exprt &>(expr.function().type().find(ID_C_bound));
1582 
1583  if(bound.is_nil())
1584  {
1586  error() << "pointer-to-member not bound" << eom;
1587  throw 0;
1588  }
1589 
1590  // add `this'
1591  assert(bound.type().id()==ID_pointer);
1592  expr.arguments().insert(expr.arguments().begin(), bound);
1593 
1594  // we don't need the object any more
1595  expr.function().type().remove(ID_C_bound);
1596  }
1597 
1598  // do implicit dereference
1599  if(expr.function().id() == ID_address_of)
1600  {
1601  exprt tmp;
1602  tmp.swap(to_address_of_expr(expr.function()).object());
1603  expr.function().swap(tmp);
1604  }
1605  else
1606  {
1607  assert(expr.function().type().id()==ID_pointer);
1608  dereference_exprt tmp(expr.function());
1609  tmp.add_source_location() = expr.function().source_location();
1610  expr.function().swap(tmp);
1611  }
1612 
1613  if(expr.function().type().id()!=ID_code)
1614  {
1616  error() << "expecting code as argument" << eom;
1617  throw 0;
1618  }
1619  }
1620  else if(expr.function().type().id()==ID_code)
1621  {
1622  if(expr.function().type().get_bool(ID_C_is_virtual) && !is_qualified)
1623  {
1624  exprt vtptr_member;
1625  if(op0.id()==ID_member || op0.id()==ID_ptrmember)
1626  {
1627  vtptr_member.id(op0.id());
1628  vtptr_member.add_to_operands(std::move(to_unary_expr(op0).op()));
1629  }
1630  else
1631  {
1632  vtptr_member.id(ID_ptrmember);
1633  exprt this_expr("cpp-this");
1634  vtptr_member.add_to_operands(std::move(this_expr));
1635  }
1636 
1637  // get the virtual table
1638  typet this_type=
1639  to_code_type(expr.function().type()).parameters().front().type();
1640  irep_idt vtable_name=
1641  this_type.subtype().get_string(ID_identifier) +"::@vtable_pointer";
1642 
1643  const struct_typet &vt_struct=
1644  to_struct_type(follow(this_type.subtype()));
1645 
1646  const struct_typet::componentt &vt_compo=
1647  vt_struct.get_component(vtable_name);
1648 
1649  assert(vt_compo.is_not_nil());
1650 
1651  vtptr_member.set(ID_component_name, vtable_name);
1652 
1653  // look for the right entry
1654  irep_idt vtentry_component_name =
1655  vt_compo.type().subtype().get_string(ID_identifier) +
1656  "::" + expr.function().type().get_string(ID_C_virtual_name);
1657 
1658  exprt vtentry_member(ID_ptrmember);
1659  vtentry_member.copy_to_operands(vtptr_member);
1660  vtentry_member.set(ID_component_name, vtentry_component_name);
1661  typecheck_expr(vtentry_member);
1662 
1663  assert(vtentry_member.type().id()==ID_pointer);
1664 
1665  {
1666  dereference_exprt tmp(vtentry_member);
1667  tmp.add_source_location() = expr.function().source_location();
1668  vtentry_member.swap(tmp);
1669  }
1670 
1671  // Typecheck the expression as if it was not virtual
1672  // (add the this pointer)
1673 
1674  expr.type()=
1675  to_code_type(expr.function().type()).return_type();
1676 
1678 
1679  // Let's make the call virtual
1680  expr.function().swap(vtentry_member);
1681 
1684  return;
1685  }
1686  }
1687  else if(expr.function().type().id()==ID_struct)
1688  {
1689  const cpp_namet cppname("operator()", expr.source_location());
1690 
1691  exprt member(ID_member);
1692  member.add(ID_component_cpp_name)=cppname;
1693 
1694  member.add_to_operands(std::move(op0));
1695 
1696  expr.function().swap(member);
1698 
1699  return;
1700  }
1701  else
1702  {
1704  error() << "function call expects function or function "
1705  << "pointer as argument, but got '"
1706  << to_string(expr.function().type()) << "'" << eom;
1707  throw 0;
1708  }
1709 
1710  expr.type()=
1711  to_code_type(expr.function().type()).return_type();
1712 
1713  if(expr.type().id()==ID_constructor)
1714  {
1715  assert(expr.function().id() == ID_symbol);
1716 
1717  const code_typet::parameterst &parameters=
1718  to_code_type(expr.function().type()).parameters();
1719 
1720  assert(parameters.size()>=1);
1721 
1722  const typet &this_type=parameters[0].type();
1723 
1724  // change type from 'constructor' to object type
1725  expr.type()=this_type.subtype();
1726 
1727  // create temporary object
1728  side_effect_exprt tmp_object_expr(
1729  ID_temporary_object, this_type.subtype(), expr.source_location());
1730  tmp_object_expr.set(ID_C_lvalue, true);
1731  tmp_object_expr.set(ID_mode, ID_cpp);
1732 
1733  exprt member;
1734 
1735  exprt new_object(ID_new_object, tmp_object_expr.type());
1736  new_object.set(ID_C_lvalue, true);
1737 
1738  PRECONDITION(tmp_object_expr.type().id() == ID_struct_tag);
1739 
1741  new_object,
1742  expr.function().get(ID_identifier),
1743  member);
1744 
1745  // special case for the initialization of parents
1746  if(member.get_bool(ID_C_not_accessible))
1747  {
1748  PRECONDITION(!member.get(ID_C_access).empty());
1749  tmp_object_expr.set(ID_C_not_accessible, true);
1750  tmp_object_expr.set(ID_C_access, member.get(ID_C_access));
1751  }
1752 
1753  // the constructor is being used, so make sure the destructor
1754  // will be available
1755  {
1756  // find name of destructor
1757  const struct_typet::componentst &components=
1758  to_struct_type(follow(tmp_object_expr.type())).components();
1759 
1760  for(const auto &c : components)
1761  {
1762  const typet &type = c.type();
1763 
1764  if(
1765  !c.get_bool(ID_from_base) && type.id() == ID_code &&
1766  to_code_type(type).return_type().id() == ID_destructor)
1767  {
1769  break;
1770  }
1771  }
1772  }
1773 
1774  expr.function().swap(member);
1775 
1778 
1779  const code_expressiont new_code(expr);
1780  tmp_object_expr.add(ID_initializer)=new_code;
1781  expr.swap(tmp_object_expr);
1782  return;
1783  }
1784 
1785  assert(expr.operands().size()==2);
1786 
1787  if(expr.function().id()==ID_member)
1789  else
1790  {
1791  // for the object of a method call,
1792  // we are willing to add an "address_of"
1793  // for the sake of operator overloading
1794 
1795  const code_typet::parameterst &parameters =
1796  to_code_type(expr.function().type()).parameters();
1797 
1798  if(
1799  !parameters.empty() && parameters.front().get_this() &&
1800  !expr.arguments().empty())
1801  {
1802  const code_typet::parametert &parameter = parameters.front();
1803 
1804  exprt &operand = expr.arguments().front();
1805  INVARIANT(
1806  parameter.type().id() == ID_pointer,
1807  "`this' parameter should be a pointer");
1808 
1809  if(
1810  operand.type().id() != ID_pointer &&
1811  operand.type() == parameter.type().subtype())
1812  {
1813  address_of_exprt tmp(operand, pointer_type(operand.type()));
1814  tmp.add_source_location()=operand.source_location();
1815  operand=tmp;
1816  }
1817  }
1818  }
1819 
1820  assert(expr.operands().size()==2);
1821 
1823 
1824  assert(expr.operands().size()==2);
1825 
1827 
1828  // we will deal with some 'special' functions here
1829  exprt tmp=do_special_functions(expr);
1830  if(tmp.is_not_nil())
1831  expr.swap(tmp);
1832 }
1833 
1837 {
1838  exprt &f_op=expr.function();
1839  const code_typet &code_type=to_code_type(f_op.type());
1840  const code_typet::parameterst &parameters=code_type.parameters();
1841 
1842  // do default arguments
1843 
1844  if(parameters.size()>expr.arguments().size())
1845  {
1846  std::size_t i=expr.arguments().size();
1847 
1848  for(; i<parameters.size(); i++)
1849  {
1850  if(!parameters[i].has_default_value())
1851  break;
1852 
1853  const exprt &value=parameters[i].default_value();
1854  expr.arguments().push_back(value);
1855  }
1856  }
1857 
1858  exprt::operandst::iterator arg_it=expr.arguments().begin();
1859  for(const auto &parameter : parameters)
1860  {
1861  if(parameter.get_bool(ID_C_call_by_value))
1862  {
1863  assert(is_reference(parameter.type()));
1864 
1865  if(arg_it->id()!=ID_temporary_object)
1866  {
1867  // create a temporary for the parameter
1868 
1869  exprt temporary;
1870  new_temporary(
1871  arg_it->source_location(),
1872  parameter.type().subtype(),
1873  already_typechecked_exprt{*arg_it},
1874  temporary);
1875  arg_it->swap(temporary);
1876  }
1877  }
1878 
1879  ++arg_it;
1880  }
1881 
1883 }
1884 
1886  side_effect_exprt &expr)
1887 {
1888  const irep_idt &statement=expr.get(ID_statement);
1889 
1890  if(statement==ID_cpp_new ||
1891  statement==ID_cpp_new_array)
1892  {
1893  typecheck_expr_new(expr);
1894  }
1895  else if(statement==ID_cpp_delete ||
1896  statement==ID_cpp_delete_array)
1897  {
1898  typecheck_expr_delete(expr);
1899  }
1900  else if(statement==ID_preincrement ||
1901  statement==ID_predecrement ||
1902  statement==ID_postincrement ||
1903  statement==ID_postdecrement)
1904  {
1906  }
1907  else if(statement==ID_throw)
1908  {
1909  typecheck_expr_throw(expr);
1910  }
1911  else if(statement==ID_temporary_object)
1912  {
1913  // TODO
1914  }
1915  else
1917 }
1918 
1921 {
1922  assert(expr.operands().size()==2);
1923 
1924  assert(expr.function().id()==ID_member);
1925  assert(expr.function().operands().size()==1);
1926 
1927  // turn e.f(...) into xx::f(e, ...)
1928 
1929  exprt member_expr;
1930  member_expr.swap(expr.function());
1931 
1932  const symbolt &symbol=lookup(member_expr.get(ID_component_name));
1933  symbolt &method_symbol=symbol_table.get_writeable_ref(symbol.name);
1934  const symbolt &tag_symbol = lookup(symbol.type.get(ID_C_member_name));
1935 
1936  // build the right template map
1937  // if this is an instantiated template class method
1938  if(tag_symbol.type.find(ID_C_template)!=irept())
1939  {
1941  const irept &template_type = tag_symbol.type.find(ID_C_template);
1942  const irept &template_args = tag_symbol.type.find(ID_C_template_arguments);
1944  static_cast<const template_typet &>(template_type),
1945  static_cast<const cpp_template_args_tct &>(template_args));
1946  add_method_body(&method_symbol);
1947 #ifdef DEBUG
1948  std::cout << "MAP for " << symbol << ":\n";
1949  template_map.print(std::cout);
1950 #endif
1951  }
1952  else
1953  add_method_body(&method_symbol);
1954 
1955  // build new function expression
1956  exprt new_function(cpp_symbol_expr(symbol));
1957  new_function.add_source_location()=member_expr.source_location();
1958  expr.function().swap(new_function);
1959 
1960  if(!expr.function().type().get_bool(ID_C_is_static))
1961  {
1962  const code_typet &func_type=to_code_type(symbol.type);
1963  typet this_type=func_type.parameters().front().type();
1964 
1965  // Special case. Make it a reference.
1966  assert(this_type.id()==ID_pointer);
1967  this_type.set(ID_C_reference, true);
1968  this_type.set(ID_C_this, true);
1969 
1970  if(expr.arguments().size()==func_type.parameters().size())
1971  {
1972  // this might be set up for base-class initialisation
1973  if(
1974  expr.arguments().front().type() !=
1975  func_type.parameters().front().type())
1976  {
1977  implicit_typecast(expr.arguments().front(), this_type);
1978  assert(is_reference(expr.arguments().front().type()));
1979  expr.arguments().front().type().remove(ID_C_reference);
1980  }
1981  }
1982  else
1983  {
1984  exprt this_arg = to_member_expr(member_expr).compound();
1985  implicit_typecast(this_arg, this_type);
1986  assert(is_reference(this_arg.type()));
1987  this_arg.type().remove(ID_C_reference);
1988  expr.arguments().insert(expr.arguments().begin(), this_arg);
1989  }
1990  }
1991 
1992  if(
1993  symbol.value.id() == ID_cpp_not_typechecked &&
1994  !symbol.value.get_bool(ID_is_used))
1995  {
1996  symbol_table.get_writeable_ref(symbol.name).value.set(ID_is_used, true);
1997  }
1998 }
1999 
2001 {
2002  if(expr.operands().size()!=2)
2003  {
2005  error() << "assignment side effect expected to have two operands"
2006  << eom;
2007  throw 0;
2008  }
2009 
2010  typet type0 = to_binary_expr(expr).op0().type();
2011 
2012  if(is_reference(type0))
2013  type0=type0.subtype();
2014 
2015  if(cpp_is_pod(type0))
2016  {
2017  // for structs we use the 'implicit assignment operator',
2018  // and therefore, it is allowed to assign to a rvalue struct.
2019  if(type0.id() == ID_struct_tag)
2020  to_binary_expr(expr).op0().set(ID_C_lvalue, true);
2021 
2023 
2024  // Note that in C++ (as opposed to C), the assignment yields
2025  // an lvalue!
2026  expr.set(ID_C_lvalue, true);
2027  return;
2028  }
2029 
2030  // It's a non-POD.
2031  // Turn into an operator call
2032 
2033  std::string strop="operator";
2034 
2035  const irep_idt statement=expr.get(ID_statement);
2036 
2037  if(statement==ID_assign)
2038  strop += "=";
2039  else if(statement==ID_assign_shl)
2040  strop += "<<=";
2041  else if(statement==ID_assign_shr)
2042  strop += ">>=";
2043  else if(statement==ID_assign_plus)
2044  strop += "+=";
2045  else if(statement==ID_assign_minus)
2046  strop += "-=";
2047  else if(statement==ID_assign_mult)
2048  strop += "*=";
2049  else if(statement==ID_assign_div)
2050  strop += "/=";
2051  else if(statement==ID_assign_bitand)
2052  strop += "&=";
2053  else if(statement==ID_assign_bitor)
2054  strop += "|=";
2055  else if(statement==ID_assign_bitxor)
2056  strop += "^=";
2057  else
2058  {
2060  error() << "bad assignment operator '" << statement << "'" << eom;
2061  throw 0;
2062  }
2063 
2064  const cpp_namet cpp_name(strop, expr.source_location());
2065 
2066  // expr.op0() is already typechecked
2067  exprt member(ID_member);
2068  member.set(ID_component_cpp_name, cpp_name);
2070 
2072  std::move(member),
2073  {to_binary_expr(expr).op1()},
2075  expr.source_location());
2076 
2078 
2079  expr=new_expr;
2080 }
2081 
2083  side_effect_exprt &expr)
2084 {
2085  if(expr.operands().size()!=1)
2086  {
2088  error() << "statement " << expr.get_statement()
2089  << " expected to have one operand" << eom;
2090  throw 0;
2091  }
2092 
2093  auto &op = to_unary_expr(expr).op();
2094 
2096 
2097  const typet &tmp_type = op.type();
2098 
2099  if(is_number(tmp_type) ||
2100  tmp_type.id()==ID_pointer)
2101  {
2102  // standard stuff
2104  return;
2105  }
2106 
2107  // Turn into an operator call
2108 
2109  std::string str_op="operator";
2110  bool post=false;
2111 
2112  if(expr.get(ID_statement)==ID_preincrement)
2113  str_op += "++";
2114  else if(expr.get(ID_statement)==ID_predecrement)
2115  str_op += "--";
2116  else if(expr.get(ID_statement)==ID_postincrement)
2117  {
2118  str_op += "++";
2119  post=true;
2120  }
2121  else if(expr.get(ID_statement)==ID_postdecrement)
2122  {
2123  str_op += "--";
2124  post=true;
2125  }
2126  else
2127  {
2129  error() << "bad assignment operator '" << expr.get_statement() << "'"
2130  << eom;
2131  throw 0;
2132  }
2133 
2134  const cpp_namet cpp_name(str_op, expr.source_location());
2135 
2136  exprt member(ID_member);
2137  member.set(ID_component_cpp_name, cpp_name);
2139 
2141  std::move(member), {}, uninitialized_typet{}, expr.source_location());
2142 
2143  // the odd C++ way to denote the post-inc/dec operator
2144  if(post)
2145  new_expr.arguments().push_back(
2147 
2149  expr.swap(new_expr);
2150 }
2151 
2153 {
2154  if(expr.operands().size()!=1)
2155  {
2157  error() << "unary operator * expects one operand" << eom;
2158  throw 0;
2159  }
2160 
2161  exprt &op = to_dereference_expr(expr).pointer();
2162  const typet &op_type = op.type();
2163 
2164  if(op_type.id() == ID_pointer && op_type.find(ID_to_member).is_not_nil())
2165  {
2167  error() << "pointer-to-member must use "
2168  << "the .* or ->* operators" << eom;
2169  throw 0;
2170  }
2171 
2173 }
2174 
2176 {
2177  PRECONDITION(expr.id() == ID_pointer_to_member);
2178  PRECONDITION(expr.operands().size() == 2);
2179 
2180  auto &op0 = to_binary_expr(expr).op0();
2181  auto &op1 = to_binary_expr(expr).op1();
2182 
2183  if(op1.type().id() != ID_pointer || op1.type().find(ID_to_member).is_nil())
2184  {
2186  error() << "pointer-to-member expected" << eom;
2187  throw 0;
2188  }
2189 
2190  typet t0 = op0.type().id() == ID_pointer ? op0.type().subtype() : op0.type();
2191 
2192  typet t1((const typet &)op1.type().find(ID_to_member));
2193 
2194  t0=follow(t0);
2195  t1=follow(t1);
2196 
2197  if(t0.id()!=ID_struct)
2198  {
2200  error() << "pointer-to-member type error" << eom;
2201  throw 0;
2202  }
2203 
2204  const struct_typet &from_struct=to_struct_type(t0);
2205  const struct_typet &to_struct=to_struct_type(t1);
2206 
2207  if(!subtype_typecast(from_struct, to_struct))
2208  {
2210  error() << "pointer-to-member type error" << eom;
2211  throw 0;
2212  }
2213 
2214  typecheck_expr_main(op1);
2215 
2216  if(op0.type().id() != ID_pointer)
2217  {
2218  if(op0.id() == ID_dereference)
2219  {
2220  op0 = to_dereference_expr(op0).pointer();
2221  }
2222  else
2223  {
2225  op0.get_bool(ID_C_lvalue),
2226  "pointer-to-member must have lvalue operand");
2227  op0 = address_of_exprt(op0);
2228  }
2229  }
2230 
2231  exprt tmp(op1);
2232  tmp.type().set(ID_C_bound, op0);
2233  expr.swap(tmp);
2234  return;
2235 }
2236 
2238 {
2239  if(expr.id()==ID_symbol)
2240  {
2241  // Check if the function body has to be typechecked
2242  symbol_tablet::symbolst::const_iterator it=
2243  symbol_table.symbols.find(expr.get(ID_identifier));
2244 
2245  assert(it != symbol_table.symbols.end());
2246 
2247  if(it->second.value.id() == ID_cpp_not_typechecked)
2248  symbol_table.get_writeable_ref(it->first).value.set(ID_is_used, true);
2249  }
2250 
2252 }
2253 
2255 {
2256  bool override_constantness = expr.get_bool(ID_C_override_constantness);
2257 
2258  // We take care of an ambiguity in the C++ grammar.
2259  // Needs to be done before the operands!
2261 
2262  // cpp_name uses get_sub, which can get confused with expressions.
2263  if(expr.id()==ID_cpp_name)
2265  else
2266  {
2267  // This does the operands, and then calls typecheck_expr_main.
2269  }
2270 
2271  if(override_constantness)
2272  expr.type().set(ID_C_constant, false);
2273 }
2274 
2276 {
2277  // There is an ambiguity in the C++ grammar as follows:
2278  // (TYPENAME) + expr (typecast of unary plus) vs.
2279  // (expr) + expr (sum of two expressions)
2280  // Same issue with the operators & and - and *
2281 
2282  // We figure this out by resolving the type argument
2283  // and re-writing if needed
2284 
2285  if(expr.id()!="explicit-typecast")
2286  return;
2287 
2288  assert(expr.operands().size()==1);
2289 
2290  irep_idt op0_id = to_unary_expr(expr).op().id();
2291 
2292  if(
2293  expr.type().id() == ID_cpp_name &&
2294  to_unary_expr(expr).op().operands().size() == 1 &&
2295  (op0_id == ID_unary_plus || op0_id == ID_unary_minus ||
2296  op0_id == ID_address_of || op0_id == ID_dereference))
2297  {
2298  exprt resolve_result=
2299  resolve(
2300  to_cpp_name(expr.type()),
2303 
2304  if(resolve_result.id()!=ID_type)
2305  {
2306  // need to re-write the expression
2307  // e.g., (ID) +expr -> ID+expr
2308  exprt new_binary_expr;
2309 
2310  new_binary_expr.operands().resize(2);
2311  to_binary_expr(new_binary_expr).op0().swap(expr.type());
2312  to_binary_expr(new_binary_expr)
2313  .op1()
2314  .swap(to_unary_expr(to_unary_expr(expr).op()).op());
2315 
2316  if(op0_id==ID_unary_plus)
2317  new_binary_expr.id(ID_plus);
2318  else if(op0_id==ID_unary_minus)
2319  new_binary_expr.id(ID_minus);
2320  else if(op0_id==ID_address_of)
2321  new_binary_expr.id(ID_bitand);
2322  else if(op0_id==ID_dereference)
2323  new_binary_expr.id(ID_mult);
2324 
2325  new_binary_expr.add_source_location() =
2326  to_unary_expr(expr).op().source_location();
2327  expr.swap(new_binary_expr);
2328  }
2329  }
2330 }
2331 
2333 {
2334  if(expr.operands().size()!=2)
2335  {
2337  error() << "operator '" << expr.id() << "' expects two operands" << eom;
2338  throw 0;
2339  }
2340 
2343 
2345 }
2346 
2348 {
2350 }
2351 
2353 {
2354  if(expr.operands().size()!=2)
2355  {
2357  error() << "comma operator expects two operands" << eom;
2358  throw 0;
2359  }
2360 
2361  const auto &op0_type = to_binary_expr(expr).op0().type();
2362 
2363  if(op0_type.id() == ID_struct || op0_type.id() == ID_struct_tag)
2364  {
2365  // TODO: check if the comma operator has been overloaded!
2366  }
2367 
2369 }
2370 
2372 {
2374 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
empty_typet void_type()
Definition: c_types.cpp:253
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt & object()
Definition: pointer_expr.h:350
static void make_already_typechecked(exprt &expr)
const exprt & size() const
Definition: std_types.h:771
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Base class of fixed-width bit-vector types.
Definition: std_types.h:832
The Boolean type.
Definition: std_types.h:36
virtual void read(const typet &src) override
virtual bool is_subset_of(const qualifierst &other) const override
Definition: c_qualifiers.h:108
virtual void typecheck_expr_main(exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
symbol_tablet & symbol_table
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
Class type.
Definition: std_types.h:325
codet representation of an expression statement.
Definition: std_code.h:1840
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
const parameterst & parameters() const
Definition: std_types.h:655
struct configt::ansi_ct ansi_c
exprt this_expr
Definition: cpp_id.h:76
irep_idt class_identifier
Definition: cpp_id.h:75
bool is_qualified() const
Definition: cpp_name.h:109
const source_locationt & source_location() const
Definition: cpp_name.h:73
bool is_destructor() const
Definition: cpp_name.h:119
const exprt & as_expr() const
Definition: cpp_name.h:137
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:87
exprt::operandst operands
void add_object(const exprt &expr)
bool find_parent(const symbolt &symb, const irep_idt &base_name, irep_idt &identifier)
void typecheck_expr_typecast(exprt &) override
void typecheck_side_effect_assignment(side_effect_exprt &) override
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
void typecheck_type(typet &) override
void explicit_typecast_ambiguity(exprt &)
template_mapt template_map
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
void convert_pmop(exprt &expr)
void typecheck_expr_sizeof(exprt &) override
void typecheck_code(codet &) override
void typecheck_expr_explicit_typecast(exprt &)
void implicit_typecast(exprt &expr, const typet &type) override
void typecheck_cast_expr(exprt &)
void typecheck_expr_dereference(exprt &) override
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void typecheck_expr_trinary(if_exprt &) override
void typecheck_expr_rel(binary_relation_exprt &) override
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void add_method_body(symbolt *_method_symbol)
void typecheck_expr_binary_arithmetic(exprt &) override
void typecheck_expr_delete(exprt &)
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void typecheck_expr_main(exprt &) override
Called after the operands are done.
void elaborate_class_template(const typet &type)
elaborate class template instances
bool operator_is_overloaded(exprt &)
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
void typecheck_expr_new(exprt &)
void add_implicit_dereference(exprt &)
void typecheck_expr_cpp_name(exprt &, const cpp_typecheck_fargst &)
void typecheck_expr(exprt &) override
void typecheck_expr_side_effect(side_effect_exprt &) override
void typecheck_expr_comma(exprt &) override
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void typecheck_expr_explicit_constructor_call(exprt &)
void typecheck_function_expr(exprt &, const cpp_typecheck_fargst &)
void typecheck_method_application(side_effect_expr_function_callt &)
std::string to_string(const typet &) override
void typecheck_expr_this(exprt &)
void typecheck_expr_throw(exprt &)
bool overloadable(const exprt &)
void typecheck_expr_index(exprt &) override
void typecheck_side_effect_inc_dec(side_effect_exprt &)
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
void typecheck_expr_ptrmember(exprt &) override
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
Definition: cpp_typecheck.h:83
cpp_scopest cpp_scopes
void typecheck_expr_address_of(exprt &) override
void typecheck_expr_function_identifier(exprt &) override
void typecheck_expr_member(exprt &) override
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
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
The Boolean constant false.
Definition: std_expr.h:2811
The trinary if-then-else operator.
Definition: std_expr.h:2172
Array index operator.
Definition: std_expr.h:1328
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
subt & get_sub()
Definition: irep.h:467
irept & add(const irep_namet &name)
Definition: irep.cpp:116
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
void remove(const irep_namet &name)
Definition: irep.cpp:96
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
const exprt & compound() const
Definition: std_expr.h:2654
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
exprt & op0()
Definition: std_expr.h:844
const 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
The NIL expression.
Definition: std_expr.h:2820
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
exprt::operandst & arguments()
Definition: std_code.h:2164
An expression containing a side effect.
Definition: std_code.h:1896
const irep_idt & get_statement() const
Definition: std_code.h:1918
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
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
Definition: std_types.h:285
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
Base type for structs and unions.
Definition: std_types.h:62
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:49
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void print(std::ostream &out) const
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
source_locationt & add_source_location()
Definition: type.h:76
const exprt & op() const
Definition: std_expr.h:293
configt config
Definition: config.cpp:25
irept cpp_exception_list(const typet &src, const namespacet &ns)
turns a type into a list of relevant exception IDs
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.
static exprt collect_comma_expression(const exprt &src)
struct operator_entryt operators[]
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:497
#define forall_operands(it, expr)
Definition: expr.h:18
Expression Initialization.
dstringt irep_idt
Definition: irep.h:37
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:129
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#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
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
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
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:381
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
std::size_t int_width
Definition: config.h:110