CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_template.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
12#include <util/base_exceptions.h> // IWYU pragma: keep
13#include <util/simplify_expr.h>
15
16#include "cpp_convert_type.h"
18#include "cpp_template_args.h"
19#include "cpp_template_type.h"
20#include "cpp_type2name.h"
21#include "cpp_typecheck.h"
22
26{
28 old_type.template_parameters();
30 new_type.template_parameters();
31
32 for(std::size_t i=0; i<new_parameters.size(); i++)
33 {
34 if(i<old_parameters.size() &&
35 old_parameters[i].has_default_argument() &&
36 !new_parameters[i].has_default_argument())
37 {
38 // TODO The default may depend on previous parameters!!
39 new_parameters[i].default_argument()=old_parameters[i].default_argument();
40 }
41 }
42}
43
45 cpp_declarationt &declaration)
46{
47 // Do template parameters. This also sets up the template scope.
50
51 typet &type=declaration.type();
52 template_typet &template_type=declaration.template_type();
53
54 bool has_body=type.find(ID_body).is_not_nil();
55
56 const cpp_namet &cpp_name=
57 static_cast<const cpp_namet &>(type.find(ID_tag));
58
59 if(cpp_name.is_nil())
60 {
62 error() << "class templates must not be anonymous" << eom;
63 throw 0;
64 }
65
66 if(!cpp_name.is_simple_name())
67 {
68 error().source_location=cpp_name.source_location();
69 error() << "simple name expected as class template tag" << eom;
70 throw 0;
71 }
72
73 irep_idt base_name=cpp_name.get_base_name();
74
75 const cpp_template_args_non_tct &partial_specialization_args=
76 declaration.partial_specialization_args();
77
80 base_name, template_type, partial_specialization_args);
81
82 #if 0
83 // Check if the name is already used by a different template
84 // in the same scope.
85 {
86 const auto id_set=
88 base_name,
91
92 if(!id_set.empty())
93 {
94 const symbolt &previous=lookup((*id_set.begin())->identifier);
95 if(previous.name!=symbol_name || id_set.size()>1)
96 {
97 error().source_location=cpp_name.source_location();
98 str << "template declaration of '" << base_name.c_str()
99 << " does not match previous declaration\n";
100 str << "location of previous definition: " << previous.location;
101 throw 0;
102 }
103 }
104 }
105 #endif
106
107 // check if we have it already
108
110 {
111 // there already
115
117 previous_declaration.type().find(ID_body).is_not_nil();
118
119 // check if we have 2 bodies
120 if(has_body && previous_has_body)
121 {
122 error().source_location=cpp_name.source_location();
123 error() << "template struct '" << base_name << "' defined previously\n"
124 << "location of previous definition: " << previous_symbol.location
125 << eom;
126 throw 0;
127 }
128
129 if(has_body)
130 {
131 // We replace the template!
132 // We have to retain any default parameters from the previous declaration.
134 previous_declaration.template_type(),
135 declaration.template_type());
136
137 previous_symbol.type.swap(declaration);
138
139 #if 0
140 std::cout << "*****\n";
141 std::cout << *cpp_scopes.id_map[symbol_name];
142 std::cout << "*****\n";
143 std::cout << "II: " << symbol_name << '\n';
144 #endif
145
146 // We also replace the template scope (the old one could be deleted).
148
149 // We also fix the parent scope in order to see the new
150 // template arguments
151 }
152 else
153 {
154 // just update any default arguments
156 declaration.template_type(),
157 previous_declaration.template_type());
158 }
159
160 INVARIANT(
161 cpp_scopes.id_map[symbol_name]->is_template_scope(),
162 "symbol should be in template scope");
163
164 return;
165 }
166
167 // it's not there yet
168
169 symbolt symbol{symbol_name, typet{}, ID_cpp};
170 symbol.base_name=base_name;
171 symbol.location=cpp_name.source_location();
172 symbol.module=module;
173 symbol.type.swap(declaration);
174 symbol.value = exprt(ID_template_decls);
175
176 symbol.pretty_name=
177 cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
178
179 symbolt *new_symbol;
180 if(symbol_table.move(symbol, new_symbol))
181 {
182 error().source_location=symbol.location;
183 error() << "cpp_typecheckt::typecheck_compound_type: "
184 << "symbol_table.move() failed"
185 << eom;
186 throw 0;
187 }
188
189 // put into current scope
190 cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
192 id.prefix=cpp_scopes.current_scope().prefix+
193 id2string(new_symbol->base_name);
194
195 // link the template symbol with the template scope
197
198 INVARIANT(
199 cpp_scopes.id_map[symbol_name]->is_template_scope(),
200 "symbol should be in template scope");
201}
202
205 cpp_declarationt &declaration)
206{
207 PRECONDITION(declaration.declarators().size() == 1);
208
209 cpp_declaratort &declarator=declaration.declarators()[0];
210 const cpp_namet &cpp_name = declarator.name();
211
212 // do template arguments
213 // this also sets up the template scope
216
217 if(!cpp_name.is_simple_name())
218 {
219 error().source_location=declaration.source_location();
220 error() << "function template must have simple name" << eom;
221 throw 0;
222 }
223
224 irep_idt base_name=cpp_name.get_base_name();
225
226 template_typet &template_type=declaration.template_type();
227
228 typet function_type=
229 declarator.merge_type(declaration.type());
230
232
235 base_name,
236 template_type,
237 function_type);
238
239 bool has_value=declarator.find(ID_value).is_not_nil();
240
241 // check if we have it already
242
244
246 {
248 .declarators()[0]
249 .find(ID_value)
250 .is_not_nil();
251
253 {
254 error().source_location=cpp_name.source_location();
255 error() << "function template symbol '" << base_name
256 << "' declared previously\n"
257 << "location of previous definition: "
258 << previous_symbol->location << eom;
259 throw 0;
260 }
261
262 if(has_value)
263 {
264 previous_symbol->type.swap(declaration);
266 }
267
268 // todo: the old template scope now is useless,
269 // and thus, we could delete it
270 return;
271 }
272
273 symbolt symbol{symbol_name, typet{}, ID_cpp};
274 symbol.base_name=base_name;
275 symbol.location=cpp_name.source_location();
276 symbol.module=module;
277 symbol.type.swap(declaration);
278 symbol.pretty_name=
279 cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
280
281 symbolt *new_symbol;
282 if(symbol_table.move(symbol, new_symbol))
283 {
284 error().source_location=symbol.location;
285 error() << "cpp_typecheckt::typecheck_compound_type: "
286 << "symbol_table.move() failed"
287 << eom;
288 throw 0;
289 }
290
291 // put into scope
292 cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
294 id.prefix=cpp_scopes.current_scope().prefix+
295 id2string(new_symbol->base_name);
296
297 // link the template symbol with the template scope
299 INVARIANT(
300 template_scope.is_template_scope(), "symbol should be in template scope");
301}
302
305 cpp_declarationt &declaration)
306{
307 PRECONDITION(declaration.declarators().size() == 1);
308
309 cpp_declaratort &declarator=declaration.declarators()[0];
310 const cpp_namet &cpp_name = declarator.name();
311
312 PRECONDITION(cpp_name.is_qualified() || cpp_name.has_template_args());
313
314 // must be of the form: name1<template_args>::name2
315 // or: name1<template_args>::operator X
316 if(cpp_name.get_sub().size()==4 &&
317 cpp_name.get_sub()[0].id()==ID_name &&
318 cpp_name.get_sub()[1].id()==ID_template_args &&
319 cpp_name.get_sub()[2].id()=="::" &&
320 cpp_name.get_sub()[3].id()==ID_name)
321 {
322 }
323 else if(cpp_name.get_sub().size()==5 &&
324 cpp_name.get_sub()[0].id()==ID_name &&
325 cpp_name.get_sub()[1].id()==ID_template_args &&
326 cpp_name.get_sub()[2].id()=="::" &&
327 cpp_name.get_sub()[3].id()==ID_operator)
328 {
329 }
330 else
331 {
332 return; // TODO
333
334#if 0
335 error().source_location=cpp_name.source_location();
336 error() << "bad template name" << eom;
337 throw 0;
338#endif
339 }
340
341 // let's find the class template this function template belongs to.
342 const auto id_set = cpp_scopes.current_scope().lookup(
343 cpp_name.get_sub().front().get(ID_identifier),
344 cpp_scopet::SCOPE_ONLY, // look only in current scope
345 cpp_scopet::id_classt::TEMPLATE); // must be template
346
347 if(id_set.empty())
348 {
350 error().source_location=cpp_name.source_location();
351 error() << "class template '"
352 << cpp_name.get_sub().front().get(ID_identifier) << "' not found"
353 << eom;
354 throw 0;
355 }
356 else if(id_set.size()>1)
357 {
358 error().source_location=cpp_name.source_location();
359 error() << "class template '"
360 << cpp_name.get_sub().front().get(ID_identifier) << "' is ambiguous"
361 << eom;
362 throw 0;
363 }
364 else if((*(id_set.begin()))->id_class!=cpp_idt::id_classt::TEMPLATE)
365 {
366 // std::cerr << *(*id_set.begin()) << '\n';
367 error().source_location=cpp_name.source_location();
368 error() << "class template '"
369 << cpp_name.get_sub().front().get(ID_identifier)
370 << "' is not a template" << eom;
371 throw 0;
372 }
373
374 const cpp_idt &cpp_id=**(id_set.begin());
376
378 static_cast<exprt &>(template_symbol.value.add(ID_template_methods));
379
380 template_methods.copy_to_operands(declaration);
381
382 // save current scope
384
385 const irept &instantiated_with =
387
388 for(std::size_t i=0; i<instantiated_with.get_sub().size(); i++)
389 {
391 static_cast<const cpp_template_args_tct &>(
392 instantiated_with.get_sub()[i]);
393
394 cpp_declarationt decl_tmp=declaration;
395
396 // do template arguments
397 // this also sets up the template scope of the method
400
402
403 // mapping from template arguments to values/types
405
407 decl_tmp.remove(ID_is_template);
408
410 cpp_saved_scope.restore();
411 }
412}
413
415 const irep_idt &base_name,
416 const template_typet &template_type,
417 const cpp_template_args_non_tct &partial_specialization_args)
418{
419 std::string identifier=
421 "template."+id2string(base_name) + "<";
422
423 int counter=0;
424
425 // these are probably not needed -- templates
426 // should be unique in a namespace
427 for(template_typet::template_parameterst::const_iterator
428 it=template_type.template_parameters().begin();
429 it!=template_type.template_parameters().end();
430 it++)
431 {
432 if(counter!=0)
433 identifier+=',';
434
435 if(it->id()==ID_type)
436 identifier+="Type"+std::to_string(counter);
437 else
438 identifier+="Non_Type"+std::to_string(counter);
439
440 counter++;
441 }
442
443 identifier += ">";
444
445 if(!partial_specialization_args.arguments().empty())
446 {
447 identifier+="_specialized_to_<";
448
449 counter=0;
450 for(cpp_template_args_non_tct::argumentst::const_iterator
451 it=partial_specialization_args.arguments().begin();
452 it!=partial_specialization_args.arguments().end();
453 it++, counter++)
454 {
455 if(counter!=0)
456 identifier+=',';
457
458 // These are not yet typechecked, as they may depend
459 // on unassigned template parameters.
460
461 if(it->id() == ID_type || it->id() == ID_ambiguous)
462 identifier+=cpp_type2name(it->type());
463 else
464 identifier+=cpp_expr2name(*it);
465 }
466
467 identifier+='>';
468 }
469
470 return identifier;
471}
472
474 const irep_idt &base_name,
475 const template_typet &template_type,
476 const typet &function_type)
477{
478 // we first build something without function arguments
479 cpp_template_args_non_tct partial_specialization_args;
480 std::string identifier=
481 class_template_identifier(base_name, template_type,
482 partial_specialization_args);
483
484 // we must also add the signature of the function to the identifier
485 identifier+=cpp_type2name(function_type);
486
487 return identifier;
488}
489
491 cpp_declarationt &declaration)
492{
493 cpp_save_scopet saved_scope(cpp_scopes);
494
495 typet &type=declaration.type();
496
497 PRECONDITION(type.id() == ID_struct);
498
500 static_cast<cpp_namet &>(type.add(ID_tag));
501
502 if(cpp_name.is_qualified())
503 {
504 error().source_location=cpp_name.source_location();
505 error() << "qualifiers not expected here" << eom;
506 throw 0;
507 }
508
509 if(cpp_name.get_sub().size()!=2 ||
510 cpp_name.get_sub()[0].id()!=ID_name ||
511 cpp_name.get_sub()[1].id()!=ID_template_args)
512 {
513 // currently we are more restrictive
514 // than the standard
515 error().source_location=cpp_name.source_location();
516 error() << "bad template-class-specialization name" << eom;
517 throw 0;
518 }
519
520 irep_idt base_name=
521 cpp_name.get_sub()[0].get(ID_identifier);
522
523 // copy the template arguments
526
527 // Remove the template arguments from the name.
528 cpp_name.get_sub().pop_back();
529
530 // get the template symbol
531
534
535 // remove any specializations
536 for(cpp_scopest::id_sett::iterator
537 it=id_set.begin();
538 it!=id_set.end();
539 ) // no it++
540 {
541 cpp_scopest::id_sett::iterator next=it;
542 next++;
543
544 if(lookup((*it)->identifier).type.find(ID_specialization_of).is_not_nil())
545 id_set.erase(it);
546
547 it=next;
548 }
549
550 // only one should be left
551 if(id_set.empty())
552 {
554 error() << "class template '" << base_name << "' not found" << eom;
555 throw 0;
556 }
557 else if(id_set.size()>1)
558 {
560 error() << "class template '" << base_name << "' is ambiguous" << eom;
561 throw 0;
562 }
563
564 symbol_table_baset::symbolst::const_iterator s_it =
565 symbol_table.symbols.find((*id_set.begin())->identifier);
566
568
569 const symbolt &template_symbol=s_it->second;
570
571 if(!template_symbol.type.get_bool(ID_is_template))
572 {
574 error() << "expected a template" << eom;
575 }
576
577 #if 0
578 // is this partial specialization?
579 if(declaration.template_type().parameters().empty())
580 {
581 // typecheck arguments -- these are for the 'primary' template!
584 declaration.source_location(),
587
588 // Full specialization, i.e., template<>.
589 // We instantiate.
591 cpp_name.source_location(),
594 type);
595 }
596 else // NOLINT(readability/braces)
597 #endif
598
599 {
600 // partial specialization -- we typecheck
602 declaration.set_specialization_of(template_symbol.name);
603
604 typecheck_class_template(declaration);
605 }
606}
607
609 cpp_declarationt &declaration)
610{
611 cpp_save_scopet saved_scope(cpp_scopes);
612
613 if(declaration.declarators().size()!=1 ||
614 declaration.declarators().front().type().id()!=ID_function_type)
615 {
616 error().source_location=declaration.type().source_location();
617 error() << "expected function template specialization" << eom;
618 throw 0;
619 }
620
621 PRECONDITION(declaration.declarators().size() == 1);
622 cpp_declaratort declarator=declaration.declarators().front();
623 cpp_namet &cpp_name=declarator.name();
624
625 // There is specialization (instantiation with template arguments)
626 // but also function overloading (no template arguments)
627
628 PRECONDITION(!cpp_name.get_sub().empty());
629
630 if(cpp_name.get_sub().back().id()==ID_template_args)
631 {
632 // proper specialization with arguments
633 if(cpp_name.get_sub().size()!=2 ||
634 cpp_name.get_sub()[0].id()!=ID_name ||
635 cpp_name.get_sub()[1].id()!=ID_template_args)
636 {
637 // currently we are more restrictive
638 // than the standard
639 error().source_location=cpp_name.source_location();
640 error() << "bad template-function-specialization name" << eom;
641 throw 0;
642 }
643
644 std::string base_name=
645 cpp_name.get_sub()[0].get(ID_identifier).c_str();
646
647 const auto id_set =
649
650 if(id_set.empty())
651 {
652 error().source_location=cpp_name.source_location();
653 error() << "template function '" << base_name << "' not found" << eom;
654 throw 0;
655 }
656 else if(id_set.size()>1)
657 {
658 error().source_location=cpp_name.source_location();
659 error() << "template function '" << base_name << "' is ambiguous" << eom;
660 throw 0;
661 }
662
664 lookup((*id_set.begin())->identifier);
665
668 declaration.source_location(),
671
672 cpp_name.get_sub().pop_back();
673
675 specialization.swap(declarator);
676
678 cpp_name.source_location(),
683 }
684 else
685 {
686 // Just overloading, but this is still a template
687 // for disambiguation purposes!
688 // http://www.gotw.ca/publications/mill17.htm
690
693 new_declaration.set(ID_C_template, ""); // todo, get identifier
694
696 }
697}
698
700 template_typet &type)
701{
703
704 PRECONDITION(type.id() == ID_template);
705
706 std::string id_suffix="template::"+std::to_string(template_counter++);
707
708 // produce a new scope for the template parameters
711
713
714 // put template parameters into this scope
716 type.template_parameters();
717
718 unsigned anon_count=0;
719
720 for(template_typet::template_parameterst::iterator
721 it=parameters.begin();
722 it!=parameters.end();
723 it++)
724 {
725 exprt &parameter=*it;
726
727 cpp_declarationt declaration;
728 declaration.swap(static_cast<cpp_declarationt &>(parameter));
729
731
732 // there must be _one_ declarator
733 PRECONDITION(declaration.declarators().size() == 1);
734
735 cpp_declaratort &declarator=declaration.declarators().front();
736
737 // it may be anonymous
738 if(declarator.name().is_nil())
739 declarator.name() = cpp_namet("anon#" + std::to_string(++anon_count));
740
741 #if 1
742 // The declarator needs to be just a name
743 if(declarator.name().get_sub().size()!=1 ||
744 declarator.name().get_sub().front().id()!=ID_name)
745 {
746 error().source_location=declaration.source_location();
747 error() << "template parameter must be simple name" << eom;
748 throw 0;
749 }
750
752
753 irep_idt base_name=declarator.name().get_sub().front().get(ID_identifier);
754 irep_idt identifier=scope.prefix+id2string(base_name);
755
756 // add to scope
757 cpp_idt &id=scope.insert(base_name);
758 id.identifier=identifier;
760
761 // is it a type or not?
762 if(declaration.get_bool(ID_is_type))
763 {
765 parameter.type().add_source_location()=declaration.find_source_location();
766 }
767 else
768 {
769 // The type is not checked, as it might depend
770 // on earlier parameters.
771 parameter = symbol_exprt(identifier, declaration.type());
772 }
773
774 // There might be a default type or default value.
775 // We store it for later, as it can't be typechecked now
776 // because of possible dependencies on earlier parameters!
777 if(declarator.value().is_not_nil())
778 parameter.add(ID_C_default_value)=declarator.value();
779
780 #else
781 // is it a type or not?
782 cpp_declarator_converter.is_typedef=declaration.get_bool(ID_is_type);
783
784 // say it a template parameter
785 cpp_declarator_converter.is_template_parameter=true;
786
787 // There might be a default type or default value.
788 // We store it for later, as it can't be typechecked now
789 // because of possible dependencies on earlier parameters!
790 exprt default_value=declarator.value();
791 declarator.value().make_nil();
792
793 const symbolt &symbol=
794 cpp_declarator_converter.convert(declaration, declarator);
795
796 if(cpp_declarator_converter.is_typedef)
797 {
799 parameter.type().add_source_location()=declaration.find_location();
800 }
801 else
802 parameter=symbol.symbol_expr();
803
804 // set (non-typechecked) default value
805 if(default_value.is_not_nil())
806 parameter.add(ID_C_default_value)=default_value;
807
808 parameter.add_source_location()=declaration.find_location();
809 #endif
810 }
811
812 return template_scope;
813}
814
818 const source_locationt &source_location,
821{
822 // old stuff
824
826
827 const template_typet &template_type=
829
830 // bad re-cast, but better than copying the args one by one
833
835 result.arguments();
836
837 const template_typet::template_parameterst &parameters=
838 template_type.template_parameters();
839
840 if(parameters.size()<args.size())
841 {
842 error().source_location=source_location;
843 error() << "too many template arguments (expected "
844 << parameters.size() << ", but got "
845 << args.size() << ")" << eom;
846 throw 0;
847 }
848
849 // we will modify the template map
852
853 // check for default arguments
854 for(std::size_t i=0; i<parameters.size(); i++)
855 {
856 const template_parametert &parameter=parameters[i];
858
859 if(i>=args.size())
860 {
861 // Check for default argument for the parameter.
862 // These may depend on previous arguments.
863 if(!parameter.has_default_argument())
864 {
865 error().source_location=source_location;
866 error() << "not enough template arguments (expected "
867 << parameters.size() << ", but got " << args.size()
868 << ")" << eom;
869 throw 0;
870 }
871
872 args.push_back(parameter.default_argument());
873
874 // these need to be typechecked in the scope of the template,
875 // not in the current scope!
878 template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
880 }
881
882 DATA_INVARIANT(i < args.size(), "i must be in bounds");
883
884 exprt &arg=args[i];
885
886 if(parameter.id()==ID_type)
887 {
888 if(arg.id()==ID_type)
889 {
890 typecheck_type(arg.type());
891 }
892 else if(arg.id() == ID_ambiguous)
893 {
894 typecheck_type(arg.type());
895 typet t=arg.type();
896 arg=exprt(ID_type, t);
897 }
898 else
899 {
901 error() << "expected type, but got expression" << eom;
902 throw 0;
903 }
904 }
905 else // expression
906 {
907 if(arg.id()==ID_type)
908 {
910 error() << "expected expression, but got type" << eom;
911 throw 0;
912 }
913 else if(arg.id() == ID_ambiguous)
914 {
915 exprt e;
916 e.swap(arg.type());
917 arg.swap(e);
918 }
919
920 typet type=parameter.type();
921
922 // First check the parameter type (might have earlier
923 // type parameters in it). Needs to be checked in scope
924 // of template.
925 {
929 template_scope!=nullptr,
931 "template_scope is null");
933 typecheck_type(type);
934 }
935
936 // Now check the argument to match that.
937 typecheck_expr(arg);
938 simplify(arg, *this);
939 implicit_typecast(arg, type);
940 }
941
942 // Set right away -- this is for the benefit of default
943 // arguments and later parameters whose type might
944 // depend on an earlier parameter.
945
947 }
948
949 // restore template map
951
952 // now the numbers should match
954 args.size() == parameters.size(),
955 "argument and parameter numbers must match");
956
957 return result;
958}
959
961 cpp_declarationt &declaration)
962{
963 PRECONDITION(declaration.is_template());
964
965 if(declaration.member_spec().is_virtual())
966 {
967 error().source_location=declaration.source_location();
968 error() << "invalid use of 'virtual' in template declaration"
969 << eom;
970 throw 0;
971 }
972
973 if(declaration.is_typedef())
974 {
975 error().source_location=declaration.source_location();
976 error() << "template declaration for typedef" << eom;
977 throw 0;
978 }
979
980 typet &type=declaration.type();
981
982 // there are
983 // 1) function templates
984 // 2) class templates
985 // 3) template members of class templates (static or methods)
986 // 4) variable templates (C++14)
987
988 if(declaration.is_class_template())
989 {
990 // there should not be declarators
991 if(!declaration.declarators().empty())
992 {
993 error().source_location=declaration.source_location();
994 error() << "class template not expected to have declarators"
995 << eom;
996 throw 0;
997 }
998
999 // it needs to be a class template
1000 if(type.id()!=ID_struct)
1001 {
1002 error().source_location=declaration.source_location();
1003 error() << "expected class template" << eom;
1004 throw 0;
1005 }
1006
1007 // Is it class template specialization?
1008 // We can tell if there are template arguments in the class name,
1009 // like template<...> class tag<stuff> ...
1010 if((static_cast<const cpp_namet &>(
1011 type.find(ID_tag))).has_template_args())
1012 {
1014 return;
1015 }
1016
1017 typecheck_class_template(declaration);
1018 return;
1019 }
1020 // maybe function template, maybe class template member, maybe
1021 // template variable
1022 else
1023 {
1024 // there should be declarators in either case
1025 if(declaration.declarators().empty())
1026 {
1027 error().source_location=declaration.source_location();
1028 error() << "non-class template is expected to have a declarator"
1029 << eom;
1030 throw 0;
1031 }
1032
1033 // Is it function template specialization?
1034 // Only full specialization is allowed!
1035 if(declaration.template_type().template_parameters().empty())
1036 {
1038 return;
1039 }
1040
1041 // Explicit qualification is forbidden for function templates,
1042 // which we can use to distinguish them.
1043
1045 declaration.declarators().size() >= 1, "declarator required");
1046
1047 cpp_declaratort &declarator=declaration.declarators()[0];
1048 const cpp_namet &cpp_name = declarator.name();
1049
1050 if(cpp_name.is_qualified() ||
1051 cpp_name.has_template_args())
1052 return typecheck_class_template_member(declaration);
1053
1054 // must be function template
1055 typecheck_function_template(declaration);
1056 return;
1057 }
1058}
Generic exception types primarily designed for use with invariants.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
symbol_table_baset & symbol_table
const declaratorst & declarators() const
const cpp_member_spect & member_spec() const
void set_specialization_of(const irep_idt &id)
bool is_template() const
bool is_class_template() const
cpp_template_args_non_tct & partial_specialization_args()
template_typet & template_type()
bool is_typedef() const
typet merge_type(const typet &declaration_type) const
cpp_namet & name()
irep_idt identifier
Definition cpp_id.h:72
std::string prefix
Definition cpp_id.h:79
id_classt id_class
Definition cpp_id.h:45
void go_to(cpp_idt &id)
Definition cpp_scopes.h:103
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
id_mapt id_map
Definition cpp_scopes.h:68
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
cpp_idt & insert(const irep_idt &_base_name)
Definition cpp_scope.h:52
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition cpp_scope.h:32
exprt::operandst argumentst
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
void typecheck_type(typet &) override
template_mapt template_map
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
void convert_template_declaration(cpp_declarationt &declaration)
void implicit_typecast(exprt &expr, const typet &type) override
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
void convert_non_template_declaration(cpp_declarationt &declaration)
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
unsigned template_counter
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
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 convert(cpp_linkage_spect &)
void typecheck_expr(exprt &) override
cpp_scopet & typecheck_template_parameters(template_typet &type)
void typecheck_class_template(cpp_declarationt &declaration)
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{})
cpp_scopest cpp_scopes
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void convert_class_template_specialization(cpp_declarationt &declaration)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
const char * c_str() const
Definition dstring.h:116
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
bool is_not_nil() const
Definition irep.h:372
subt & get_sub()
Definition irep.h:448
void make_nil()
Definition irep.h:446
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
bool is_nil() const
Definition irep.h:368
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & result() const
Definition message.h:401
static eomt eom
Definition message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Expression to hold a symbol (variable)
Definition std_expr.h:131
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void set(const template_parametert &parameter, const exprt &value)
void swap(template_mapt &template_map)
template_parameterst & template_parameters()
std::vector< template_parametert > template_parameterst
An expression denoting a type.
Definition std_expr.h:3081
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
C++ Language Type Checking.
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
std::string cpp_type2name(const typet &type)
std::string cpp_expr2name(const exprt &expr)
C++ Language Module.
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool simplify(exprt &expr, const namespacet &ns)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
a template parameter symbol that is a type
Author: Diffblue Ltd.