cprover
Loading...
Searching...
No Matches
cpp_typecheck_resolve.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
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>
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";
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 {
287 to_struct_union_type(object_type),
288 identifier.identifier,
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
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:
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
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
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
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);
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
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;
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
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 =
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())
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)
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:68
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
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:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
bool has_ellipsis() const
Definition: std_types.h:611
const declaratorst & declarators() const
irep_idt get_specialization_of() const
bool is_class_template() const
cpp_template_args_non_tct & partial_specialization_args()
template_typet & template_type()
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
bool has_template_args() const
Definition: cpp_name.h:124
const source_locationt & source_location() const
Definition: cpp_name.h:73
void go_to_root_scope()
Definition: cpp_scopes.h:98
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_idt & get_id(const irep_idt &identifier)
Definition: cpp_scopes.h:72
std::set< cpp_idt * > id_sett
Definition: cpp_scopes.h:30
id_mapt id_map
Definition: cpp_scopes.h:68
cpp_scopet & get_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:80
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & get_root_scope()
Definition: cpp_scopes.h:93
cpp_scopet & get_parent() const
Definition: cpp_scope.h:88
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
@ 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
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Extract member of struct or union.
Definition: std_expr.h:2667
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
mstreamt & warning() const
Definition: message.h:404
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:2874
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 componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
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:2771
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
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_non_tct & to_cpp_template_args_non_tc(irept &irep)
cpp_template_args_tct & to_cpp_template_args_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:47
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:137
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:144
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
cpp_template_args_tct specialization_args