cprover
cpp_typecheck_resolve.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_resolve.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <algorithm>
19 
20 #include <util/arith_tools.h>
21 #include <util/c_types.h>
23 #include <util/prefix.h>
24 #include <util/simplify_expr.h>
25 #include <util/std_expr.h>
26 #include <util/string_constant.h>
27 
29 #include <ansi-c/merged_type.h>
30 
31 #include "cpp_convert_type.h"
32 #include "cpp_type2name.h"
33 #include "cpp_typecheck.h"
34 #include "cpp_typecheck_fargs.h"
35 #include "cpp_util.h"
36 
38  cpp_typecheck(_cpp_typecheck),
39  original_scope(nullptr) // set in resolve_scope()
40 {
41 }
42 
44  const cpp_scopest::id_sett &id_set,
45  const cpp_typecheck_fargst &fargs,
46  resolve_identifierst &identifiers)
47 {
48  for(const auto &id_ptr : id_set)
49  {
50  const cpp_idt &identifier = *id_ptr;
51  exprt e=convert_identifier(identifier, fargs);
52 
53  if(e.is_not_nil())
54  {
55  if(e.id()==ID_type)
56  assert(e.type().is_not_nil());
57 
58  identifiers.push_back(e);
59  }
60  }
61 }
62 
64  resolve_identifierst &identifiers,
65  const cpp_template_args_non_tct &template_args,
66  const cpp_typecheck_fargst &fargs)
67 {
68  resolve_identifierst old_identifiers;
69  old_identifiers.swap(identifiers);
70 
71  for(const auto &old_id : old_identifiers)
72  {
73  exprt e = old_id;
74  apply_template_args(e, template_args, fargs);
75 
76  if(e.is_not_nil())
77  {
78  if(e.id()==ID_type)
79  assert(e.type().is_not_nil());
80 
81  identifiers.push_back(e);
82  }
83  }
84 }
85 
88  resolve_identifierst &identifiers,
89  const cpp_typecheck_fargst &fargs)
90 {
91  resolve_identifierst old_identifiers;
92  old_identifiers.swap(identifiers);
93 
94  for(const auto &old_id : old_identifiers)
95  {
96  exprt e = guess_function_template_args(old_id, fargs);
97 
98  if(e.is_not_nil())
99  {
100  assert(e.id()!=ID_type);
101  identifiers.push_back(e);
102  }
103  }
104 
105  disambiguate_functions(identifiers, fargs);
106 
107  // there should only be one left, or we have failed to disambiguate
108  if(identifiers.size()==1)
109  {
110  // instantiate that one
111  exprt e=*identifiers.begin();
112  assert(e.id()==ID_template_function_instance);
113 
114  const symbolt &template_symbol=
115  cpp_typecheck.lookup(e.type().get(ID_C_template));
116 
117  const cpp_template_args_tct &template_args=
118  to_cpp_template_args_tc(e.type().find(ID_C_template_arguments));
119 
120  // Let's build the instance.
121 
122  const symbolt &new_symbol=
125  template_symbol,
126  template_args,
127  template_args);
128 
129  identifiers.clear();
130  identifiers.push_back(
131  symbol_exprt(new_symbol.name, new_symbol.type));
132  }
133 }
134 
136  resolve_identifierst &identifiers)
137 {
138  resolve_identifierst old_identifiers;
139  old_identifiers.swap(identifiers);
140 
141  for(const auto &old_id : old_identifiers)
142  {
143  if(!cpp_typecheck.follow(old_id.type()).get_bool(ID_is_template))
144  identifiers.push_back(old_id);
145  }
146 }
147 
149  resolve_identifierst &identifiers)
150 {
151  resolve_identifierst old_identifiers;
152  old_identifiers.swap(identifiers);
153 
154  std::set<irep_idt> ids;
155  std::set<exprt> other;
156 
157  for(const auto &old_id : old_identifiers)
158  {
159  irep_idt id;
160 
161  if(old_id.id() == ID_symbol)
162  id = to_symbol_expr(old_id).get_identifier();
163  else if(old_id.id() == ID_type && old_id.type().id() == ID_struct_tag)
164  id = to_struct_tag_type(old_id.type()).get_identifier();
165  else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag)
166  id = to_union_tag_type(old_id.type()).get_identifier();
167 
168  if(id.empty())
169  {
170  if(other.insert(old_id).second)
171  identifiers.push_back(old_id);
172  }
173  else
174  {
175  if(ids.insert(id).second)
176  identifiers.push_back(old_id);
177  }
178  }
179 }
180 
182  const cpp_idt &identifier)
183 {
184 #ifdef DEBUG
185  std::cout << "RESOLVE MAP:\n";
186  cpp_typecheck.template_map.print(std::cout);
187 #endif
188 
189  // look up the parameter in the template map
191 
192  if(e.is_nil() ||
193  (e.id()==ID_type && e.type().is_nil()))
194  {
196  cpp_typecheck.error() << "internal error: template parameter "
197  << "without instance:\n"
198  << identifier << messaget::eom;
199  throw 0;
200  }
201 
203 
204  return e;
205 }
206 
208  const cpp_idt &identifier,
209  const cpp_typecheck_fargst &fargs)
210 {
212  return convert_template_parameter(identifier);
213 
214  exprt e;
215 
216  if(identifier.is_member &&
217  !identifier.is_constructor &&
218  !identifier.is_static_member)
219  {
220  // a regular struct or union member
221 
222  const symbolt &compound_symbol=
224 
225  assert(compound_symbol.type.id()==ID_struct ||
226  compound_symbol.type.id()==ID_union);
227 
228  const struct_union_typet &struct_union_type=
229  to_struct_union_type(compound_symbol.type);
230 
231  const exprt &component =
232  struct_union_type.get_component(identifier.identifier);
233 
234  const typet &type=component.type();
235  assert(type.is_not_nil());
236 
238  {
239  e=type_exprt(type);
240  }
241  else if(identifier.id_class==cpp_scopet::id_classt::SYMBOL)
242  {
243  // A non-static, non-type member.
244  // There has to be an object.
245  e=exprt(ID_member);
246  e.set(ID_component_name, identifier.identifier);
248 
249  exprt object;
250  object.make_nil();
251 
252  #if 0
253  std::cout << "I: " << identifier.class_identifier
254  << " "
256  this_class_identifier << '\n';
257  #endif
258 
259  const exprt &this_expr=
261 
262  if(fargs.has_object)
263  {
264  // the object is given to us in fargs
265  assert(!fargs.operands.empty());
266  object=fargs.operands.front();
267  }
268  else if(this_expr.is_not_nil())
269  {
270  // use this->...
271  assert(this_expr.type().id()==ID_pointer);
272  object=exprt(ID_dereference, this_expr.type().subtype());
273  object.copy_to_operands(this_expr);
274  object.type().set(ID_C_constant,
275  this_expr.type().subtype().get_bool(ID_C_constant));
276  object.set(ID_C_lvalue, true);
277  object.add_source_location()=source_location;
278  }
279 
280  // check if the member can be applied to the object
281  typet object_type=cpp_typecheck.follow(object.type());
282 
283  if(object_type.id()==ID_struct ||
284  object_type.id()==ID_union)
285  {
286  if(!has_component_rec(
287  to_struct_union_type(object_type),
288  identifier.identifier,
289  cpp_typecheck))
290  object.make_nil(); // failed!
291  }
292  else
293  object.make_nil();
294 
295  if(object.is_not_nil())
296  {
297  // we got an object
298  e.add_to_operands(std::move(object));
299 
300  bool old_value=cpp_typecheck.disable_access_control;
304  }
305  else
306  {
307  // this has to be a method or form a pointer-to-member expression
308  if(identifier.is_method)
310  else
311  {
312  e.id(ID_ptrmember);
314  exprt("cpp-this", pointer_type(compound_symbol.type)));
315  e.type() = type;
316  }
317  }
318  }
319  }
320  else
321  {
322  const symbolt &symbol=
323  cpp_typecheck.lookup(identifier.identifier);
324 
325  if(symbol.is_type)
326  {
327  e.make_nil();
328 
329  if(symbol.is_macro) // includes typedefs
330  {
331  e = type_exprt(symbol.type);
332  assert(symbol.type.is_not_nil());
333  }
334  else if(symbol.type.id()==ID_c_enum)
335  {
336  e = type_exprt(c_enum_tag_typet(symbol.name));
337  }
338  else if(symbol.type.id() == ID_struct)
339  {
340  e = type_exprt(struct_tag_typet(symbol.name));
341  }
342  else if(symbol.type.id() == ID_union)
343  {
344  e = type_exprt(union_tag_typet(symbol.name));
345  }
346  }
347  else if(symbol.is_macro)
348  {
349  e=symbol.value;
350  assert(e.is_not_nil());
351  }
352  else
353  {
354  bool constant = symbol.type.get_bool(ID_C_constant);
355 
356  if(
357  constant && symbol.value.is_not_nil() && is_number(symbol.type) &&
358  symbol.value.id() == ID_constant)
359  {
360  e=symbol.value;
361  }
362  else
363  {
364  e=cpp_symbol_expr(symbol);
365  }
366  }
367  }
368 
370 
371  return e;
372 }
373 
375  resolve_identifierst &identifiers,
376  const wantt want)
377 {
378  resolve_identifierst old_identifiers;
379  old_identifiers.swap(identifiers);
380 
381  for(const auto &old_id : old_identifiers)
382  {
383  bool match=false;
384 
385  switch(want)
386  {
387  case wantt::TYPE:
388  match = (old_id.id() == ID_type);
389  break;
390 
391  case wantt::VAR:
392  match = (old_id.id() != ID_type);
393  break;
394 
395  case wantt::BOTH:
396  match=true;
397  break;
398 
399  default:
400  UNREACHABLE;
401  }
402 
403  if(match)
404  identifiers.push_back(old_id);
405  }
406 }
407 
409  resolve_identifierst &identifiers,
410  const cpp_typecheck_fargst &fargs)
411 {
412  if(!fargs.in_use)
413  return;
414 
415  resolve_identifierst old_identifiers;
416  old_identifiers.swap(identifiers);
417 
418  identifiers.clear();
419 
420  // put in the ones that match precisely
421  for(const auto &old_id : old_identifiers)
422  {
423  unsigned distance;
424  if(disambiguate_functions(old_id, distance, fargs))
425  if(distance<=0)
426  identifiers.push_back(old_id);
427  }
428 }
429 
431  resolve_identifierst &identifiers,
432  const cpp_typecheck_fargst &fargs)
433 {
434  resolve_identifierst old_identifiers;
435  old_identifiers.swap(identifiers);
436 
437  // sort according to distance
438  std::multimap<std::size_t, exprt> distance_map;
439 
440  for(const auto &old_id : old_identifiers)
441  {
442  unsigned args_distance;
443 
444  if(disambiguate_functions(old_id, args_distance, fargs))
445  {
446  std::size_t template_distance=0;
447 
448  if(!old_id.type().get(ID_C_template).empty())
449  template_distance = old_id.type()
450  .find(ID_C_template_arguments)
451  .find(ID_arguments)
452  .get_sub()
453  .size();
454 
455  // we give strong preference to functions that have
456  // fewer template arguments
457  std::size_t total_distance=
458  // NOLINTNEXTLINE(whitespace/operators)
459  1000*template_distance+args_distance;
460 
461  distance_map.insert({total_distance, old_id});
462  }
463  }
464 
465  old_identifiers.clear();
466 
467  // put in the top ones
468  if(!distance_map.empty())
469  {
470  auto range = distance_map.equal_range(distance_map.begin()->first);
471  for(auto it = range.first; it != range.second; ++it)
472  old_identifiers.push_back(it->second);
473  }
474 
475  if(old_identifiers.size() > 1 && fargs.in_use)
476  {
477  // try to further disambiguate functions
478 
479  for(resolve_identifierst::const_iterator old_it = old_identifiers.begin();
480  old_it != old_identifiers.end();
481  ++old_it)
482  {
483 #if 0
484  std::cout << "I1: " << old_it->get(ID_identifier) << '\n';
485 #endif
486 
487  if(old_it->type().id() != ID_code)
488  {
489  identifiers.push_back(*old_it);
490  continue;
491  }
492 
493  const code_typet &f1 = to_code_type(old_it->type());
494 
495  for(resolve_identifierst::const_iterator resolve_it = old_it + 1;
496  resolve_it != old_identifiers.end();
497  ++resolve_it)
498  {
499  if(resolve_it->type().id() != ID_code)
500  continue;
501 
502  const code_typet &f2 = to_code_type(resolve_it->type());
503 
504  // TODO: may fail when using ellipsis
505  assert(f1.parameters().size() == f2.parameters().size());
506 
507  bool f1_better=true;
508  bool f2_better=true;
509 
510  for(std::size_t i=0;
511  i<f1.parameters().size() && (f1_better || f2_better);
512  i++)
513  {
514  typet type1=f1.parameters()[i].type();
515  typet type2=f2.parameters()[i].type();
516 
517  if(type1 == type2)
518  continue;
519 
520  if(is_reference(type1) != is_reference(type2))
521  continue;
522 
523  if(type1.id()==ID_pointer)
524  {
525  typet tmp=type1.subtype();
526  type1=tmp;
527  }
528 
529  if(type2.id()==ID_pointer)
530  {
531  typet tmp=type2.subtype();
532  type2=tmp;
533  }
534 
535  const typet &followed1=cpp_typecheck.follow(type1);
536  const typet &followed2=cpp_typecheck.follow(type2);
537 
538  if(followed1.id() != ID_struct || followed2.id() != ID_struct)
539  continue;
540 
541  const struct_typet &struct1=to_struct_type(followed1);
542  const struct_typet &struct2=to_struct_type(followed2);
543 
544  if(f1_better && cpp_typecheck.subtype_typecast(struct1, struct2))
545  {
546  f2_better=false;
547  }
548  else if(f2_better && cpp_typecheck.subtype_typecast(struct2, struct1))
549  {
550  f1_better=false;
551  }
552  }
553 
554  if(!f1_better || f2_better)
555  identifiers.push_back(*resolve_it);
556  }
557  }
558  }
559  else
560  {
561  identifiers.swap(old_identifiers);
562  }
563 
564  remove_duplicates(identifiers);
565 }
566 
568  resolve_identifierst &identifiers)
569 {
570  resolve_identifierst new_identifiers;
571 
572  for(const auto &identifier : identifiers)
573  {
574  if(identifier.id() != ID_type)
575  {
576  // already an expression
577  new_identifiers.push_back(identifier);
578  continue;
579  }
580 
581  const typet &symbol_type = cpp_typecheck.follow(identifier.type());
582 
583  // is it a POD?
584 
585  if(cpp_typecheck.cpp_is_pod(symbol_type))
586  {
587  // there are two pod constructors:
588 
589  // 1. no arguments, default initialization
590  {
591  const code_typet t1({}, identifier.type());
592  exprt pod_constructor1(ID_pod_constructor, t1);
593  new_identifiers.push_back(pod_constructor1);
594  }
595 
596  // 2. one argument, copy/conversion
597  {
598  const code_typet t2(
599  {code_typet::parametert(identifier.type())}, identifier.type());
600  exprt pod_constructor2(ID_pod_constructor, t2);
601  new_identifiers.push_back(pod_constructor2);
602  }
603 
604  // enums, in addition, can also be constructed from int
605  if(symbol_type.id()==ID_c_enum_tag)
606  {
607  const code_typet t3(
608  {code_typet::parametert(signed_int_type())}, identifier.type());
609  exprt pod_constructor3(ID_pod_constructor, t3);
610  new_identifiers.push_back(pod_constructor3);
611  }
612  }
613  else if(symbol_type.id()==ID_struct)
614  {
615  const struct_typet &struct_type=to_struct_type(symbol_type);
616 
617  // go over components
618  for(const auto &component : struct_type.components())
619  {
620  const typet &type=component.type();
621 
622  if(component.get_bool(ID_from_base))
623  continue;
624 
625  if(
626  type.id() == ID_code &&
627  to_code_type(type).return_type().id() == ID_constructor)
628  {
629  const symbolt &symb =
630  cpp_typecheck.lookup(component.get_name());
631  exprt e=cpp_symbol_expr(symb);
632  e.type()=type;
633  new_identifiers.push_back(e);
634  }
635  }
636  }
637  }
638 
639  identifiers.swap(new_identifiers);
640 }
641 
643  exprt &argument,
644  const cpp_typecheck_fargst &fargs)
645 {
646  if(argument.id() == ID_ambiguous) // could come from a template parameter
647  {
648  // this must be resolved in the template scope
651 
652  argument = resolve(to_cpp_name(argument.type()), wantt::VAR, fargs, false);
653  }
654 }
655 
657  const irep_idt &base_name,
658  const cpp_typecheck_fargst &fargs,
659  const cpp_template_args_non_tct &template_args)
660 {
661  exprt dest;
662 
663  const cpp_template_args_non_tct::argumentst &arguments=
664  template_args.arguments();
665 
666  if(base_name==ID_unsignedbv ||
667  base_name==ID_signedbv)
668  {
669  if(arguments.size()!=1)
670  {
673  << base_name << " expects one template argument, but got "
674  << arguments.size() << messaget::eom;
675  throw 0;
676  }
677 
678  exprt argument=arguments.front(); // copy
679 
680  if(argument.id()==ID_type)
681  {
684  << base_name << " expects one integer template argument, "
685  << "but got type" << messaget::eom;
686  throw 0;
687  }
688 
689  resolve_argument(argument, fargs);
690 
691  const auto i = numeric_cast<mp_integer>(argument);
692  if(!i.has_value())
693  {
695  cpp_typecheck.error() << "template argument must be constant"
696  << messaget::eom;
697  throw 0;
698  }
699 
700  if(*i < 1)
701  {
704  << "template argument must be greater than zero"
705  << messaget::eom;
706  throw 0;
707  }
708 
709  dest=type_exprt(typet(base_name));
710  dest.type().set(ID_width, integer2string(*i));
711  }
712  else if(base_name==ID_fixedbv)
713  {
714  if(arguments.size()!=2)
715  {
718  << base_name << " expects two template arguments, but got "
719  << arguments.size() << messaget::eom;
720  throw 0;
721  }
722 
723  exprt argument0=arguments[0];
724  resolve_argument(argument0, fargs);
725  exprt argument1=arguments[1];
726  resolve_argument(argument1, fargs);
727 
728  if(argument0.id()==ID_type)
729  {
732  << base_name << " expects two integer template arguments, "
733  << "but got type" << messaget::eom;
734  throw 0;
735  }
736 
737  if(argument1.id()==ID_type)
738  {
741  << base_name << " expects two integer template arguments, "
742  << "but got type" << messaget::eom;
743  throw 0;
744  }
745 
746  const auto width = numeric_cast<mp_integer>(argument0);
747 
748  if(!width.has_value())
749  {
751  cpp_typecheck.error() << "template argument must be constant"
752  << messaget::eom;
753  throw 0;
754  }
755 
756  const auto integer_bits = numeric_cast<mp_integer>(argument1);
757 
758  if(!integer_bits.has_value())
759  {
761  cpp_typecheck.error() << "template argument must be constant"
762  << messaget::eom;
763  throw 0;
764  }
765 
766  if(*width < 1)
767  {
770  << "template argument must be greater than zero"
771  << messaget::eom;
772  throw 0;
773  }
774 
775  if(*integer_bits < 0)
776  {
779  << "template argument must be greater or equal zero"
780  << messaget::eom;
781  throw 0;
782  }
783 
784  if(*integer_bits > *width)
785  {
788  << "template argument must be smaller or equal width"
789  << messaget::eom;
790  throw 0;
791  }
792 
793  dest=type_exprt(typet(base_name));
794  dest.type().set(ID_width, integer2string(*width));
795  dest.type().set(ID_integer_bits, integer2string(*integer_bits));
796  }
797  else if(base_name==ID_integer)
798  {
799  if(!arguments.empty())
800  {
803  << base_name << " expects no template arguments"
804  << messaget::eom;
805  throw 0;
806  }
807 
808  dest=type_exprt(typet(base_name));
809  }
810  else if(has_prefix(id2string(base_name), "constant_infinity"))
811  {
812  // ok, but type missing
813  dest=exprt(ID_infinity, size_type());
814  }
815  else if(base_name=="dump_scopes")
816  {
817  dest=exprt(ID_constant, typet(ID_empty));
818  cpp_typecheck.warning() << "Scopes in location "
822  }
823  else if(base_name=="current_scope")
824  {
825  dest=exprt(ID_constant, typet(ID_empty));
826  cpp_typecheck.warning() << "Scope in location " << source_location
827  << ": " << original_scope->prefix
828  << messaget::eom;
829  }
830  else if(base_name == ID_size_t)
831  {
832  dest=type_exprt(size_type());
833  }
834  else if(base_name == ID_ssize_t)
835  {
837  }
838  else
839  {
841  cpp_typecheck.error() << "unknown built-in identifier: "
842  << base_name << messaget::eom;
843  throw 0;
844  }
845 
846  return dest;
847 }
848 
853  const cpp_namet &cpp_name,
854  irep_idt &base_name,
855  cpp_template_args_non_tct &template_args)
856 {
857  assert(!cpp_name.get_sub().empty());
858 
860  source_location=cpp_name.source_location();
861 
862  irept::subt::const_iterator pos=cpp_name.get_sub().begin();
863 
864  bool recursive=true;
865 
866  // check if we need to go to the root scope
867  if(pos->id()=="::")
868  {
869  pos++;
871  recursive=false;
872  }
873 
874  std::string final_base_name;
875  template_args.make_nil();
876 
877  while(pos!=cpp_name.get_sub().end())
878  {
879  if(pos->id()==ID_name)
880  final_base_name+=pos->get_string(ID_identifier);
881  else if(pos->id()==ID_template_args)
882  template_args=to_cpp_template_args_non_tc(*pos);
883  else if(pos->id()=="::")
884  {
885  if(template_args.is_not_nil())
886  {
887  const auto id_set = cpp_typecheck.cpp_scopes.current_scope().lookup(
888  final_base_name,
891 
892 #ifdef DEBUG
893  std::cout << "S: "
895  << '\n';
897  std::cout << "X: " << id_set.size() << '\n';
898 #endif
899  struct_tag_typet instance =
900  disambiguate_template_classes(final_base_name, id_set, template_args);
901 
903 
904  // the "::" triggers template elaboration
906 
909 
910  template_args.make_nil();
911  }
912  else
913  {
915  final_base_name,
917 
918  filter_for_named_scopes(id_set);
919 
920  if(id_set.empty())
921  {
925  << "scope '" << final_base_name << "' not found" << messaget::eom;
926  throw 0;
927  }
928  else if(id_set.size()>=2)
929  {
932  cpp_typecheck.error() << "scope '" << final_base_name
933  << "' is ambiguous" << messaget::eom;
934  throw 0;
935  }
936 
937  assert(id_set.size()==1);
938 
939  cpp_typecheck.cpp_scopes.go_to(**id_set.begin());
940 
941  // the "::" triggers template elaboration
943  {
944  struct_tag_typet instance(
947  }
948  }
949 
950  // we start from fresh
951  final_base_name.clear();
952  }
953  else if(pos->id()==ID_operator)
954  {
955  final_base_name+="operator";
956 
957  irept::subt::const_iterator next=pos+1;
958  assert(next != cpp_name.get_sub().end());
959 
960  if(
961  next->id() == ID_cpp_name || next->id() == ID_pointer ||
962  next->id() == ID_int || next->id() == ID_char ||
963  next->id() == ID_c_bool || next->id() == ID_merged_type)
964  {
965  // it's a cast operator
966  irept next_ir=*next;
967  typet op_name;
968  op_name.swap(next_ir);
969  cpp_typecheck.typecheck_type(op_name);
970  final_base_name+="("+cpp_type2name(op_name)+")";
971  pos++;
972  }
973  }
974  else
975  final_base_name+=pos->id_string();
976 
977  pos++;
978  }
979 
980  base_name=final_base_name;
981 
983 }
984 
987  const irep_idt &base_name,
988  const cpp_scopest::id_sett &id_set,
989  const cpp_template_args_non_tct &full_template_args)
990 {
991  if(id_set.empty())
992  {
995  cpp_typecheck.error() << "template scope '" << base_name << "' not found"
996  << messaget::eom;
997  throw 0;
998  }
999 
1000  std::set<irep_idt> primary_templates;
1001 
1002  for(const auto &id_ptr : id_set)
1003  {
1004  const irep_idt id = id_ptr->identifier;
1005  const symbolt &s=cpp_typecheck.lookup(id);
1006  if(!s.type.get_bool(ID_is_template))
1007  continue;
1008  const cpp_declarationt &cpp_declaration=to_cpp_declaration(s.type);
1009  if(!cpp_declaration.is_class_template())
1010  continue;
1011  irep_idt specialization_of=cpp_declaration.get_specialization_of();
1012  if(!specialization_of.empty())
1013  primary_templates.insert(specialization_of);
1014  else
1015  primary_templates.insert(id);
1016  }
1017 
1018  assert(!primary_templates.empty());
1019 
1020  if(primary_templates.size()>=2)
1021  {
1024  cpp_typecheck.error() << "template scope '" << base_name << "' is ambiguous"
1025  << messaget::eom;
1026  throw 0;
1027  }
1028 
1029  const symbolt &primary_template_symbol=
1030  cpp_typecheck.lookup(*primary_templates.begin());
1031 
1032  // We typecheck the template arguments in the context
1033  // of the original scope!
1034  cpp_template_args_tct full_template_args_tc;
1035 
1036  {
1038 
1040 
1041  // use template type of 'primary template'
1042  full_template_args_tc=
1045  primary_template_symbol,
1046  full_template_args);
1047 
1048  for(auto &arg : full_template_args_tc.arguments())
1049  {
1050  if(arg.id() == ID_type)
1051  continue;
1052  if(arg.id() == ID_symbol)
1053  {
1054  const symbol_exprt &s = to_symbol_expr(arg);
1055  const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier());
1056 
1057  if(
1058  cpp_typecheck.cpp_is_pod(symbol.type) &&
1059  symbol.type.get_bool(ID_C_constant))
1060  {
1061  arg = symbol.value;
1062  }
1063  }
1064  simplify(arg, cpp_typecheck);
1065  }
1066 
1067  // go back to where we used to be
1068  }
1069 
1070  // find any matches
1071 
1072  std::vector<matcht> matches;
1073 
1074  // the baseline
1075  matches.push_back(
1076  matcht(full_template_args_tc, full_template_args_tc,
1077  primary_template_symbol.name));
1078 
1079  for(const auto &id_ptr : id_set)
1080  {
1081  const irep_idt id = id_ptr->identifier;
1082  const symbolt &s=cpp_typecheck.lookup(id);
1083 
1084  if(s.type.get(ID_specialization_of).empty())
1085  continue;
1086 
1087  const cpp_declarationt &cpp_declaration=
1089 
1090  const cpp_template_args_non_tct &partial_specialization_args=
1091  cpp_declaration.partial_specialization_args();
1092 
1093  // alright, set up template arguments as 'unassigned'
1094 
1097 
1099  cpp_declaration.template_type());
1100 
1101  // iterate over template instance
1102  assert(full_template_args_tc.arguments().size()==
1103  partial_specialization_args.arguments().size());
1104 
1105  // we need to do this in the right scope
1106 
1107  cpp_scopet *template_scope=
1108  static_cast<cpp_scopet *>(
1110 
1111  if(template_scope==nullptr)
1112  {
1114  cpp_typecheck.error() << "template identifier: " << id << '\n'
1115  << "class template instantiation error"
1116  << messaget::eom;
1117  throw 0;
1118  }
1119 
1120  // enter the scope of the template
1121  cpp_typecheck.cpp_scopes.go_to(*template_scope);
1122 
1123  for(std::size_t i=0; i<full_template_args_tc.arguments().size(); i++)
1124  {
1125  if(full_template_args_tc.arguments()[i].id()==ID_type)
1126  guess_template_args(partial_specialization_args.arguments()[i].type(),
1127  full_template_args_tc.arguments()[i].type());
1128  else
1129  guess_template_args(partial_specialization_args.arguments()[i],
1130  full_template_args_tc.arguments()[i]);
1131  }
1132 
1133  // see if that has worked out
1134 
1135  cpp_template_args_tct guessed_template_args=
1137  cpp_declaration.template_type());
1138 
1139  if(!guessed_template_args.has_unassigned())
1140  {
1141  // check: we can now typecheck the partial_specialization_args
1142 
1143  cpp_template_args_tct partial_specialization_args_tc=
1146  primary_template_symbol,
1147  partial_specialization_args);
1148 
1149  // if these match the arguments, we have a match
1150 
1151  assert(partial_specialization_args_tc.arguments().size()==
1152  full_template_args_tc.arguments().size());
1153 
1154  if(partial_specialization_args_tc==
1155  full_template_args_tc)
1156  {
1157  matches.push_back(matcht(
1158  guessed_template_args, full_template_args_tc, id));
1159  }
1160  }
1161  }
1162 
1163  assert(!matches.empty());
1164 
1165  std::sort(matches.begin(), matches.end());
1166 
1167  #if 0
1168  for(std::vector<matcht>::const_iterator
1169  m_it=matches.begin();
1170  m_it!=matches.end();
1171  m_it++)
1172  {
1173  std::cout << "M: " << m_it->cost
1174  << " " << m_it->id << '\n';
1175  }
1176 
1177  std::cout << '\n';
1178  #endif
1179 
1180  const matcht &match=*matches.begin();
1181 
1182  const symbolt &choice=
1183  cpp_typecheck.lookup(match.id);
1184 
1185  #if 0
1186  // build instance
1187  const symbolt &instance=
1190  choice,
1191  match.specialization_args,
1192  match.full_args);
1193 
1194  if(instance.type.id()!=ID_struct)
1195  {
1197  cpp_typecheck.error() << "template '"
1198  << base_name << "' is not a class" << messaget::eom;
1199  throw 0;
1200  }
1201 
1202  struct_tag_typet result(instance.name);
1204 
1205  return result;
1206  #else
1207 
1208  // build instance
1209  const symbolt &instance=
1212  choice,
1213  match.specialization_args,
1214  match.full_args);
1215 
1216  struct_tag_typet result(instance.name);
1218 
1219  return result;
1220  #endif
1221 }
1222 
1224  const cpp_namet &cpp_name)
1225 {
1226  irep_idt base_name;
1227  cpp_template_args_non_tct template_args;
1228  template_args.make_nil();
1229 
1231  resolve_scope(cpp_name, base_name, template_args);
1232 
1233  bool qualified=cpp_name.is_qualified();
1234 
1235  auto id_set = cpp_typecheck.cpp_scopes.current_scope().lookup(
1236  base_name, qualified ? cpp_scopet::QUALIFIED : cpp_scopet::RECURSIVE);
1237 
1238  filter_for_namespaces(id_set);
1239 
1240  if(id_set.empty())
1241  {
1243  cpp_typecheck.error() << "namespace '" << base_name << "' not found"
1244  << messaget::eom;
1245  throw 0;
1246  }
1247  else if(id_set.size()==1)
1248  {
1249  cpp_idt &id=**id_set.begin();
1250  return (cpp_scopet &)id;
1251  }
1252  else
1253  {
1255  cpp_typecheck.error() << "namespace '" << base_name << "' is ambiguous"
1256  << messaget::eom;
1257  throw 0;
1258  }
1259 }
1260 
1262  const irep_idt &base_name,
1263  const resolve_identifierst &identifiers,
1264  std::ostream &out)
1265 {
1266  for(const auto &id_expr : identifiers)
1267  {
1268  out << " ";
1269 
1270  if(id_expr.id()==ID_type)
1271  {
1272  out << "type " << cpp_typecheck.to_string(id_expr.type());
1273  }
1274  else
1275  {
1276  irep_idt id;
1277 
1278  if(id_expr.type().get_bool(ID_is_template))
1279  out << "template ";
1280 
1281  if(id_expr.id()==ID_member)
1282  {
1283  out << "member ";
1284  id="."+id2string(base_name);
1285  }
1286  else if(id_expr.id() == ID_pod_constructor)
1287  {
1288  out << "constructor ";
1289  id.clear();
1290  }
1291  else if(id_expr.id()==ID_template_function_instance)
1292  {
1293  out << "symbol ";
1294  }
1295  else
1296  {
1297  out << "symbol ";
1298  id=cpp_typecheck.to_string(id_expr);
1299  }
1300 
1301  if(id_expr.type().get_bool(ID_is_template))
1302  {
1303  }
1304  else if(id_expr.type().id()==ID_code)
1305  {
1306  const code_typet &code_type=to_code_type(id_expr.type());
1307  const typet &return_type=code_type.return_type();
1308  const code_typet::parameterst &parameters=code_type.parameters();
1309  out << cpp_typecheck.to_string(return_type);
1310  out << " " << id << "(";
1311 
1312  bool first = true;
1313 
1314  for(const auto &parameter : parameters)
1315  {
1316  const typet &parameter_type = parameter.type();
1317 
1318  if(first)
1319  first = false;
1320  else
1321  out << ", ";
1322 
1323  out << cpp_typecheck.to_string(parameter_type);
1324  }
1325 
1326  if(code_type.has_ellipsis())
1327  {
1328  if(!parameters.empty())
1329  out << ", ";
1330  out << "...";
1331  }
1332 
1333  out << ")";
1334  }
1335  else
1336  out << id << ": " << cpp_typecheck.to_string(id_expr.type());
1337 
1338  if(id_expr.id()==ID_symbol)
1339  {
1340  const symbolt &symbol=cpp_typecheck.lookup(to_symbol_expr(id_expr));
1341  out << " (" << symbol.location << ")";
1342  }
1343  else if(id_expr.id()==ID_template_function_instance)
1344  {
1345  const symbolt &symbol=
1346  cpp_typecheck.lookup(id_expr.type().get(ID_C_template));
1347  out << " (" << symbol.location << ")";
1348  }
1349  }
1350 
1351  out << '\n';
1352  }
1353 }
1354 
1356  const cpp_namet &cpp_name,
1357  const wantt want,
1358  const cpp_typecheck_fargst &fargs,
1359  bool fail_with_exception)
1360 {
1361  irep_idt base_name;
1362  cpp_template_args_non_tct template_args;
1363  template_args.make_nil();
1364 
1367 
1368  // this changes the scope
1369  resolve_scope(cpp_name, base_name, template_args);
1370 
1371 #ifdef DEBUG
1372  std::cout << "base name: " << base_name << '\n';
1373  std::cout << "template args: " << template_args.pretty() << '\n';
1374  std::cout << "original-scope: " << original_scope->prefix << '\n';
1375  std::cout << "scope: " << cpp_typecheck.cpp_scopes.current_scope().prefix
1376  << '\n';
1377 #endif
1378 
1379  bool qualified=cpp_name.is_qualified();
1380 
1381  // do __CPROVER scope
1382  if(qualified)
1383  {
1385  return do_builtin(base_name, fargs, template_args);
1386  }
1387  else
1388  {
1389  if(base_name=="__func__" ||
1390  base_name=="__FUNCTION__" ||
1391  base_name=="__PRETTY_FUNCTION__")
1392  {
1393  // __func__ is an ANSI-C standard compliant hack to get the function name
1394  // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
1397  return std::move(s);
1398  }
1399  }
1400 
1401  cpp_scopest::id_sett id_set;
1402 
1403  cpp_scopet::lookup_kindt lookup_kind=
1405 
1406  if(template_args.is_nil())
1407  {
1408  id_set =
1409  cpp_typecheck.cpp_scopes.current_scope().lookup(base_name, lookup_kind);
1410 
1411  if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name))
1412  {
1413  cpp_idt &builtin_id =
1415  builtin_id.identifier = base_name;
1416  builtin_id.id_class = cpp_idt::id_classt::SYMBOL;
1417 
1418  id_set.insert(&builtin_id);
1419  }
1420  }
1421  else
1423  base_name, lookup_kind, cpp_idt::id_classt::TEMPLATE);
1424 
1425  // Argument-dependent name lookup
1426  #if 0
1427  // not clear what this is good for
1428  if(!qualified && !fargs.has_object)
1429  resolve_with_arguments(id_set, base_name, fargs);
1430  #endif
1431 
1432  if(id_set.empty())
1433  {
1434  if(!fail_with_exception)
1435  return nil_exprt();
1436 
1439 
1440  if(qualified)
1441  {
1442  cpp_typecheck.error() << "symbol '" << base_name << "' not found";
1443 
1445  cpp_typecheck.error() << " in root scope";
1446  else
1448  << " in scope '" << cpp_typecheck.cpp_scopes.current_scope().prefix
1449  << "'";
1450  }
1451  else
1452  {
1453  cpp_typecheck.error() << "symbol '" << base_name << "' is unknown";
1454  }
1455 
1457  // cpp_typecheck.cpp_scopes.get_root_scope().print(std::cout);
1458  // cpp_typecheck.cpp_scopes.current_scope().print(std::cout);
1459  throw 0;
1460  }
1461 
1462  resolve_identifierst identifiers;
1463 
1464  if(template_args.is_not_nil())
1465  {
1466  // first figure out if we are doing functions/methods or
1467  // classes
1468  bool have_classes=false, have_methods=false;
1469 
1470  for(const auto &id_ptr : id_set)
1471  {
1472  const irep_idt id = id_ptr->identifier;
1473  const symbolt &s=cpp_typecheck.lookup(id);
1474  assert(s.type.get_bool(ID_is_template));
1476  have_classes=true;
1477  else
1478  have_methods=true;
1479  }
1480 
1481  if(want==wantt::BOTH && have_classes && have_methods)
1482  {
1483  if(!fail_with_exception)
1484  return nil_exprt();
1485 
1488  cpp_typecheck.error() << "template symbol '" << base_name
1489  << "' is ambiguous" << messaget::eom;
1490  throw 0;
1491  }
1492 
1493  if(want==wantt::TYPE || have_classes)
1494  {
1495  typet instance=
1496  disambiguate_template_classes(base_name, id_set, template_args);
1497 
1499 
1500  identifiers.push_back(exprt(ID_type, instance));
1501  }
1502  else
1503  {
1504  // methods and functions
1506  id_set, fargs, identifiers);
1507 
1509  identifiers, template_args, fargs);
1510  }
1511  }
1512  else
1513  {
1515  id_set, fargs, identifiers);
1516  }
1517 
1518  // change types into constructors if we want a constructor
1519  if(want==wantt::VAR)
1520  make_constructors(identifiers);
1521 
1522  filter(identifiers, want);
1523 
1524 #ifdef DEBUG
1525  std::cout << "P0 " << base_name << " " << identifiers.size() << '\n';
1526  show_identifiers(base_name, identifiers, std::cout);
1527  std::cout << '\n';
1528 #endif
1529 
1530  exprt result;
1531 
1532  // We disambiguate functions
1533  resolve_identifierst new_identifiers=identifiers;
1534 
1535  remove_templates(new_identifiers);
1536 
1537 #ifdef DEBUG
1538  std::cout << "P1 " << base_name << " " << new_identifiers.size() << '\n';
1539  show_identifiers(base_name, new_identifiers, std::cout);
1540  std::cout << '\n';
1541 #endif
1542 
1543  // we only want _exact_ matches, without templates!
1544  exact_match_functions(new_identifiers, fargs);
1545 
1546 #ifdef DEBUG
1547  std::cout << "P2 " << base_name << " " << new_identifiers.size() << '\n';
1548  show_identifiers(base_name, new_identifiers, std::cout);
1549  std::cout << '\n';
1550 #endif
1551 
1552  // no exact matches? Try again with function template guessing.
1553  if(new_identifiers.empty())
1554  {
1555  new_identifiers=identifiers;
1556 
1557  if(template_args.is_nil())
1558  {
1559  guess_function_template_args(new_identifiers, fargs);
1560 
1561  if(new_identifiers.empty())
1562  new_identifiers=identifiers;
1563  }
1564 
1565  disambiguate_functions(new_identifiers, fargs);
1566 
1567 #ifdef DEBUG
1568  std::cout << "P3 " << base_name << " " << new_identifiers.size() << '\n';
1569  show_identifiers(base_name, new_identifiers, std::cout);
1570  std::cout << '\n';
1571 #endif
1572  }
1573  else
1574  remove_duplicates(new_identifiers);
1575 
1576 #ifdef DEBUG
1577  std::cout << "P4 " << base_name << " " << new_identifiers.size() << '\n';
1578  show_identifiers(base_name, new_identifiers, std::cout);
1579  std::cout << '\n';
1580 #endif
1581 
1582  if(new_identifiers.size()==1)
1583  {
1584  result=*new_identifiers.begin();
1585  }
1586  else
1587  {
1588  // nothing or too many
1589  if(!fail_with_exception)
1590  return nil_exprt();
1591 
1592  if(new_identifiers.empty())
1593  {
1596  << "found no match for symbol '" << base_name << "', candidates are:\n";
1597  show_identifiers(base_name, identifiers, cpp_typecheck.error());
1598  }
1599  else
1600  {
1603  << "symbol '" << base_name << "' does not uniquely resolve:\n";
1604  show_identifiers(base_name, new_identifiers, cpp_typecheck.error());
1605 
1606 #ifdef DEBUG
1607  exprt e1=*new_identifiers.begin();
1608  exprt e2=*(++new_identifiers.begin());
1609  cpp_typecheck.error() << "e1==e2: " << (e1 == e2) << '\n';
1611  << "e1.type==e2.type: " << (e1.type() == e2.type()) << '\n';
1613  << "e1.id()==e2.id(): " << (e1.id() == e2.id()) << '\n';
1615  << "e1.iden==e2.iden: "
1616  << (e1.get(ID_identifier) == e2.get(ID_identifier)) << '\n';
1617  cpp_typecheck.error() << "e1.iden:: " << e1.get(ID_identifier) << '\n';
1618  cpp_typecheck.error() << "e2.iden:: " << e2.get(ID_identifier) << '\n';
1619 #endif
1620  }
1621 
1622  if(fargs.in_use)
1623  {
1624  cpp_typecheck.error() << "\nargument types:\n";
1625 
1626  for(const auto &op : fargs.operands)
1627  {
1629  << " " << cpp_typecheck.to_string(op.type()) << '\n';
1630  }
1631  }
1632 
1633  if(!cpp_typecheck.instantiation_stack.empty())
1634  {
1636  }
1637 
1639  throw 0;
1640  }
1641 
1642  // we do some checks before we return
1643  if(result.get_bool(ID_C_not_accessible))
1644  {
1645  #if 0
1646  if(!fail_with_exception)
1647  return nil_exprt();
1648 
1650  cpp_typecheck.str
1651  << "error: member '" << result.get(ID_component_name)
1652  << "' is not accessible";
1653  throw 0;
1654  #endif
1655  }
1656 
1657  switch(want)
1658  {
1659  case wantt::VAR:
1660  if(result.id()==ID_type && !cpp_typecheck.cpp_is_pod(result.type()))
1661  {
1662  if(!fail_with_exception)
1663  return nil_exprt();
1664 
1666 
1668  << "error: expected expression, but got type '"
1669  << cpp_typecheck.to_string(result.type()) << "'" << messaget::eom;
1670 
1671  throw 0;
1672  }
1673  break;
1674 
1675  case wantt::TYPE:
1676  if(result.id()!=ID_type)
1677  {
1678  if(!fail_with_exception)
1679  return nil_exprt();
1680 
1682 
1684  << "error: expected type, but got expression '"
1685  << cpp_typecheck.to_string(result) << "'" << messaget::eom;
1686 
1687  throw 0;
1688  }
1689  break;
1690 
1691  case wantt::BOTH:
1692  break;
1693  }
1694 
1695  return result;
1696 }
1697 
1699  const exprt &template_expr,
1700  const exprt &desired_expr)
1701 {
1702  if(template_expr.id()==ID_cpp_name)
1703  {
1704  const cpp_namet &cpp_name=
1705  to_cpp_name(template_expr);
1706 
1707  if(!cpp_name.is_qualified())
1708  {
1710 
1711  cpp_template_args_non_tct template_args;
1712  irep_idt base_name;
1713  resolve_scope(cpp_name, base_name, template_args);
1714 
1715  const auto id_set = cpp_typecheck.cpp_scopes.current_scope().lookup(
1716  base_name, cpp_scopet::RECURSIVE);
1717 
1718  // alright, rummage through these
1719  for(const auto &id_ptr : id_set)
1720  {
1721  const cpp_idt &id = *id_ptr;
1722  // template parameter?
1724  {
1725  // see if unassigned
1726  exprt &e=cpp_typecheck.template_map.expr_map[id.identifier];
1727  if(e.id()==ID_unassigned)
1728  {
1729  typet old_type=e.type();
1730  e = typecast_exprt::conditional_cast(desired_expr, old_type);
1731  }
1732  }
1733  }
1734  }
1735  }
1736 }
1737 
1739  const typet &template_type,
1740  const typet &desired_type)
1741 {
1742  // look at
1743  // http://publib.boulder.ibm.com/infocenter/comphelp/v8v101/topic/
1744  // com.ibm.xlcpp8a.doc/language/ref/template_argument_deduction.htm
1745 
1746  // T
1747  // const T
1748  // volatile T
1749  // T&
1750  // T*
1751  // T[10]
1752  // A<T>
1753  // C(*)(T)
1754  // T(*)()
1755  // T(*)(U)
1756  // T C::*
1757  // C T::*
1758  // T U::*
1759  // T (C::*)()
1760  // C (T::*)()
1761  // D (C::*)(T)
1762  // C (T::*)(U)
1763  // T (C::*)(U)
1764  // T (U::*)()
1765  // T (U::*)(V)
1766  // E[10][i]
1767  // B<i>
1768  // TT<T>
1769  // TT<i>
1770  // TT<C>
1771 
1772  #if 0
1773  std::cout << "TT: " << template_type.pretty() << '\n';
1774  std::cout << "DT: " << desired_type.pretty() << '\n';
1775  #endif
1776 
1777  if(template_type.id()==ID_cpp_name)
1778  {
1779  // we only care about cpp_names that are template parameters!
1780  const cpp_namet &cpp_name=to_cpp_name(template_type);
1781 
1783 
1784  if(cpp_name.has_template_args())
1785  {
1786  // this could be something like my_template<T>, and we need
1787  // to match 'T'. Then 'desired_type' has to be a template instance.
1788 
1789  // TODO
1790  }
1791  else
1792  {
1793  // template parameters aren't qualified
1794  if(!cpp_name.is_qualified())
1795  {
1796  irep_idt base_name;
1797  cpp_template_args_non_tct template_args;
1798  resolve_scope(cpp_name, base_name, template_args);
1799 
1800  const auto id_set = cpp_typecheck.cpp_scopes.current_scope().lookup(
1801  base_name, cpp_scopet::RECURSIVE);
1802 
1803  // alright, rummage through these
1804  for(const auto &id_ptr : id_set)
1805  {
1806  const cpp_idt &id = *id_ptr;
1807 
1808  // template argument?
1810  {
1811  // see if unassigned
1812  typet &t=cpp_typecheck.template_map.type_map[id.identifier];
1813  if(t.id()==ID_unassigned)
1814  {
1815  t=desired_type;
1816 
1817  // remove const, volatile (these can be added in the call)
1818  t.remove(ID_C_constant);
1819  t.remove(ID_C_volatile);
1820  #if 0
1821  std::cout << "ASSIGN " << id.identifier << " := "
1822  << cpp_typecheck.to_string(desired_type) << '\n';
1823  #endif
1824  }
1825  }
1826  }
1827  }
1828  }
1829  }
1830  else if(template_type.id()==ID_merged_type)
1831  {
1832  // look at subtypes
1833  for(const auto &t : to_merged_type(template_type).subtypes())
1834  {
1835  guess_template_args(t, desired_type);
1836  }
1837  }
1838  else if(is_reference(template_type) ||
1839  is_rvalue_reference(template_type))
1840  {
1841  guess_template_args(template_type.subtype(), desired_type);
1842  }
1843  else if(template_type.id()==ID_pointer)
1844  {
1845  if(desired_type.id() == ID_pointer)
1846  guess_template_args(template_type.subtype(), desired_type.subtype());
1847  }
1848  else if(template_type.id()==ID_array)
1849  {
1850  if(desired_type.id() == ID_array)
1851  {
1852  // look at subtype first
1853  guess_template_args(template_type.subtype(), desired_type.subtype());
1854 
1855  // size (e.g., buffer size guessing)
1857  to_array_type(template_type).size(),
1858  to_array_type(desired_type).size());
1859  }
1860  }
1861 }
1862 
1865  const exprt &expr,
1866  const cpp_typecheck_fargst &fargs)
1867 {
1868  typet tmp = cpp_typecheck.follow(expr.type());
1869 
1870  if(!tmp.get_bool(ID_is_template))
1871  return nil_exprt(); // not a template
1872 
1873  assert(expr.id()==ID_symbol);
1874 
1875  // a template is always a declaration
1876  const cpp_declarationt &cpp_declaration=
1877  to_cpp_declaration(tmp);
1878 
1879  // Class templates require explicit template arguments,
1880  // no guessing!
1881  if(cpp_declaration.is_class_template())
1882  return nil_exprt();
1883 
1884  // we need function arguments for guessing
1885  if(fargs.operands.empty())
1886  return nil_exprt(); // give up
1887 
1888  // We need to guess in the case of function templates!
1889 
1890  irep_idt template_identifier=
1892 
1893  const symbolt &template_symbol=
1894  cpp_typecheck.lookup(template_identifier);
1895 
1896  // alright, set up template arguments as 'unassigned'
1897 
1899 
1901  cpp_declaration.template_type());
1902 
1903  // there should be exactly one declarator
1904  assert(cpp_declaration.declarators().size()==1);
1905 
1906  const cpp_declaratort &function_declarator=
1907  cpp_declaration.declarators().front();
1908 
1909  // and that needs to have function type
1910  if(function_declarator.type().id()!=ID_function_type)
1911  {
1914  << "expected function type for function template"
1915  << messaget::eom;
1916  throw 0;
1917  }
1918 
1919  cpp_save_scopet cpp_saved_scope(cpp_typecheck.cpp_scopes);
1920 
1921  // we need the template scope
1922  cpp_scopet *template_scope=
1923  static_cast<cpp_scopet *>(
1924  cpp_typecheck.cpp_scopes.id_map[template_identifier]);
1925 
1926  if(template_scope==nullptr)
1927  {
1929  cpp_typecheck.error() << "template identifier: "
1930  << template_identifier << '\n'
1931  << "function template instantiation error"
1932  << messaget::eom;
1933  throw 0;
1934  }
1935 
1936  // enter the scope of the template
1937  cpp_typecheck.cpp_scopes.go_to(*template_scope);
1938 
1939  // walk through the function parameters
1940  const irept::subt &parameters=
1941  function_declarator.type().find(ID_parameters).get_sub();
1942 
1943  exprt::operandst::const_iterator it=fargs.operands.begin();
1944  for(const auto &parameter : parameters)
1945  {
1946  if(it==fargs.operands.end())
1947  break;
1948 
1949  if(parameter.id()==ID_cpp_declaration)
1950  {
1951  const cpp_declarationt &arg_declaration=
1952  to_cpp_declaration(parameter);
1953 
1954  // again, there should be one declarator
1955  assert(arg_declaration.declarators().size()==1);
1956 
1957  // turn into type
1958  typet arg_type=
1959  arg_declaration.declarators().front().
1960  merge_type(arg_declaration.type());
1961 
1962  // We only convert the arg_type,
1963  // and don't typecheck it -- that could cause all
1964  // sorts of trouble.
1966 
1967  guess_template_args(arg_type, it->type());
1968  }
1969 
1970  ++it;
1971  }
1972 
1973  // see if that has worked out
1974 
1975  cpp_template_args_tct template_args=
1977  cpp_declaration.template_type());
1978 
1979  if(template_args.has_unassigned())
1980  return nil_exprt(); // give up
1981 
1982  // Build the type of the function.
1983 
1984  typet function_type=
1985  function_declarator.merge_type(cpp_declaration.type());
1986 
1987  cpp_typecheck.typecheck_type(function_type);
1988 
1989  // Remember that this was a template
1990 
1991  function_type.set(ID_C_template, template_symbol.name);
1992  function_type.set(ID_C_template_arguments, template_args);
1993 
1994  // Seems we got an instance for all parameters. Let's return that.
1995 
1996  exprt template_function_instance(
1997  ID_template_function_instance, function_type);
1998 
1999  return template_function_instance;
2000 }
2001 
2003  exprt &expr,
2004  const cpp_template_args_non_tct &template_args_non_tc,
2005  const cpp_typecheck_fargst &fargs)
2006 {
2007  if(expr.id()!=ID_symbol)
2008  return; // templates are always symbols
2009 
2010  const symbolt &template_symbol =
2011  cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
2012 
2013  if(!template_symbol.type.get_bool(ID_is_template))
2014  return;
2015 
2016  #if 0
2017  if(template_args_non_tc.is_nil())
2018  {
2019  // no arguments, need to guess
2020  guess_function_template_args(expr, fargs);
2021  return;
2022  }
2023  #endif
2024 
2025  // We typecheck the template arguments in the context
2026  // of the original scope!
2027  cpp_template_args_tct template_args_tc;
2028 
2029  {
2031 
2033 
2034  template_args_tc=
2037  template_symbol,
2038  template_args_non_tc);
2039  // go back to where we used to be
2040  }
2041 
2042  // We never try 'unassigned' template arguments.
2043  if(template_args_tc.has_unassigned())
2044  UNREACHABLE;
2045 
2046  // a template is always a declaration
2047  const cpp_declarationt &cpp_declaration=
2048  to_cpp_declaration(template_symbol.type);
2049 
2050  // is it a class template or function template?
2051  if(cpp_declaration.is_class_template())
2052  {
2053  const symbolt &new_symbol=
2056  template_symbol,
2057  template_args_tc,
2058  template_args_tc);
2059 
2060  expr = type_exprt(struct_tag_typet(new_symbol.name));
2062  }
2063  else
2064  {
2065  // must be a function, maybe method
2066  const symbolt &new_symbol=
2069  template_symbol,
2070  template_args_tc,
2071  template_args_tc);
2072 
2073  // check if it is a method
2074  const code_typet &code_type=to_code_type(new_symbol.type);
2075 
2076  if(
2077  !code_type.parameters().empty() &&
2078  code_type.parameters().front().get_this())
2079  {
2080  // do we have an object?
2081  if(fargs.has_object)
2082  {
2083  const symbolt &type_symb=
2085  fargs.operands.begin()->type().get(ID_identifier));
2086 
2087  assert(type_symb.type.id()==ID_struct);
2088 
2089  const struct_typet &struct_type=
2090  to_struct_type(type_symb.type);
2091 
2092  DATA_INVARIANT(struct_type.has_component(new_symbol.name),
2093  "method should exist in struct");
2094 
2095  member_exprt member(
2096  *fargs.operands.begin(),
2097  new_symbol.name,
2098  code_type);
2100  expr.swap(member);
2101  return;
2102  }
2103  }
2104 
2105  expr=cpp_symbol_expr(new_symbol);
2107  }
2108 }
2109 
2111  const exprt &expr,
2112  unsigned &args_distance,
2113  const cpp_typecheck_fargst &fargs)
2114 {
2115  args_distance=0;
2116 
2117  if(expr.type().id()!=ID_code || !fargs.in_use)
2118  return true;
2119 
2120  const code_typet &type=to_code_type(expr.type());
2121 
2122  if(expr.id()==ID_member ||
2123  type.return_type().id() == ID_constructor)
2124  {
2125  // if it's a member, but does not have an object yet,
2126  // we add one
2127  if(!fargs.has_object)
2128  {
2129  const code_typet::parameterst &parameters=type.parameters();
2130  const code_typet::parametert &parameter=parameters.front();
2131 
2132  INVARIANT(parameter.get_this(), "first parameter should be `this'");
2133 
2134  if(type.return_type().id() == ID_constructor)
2135  {
2136  // it's a constructor
2137  const typet &object_type=parameter.type().subtype();
2138  symbol_exprt object(irep_idt(), object_type);
2139  object.set(ID_C_lvalue, true);
2140 
2141  cpp_typecheck_fargst new_fargs(fargs);
2142  new_fargs.add_object(object);
2143  return new_fargs.match(type, args_distance, cpp_typecheck);
2144  }
2145  else
2146  {
2147  if(
2148  expr.type().get_bool(ID_C_is_operator) &&
2149  fargs.operands.size() == parameters.size())
2150  {
2151  return fargs.match(type, args_distance, cpp_typecheck);
2152  }
2153 
2154  cpp_typecheck_fargst new_fargs(fargs);
2155  new_fargs.add_object(to_member_expr(expr).compound());
2156 
2157  return new_fargs.match(type, args_distance, cpp_typecheck);
2158  }
2159  }
2160  }
2161  else if(fargs.has_object)
2162  {
2163  // if it's not a member then we shall remove the object
2164  cpp_typecheck_fargst new_fargs(fargs);
2165  new_fargs.remove_object();
2166 
2167  return new_fargs.match(type, args_distance, cpp_typecheck);
2168  }
2169 
2170  return fargs.match(type, args_distance, cpp_typecheck);
2171 }
2172 
2174  cpp_scopest::id_sett &id_set)
2175 {
2176  cpp_scopest::id_sett new_set;
2177 
2178  // std::cout << "FILTER\n";
2179 
2180  // We only want scopes!
2181  for(const auto &id_ptr : id_set)
2182  {
2183  cpp_idt &id = *id_ptr;
2184 
2185  if(id.is_class() || id.is_enum() || id.is_namespace())
2186  {
2187  // std::cout << "X1\n";
2188  assert(id.is_scope);
2189  new_set.insert(&id);
2190  }
2191  else if(id.is_typedef())
2192  {
2193  // std::cout << "X2\n";
2194  irep_idt identifier=id.identifier;
2195 
2196  if(id.is_member)
2197  continue;
2198 
2199  while(true)
2200  {
2201  const symbolt &symbol=cpp_typecheck.lookup(identifier);
2202  assert(symbol.is_type);
2203 
2204  // todo? maybe do enum here, too?
2205  if(symbol.type.id()==ID_struct)
2206  {
2207  // this is a scope, too!
2208  cpp_idt &class_id=
2209  cpp_typecheck.cpp_scopes.get_id(identifier);
2210 
2211  assert(class_id.is_scope);
2212  new_set.insert(&class_id);
2213  break;
2214  }
2215  else
2216  break;
2217  }
2218  }
2219  else if(id.id_class==cpp_scopet::id_classt::TEMPLATE)
2220  {
2221  // std::cout << "X3\n";
2222  #if 0
2223  const symbolt &symbol=
2224  cpp_typecheck.lookup(id.identifier);
2225 
2226  // Template struct? Really needs arguments to be a scope!
2227  if(symbol.type.id() == ID_struct)
2228  {
2229  id.print(std::cout);
2230  assert(id.is_scope);
2231  new_set.insert(&id);
2232  }
2233  #endif
2234  }
2235  else if(id.id_class==cpp_scopet::id_classt::TEMPLATE_PARAMETER)
2236  {
2237  // std::cout << "X4\n";
2238  // a template parameter may evaluate to be a scope: it could
2239  // be instantiated with a class/struct/union/enum
2240  exprt e=cpp_typecheck.template_map.lookup(id.identifier);
2241 
2242  #if 0
2243  cpp_typecheck.template_map.print(std::cout);
2244  std::cout << "S: " << cpp_typecheck.cpp_scopes.current_scope().identifier
2245  << '\n';
2246  std::cout << "P: "
2248  << '\n';
2249  std::cout << "I: " << id.identifier << '\n';
2250  std::cout << "E: " << e.pretty() << '\n';
2251  #endif
2252 
2253  if(e.id()!=ID_type)
2254  continue; // expressions are definitively not a scope
2255 
2256  if(e.type().id() == ID_template_parameter_symbol_type)
2257  {
2258  auto type = to_template_parameter_symbol_type(e.type());
2259 
2260  while(true)
2261  {
2262  irep_idt identifier=type.get_identifier();
2263 
2264  const symbolt &symbol=cpp_typecheck.lookup(identifier);
2265  assert(symbol.is_type);
2266 
2267  if(symbol.type.id() == ID_template_parameter_symbol_type)
2268  type = to_template_parameter_symbol_type(symbol.type);
2269  else if(symbol.type.id()==ID_struct ||
2270  symbol.type.id()==ID_union ||
2271  symbol.type.id()==ID_c_enum)
2272  {
2273  // this is a scope, too!
2274  cpp_idt &class_id=
2275  cpp_typecheck.cpp_scopes.get_id(identifier);
2276 
2277  assert(class_id.is_scope);
2278  new_set.insert(&class_id);
2279  break;
2280  }
2281  else // give up
2282  break;
2283  }
2284  }
2285  }
2286  }
2287 
2288  id_set.swap(new_set);
2289 }
2290 
2292  cpp_scopest::id_sett &id_set)
2293 {
2294  // we only want namespaces
2295  for(cpp_scopest::id_sett::iterator
2296  it=id_set.begin();
2297  it!=id_set.end();
2298  ) // no it++
2299  {
2300  if((*it)->is_namespace())
2301  it++;
2302  else
2303  {
2304  cpp_scopest::id_sett::iterator old(it);
2305  it++;
2306  id_set.erase(old);
2307  }
2308  }
2309 }
2310 
2312  cpp_scopest::id_sett &id_set,
2313  const irep_idt &base_name,
2314  const cpp_typecheck_fargst &fargs)
2315 {
2316  // not clear what this is good for
2317  for(const auto &arg : fargs.operands)
2318  {
2319  const typet &final_type=cpp_typecheck.follow(arg.type());
2320 
2321  if(final_type.id()!=ID_struct && final_type.id()!=ID_union)
2322  continue;
2323 
2324  cpp_scopet &scope=
2325  cpp_typecheck.cpp_scopes.get_scope(final_type.get(ID_name));
2326  const auto tmp_set = scope.lookup(base_name, cpp_scopet::SCOPE_ONLY);
2327  id_set.insert(tmp_set.begin(), tmp_set.end());
2328  }
2329 }
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
unsignedbv_typet size_type()
Definition: c_types.cpp:58
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
bool get_this() const
Definition: std_types.h:600
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
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
const declaratorst & declarators() const
irep_idt get_specialization_of() const
bool is_class_template() const
template_typet & template_type()
cpp_template_args_non_tct & partial_specialization_args()
typet merge_type(const typet &declaration_type) const
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
bool is_member
Definition: cpp_id.h:42
exprt this_expr
Definition: cpp_id.h:76
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
void print(std::ostream &out, unsigned indent=0) const
Definition: cpp_id.cpp:31
bool is_constructor
Definition: cpp_id.h:43
bool is_method
Definition: cpp_id.h:42
bool is_static_member
Definition: cpp_id.h:42
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 has_template_args() const
Definition: cpp_name.h:124
void go_to_root_scope()
Definition: cpp_scopes.h:98
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_scopet & get_root_scope()
Definition: cpp_scopes.h:93
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_idt & get_id(const irep_idt &identifier)
Definition: cpp_scopes.h:72
std::set< cpp_idt * > id_sett
Definition: cpp_scopes.h:30
cpp_scopet & get_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:80
id_mapt id_map
Definition: cpp_scopes.h:68
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 is_root_scope() const
Definition: cpp_scope.h:77
exprt::operandst argumentst
exprt::operandst operands
bool match(const code_typet &code_type, unsigned &distance, cpp_typecheckt &cpp_typecheck) const
void add_object(const exprt &expr)
void remove_templates(resolve_identifierst &identifiers)
void filter(resolve_identifierst &identifiers, const wantt want)
exprt convert_template_parameter(const cpp_idt &id)
exprt convert_identifier(const cpp_idt &id, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_namespace(const cpp_namet &cpp_name)
std::vector< exprt > resolve_identifierst
cpp_typecheck_resolvet(class cpp_typecheckt &_cpp_typecheck)
void remove_duplicates(resolve_identifierst &identifiers)
void filter_for_namespaces(cpp_scopest::id_sett &id_set)
exprt resolve(const cpp_namet &cpp_name, const wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void resolve_argument(exprt &argument, const cpp_typecheck_fargst &fargs)
exprt do_builtin(const irep_idt &base_name, const cpp_typecheck_fargst &fargs, const cpp_template_args_non_tct &template_args)
void show_identifiers(const irep_idt &base_name, const resolve_identifierst &identifiers, std::ostream &out)
void filter_for_named_scopes(cpp_scopest::id_sett &id_set)
void make_constructors(resolve_identifierst &identifiers)
void guess_function_template_args(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
guess arguments of function templates
void convert_identifiers(const cpp_scopest::id_sett &id_set, const cpp_typecheck_fargst &fargs, resolve_identifierst &identifiers)
source_locationt source_location
void disambiguate_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void apply_template_args(resolve_identifierst &identifiers, const cpp_template_args_non_tct &template_args, const cpp_typecheck_fargst &fargs)
void resolve_with_arguments(cpp_scopest::id_sett &id_set, const irep_idt &base_name, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
struct_tag_typet disambiguate_template_classes(const irep_idt &base_name, const cpp_scopest::id_sett &id_set, const cpp_template_args_non_tct &template_args)
disambiguate partial specialization
cpp_typecheckt & cpp_typecheck
void exact_match_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void guess_template_args(const typet &template_parameter, const typet &desired_type)
void typecheck_type(typet &) override
instantiation_stackt instantiation_stack
template_mapt template_map
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void show_instantiation_stack(std::ostream &)
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
void elaborate_class_template(const typet &type)
elaborate class template instances
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
bool builtin_factory(const irep_idt &)
std::string to_string(const typet &) override
bool disable_access_control
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
cpp_scopest cpp_scopes
void typecheck_expr_member(exprt &) override
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
size_t size() const
Definition: dstring.h:104
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
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:383
subt & get_sub()
Definition: irep.h:467
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
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 make_nil()
Definition: irep.h:465
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
Extract member of struct or union.
Definition: std_expr.h:2613
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
message_handlert & get_message_handler()
Definition: message.h:184
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
const irep_idt & get_function() const
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
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 has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
bool is_macro
Definition: symbol.h:61
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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
const irep_idt & get_identifier() const
Definition: std_types.h:410
exprt lookup(const irep_idt &identifier) const
void build_unassigned(const template_typet &template_type)
void print(std::ostream &out) const
expr_mapt expr_map
Definition: template_map.h:32
type_mapt type_map
Definition: template_map.h:31
cpp_template_args_tct build_template_args(const template_typet &template_type) const
An expression denoting a type.
Definition: std_expr.h:2717
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
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
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:164
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
cpp_template_args_tct & to_cpp_template_args_tc(irept &irep)
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)
Cast a typet to a template_parameter_symbol_typet.
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
C++ Language Type Checking.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
literalt pos(literalt a)
Definition: literal.h:194
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition: merged_type.h:29
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:129
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:136
bool simplify(exprt &expr, const namespacet &ns)
#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
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
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
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
cpp_template_args_tct specialization_args