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