cprover
cpp_instantiate_template.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/arith_tools.h>
19 #include <util/base_exceptions.h>
20 #include <util/simplify_expr.h>
21 
22 #include <util/c_types.h>
23 
24 #include "cpp_type2name.h"
25 
27  const cpp_template_args_tct &template_args)
28 {
29  // quick hack
30  std::string result="<";
31  bool first=true;
32 
33  const cpp_template_args_tct::argumentst &arguments=
34  template_args.arguments();
35 
36  for(const auto &expr : arguments)
37  {
38  if(first)
39  first=false;
40  else
41  result+=',';
42 
44  expr.id() != ID_ambiguous, "template argument must not be ambiguous");
45 
46  if(expr.id()==ID_type)
47  {
48  const typet &type=expr.type();
49  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
50  result += id2string(to_tag_type(type).get_identifier());
51  else
52  result+=cpp_type2name(type);
53  }
54  else // expression
55  {
56  exprt e=expr;
57 
58  if(e.id() == ID_symbol)
59  {
60  const symbol_exprt &s = to_symbol_expr(e);
61  const symbolt &symbol = lookup(s.get_identifier());
62 
63  if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
64  e = symbol.value;
65  }
66 
67  make_constant(e);
68 
69  // this must be a constant, which includes true/false
70  mp_integer i;
71 
72  if(e.is_true())
73  i=1;
74  else if(e.is_false())
75  i=0;
76  else if(to_integer(to_constant_expr(e), i))
77  {
78  error().source_location = expr.find_source_location();
79  error() << "template argument expression expected to be "
80  << "scalar constant, but got '" << to_string(e) << "'" << eom;
81  throw 0;
82  }
83 
85  }
86  }
87 
88  result+='>';
89 
90  return result;
91 }
92 
94 {
95  for(const auto &e : instantiation_stack)
96  {
97  const symbolt &symbol = lookup(e.identifier);
98  out << "instantiating '" << symbol.pretty_name << "' with <";
99 
100  forall_expr(a_it, e.full_template_args.arguments())
101  {
102  if(a_it != e.full_template_args.arguments().begin())
103  out << ", ";
104 
105  if(a_it->id()==ID_type)
106  out << to_string(a_it->type());
107  else
108  out << to_string(*a_it);
109  }
110 
111  out << "> at " << e.source_location << '\n';
112  }
113 }
114 
117  cpp_scopet &template_scope,
118  const std::string &suffix)
119 {
120  cpp_scopet::id_sett id_set =
121  template_scope.lookup(suffix, cpp_scopet::SCOPE_ONLY);
122 
123  CHECK_RETURN(id_set.size() <= 1);
124 
125  if(id_set.size() == 1)
126  {
127  cpp_idt &cpp_id = **id_set.begin();
129 
130  return static_cast<cpp_scopet &>(cpp_id);
131  }
132  else
133  {
134  cpp_scopet &sub_scope = template_scope.new_scope(suffix);
136  sub_scope.prefix = template_scope.get_parent().prefix;
137  sub_scope.suffix = suffix;
138  sub_scope.add_using_scope(template_scope.get_parent());
139 
140  const std::string subscope_name =
141  id2string(template_scope.identifier) + suffix;
142  cpp_scopes.id_map.insert(
143  cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
144 
145  return sub_scope;
146  }
147 }
148 
150  const source_locationt &source_location,
151  const symbolt &template_symbol,
152  const cpp_template_args_tct &specialization_template_args,
153  const cpp_template_args_tct &full_template_args)
154 {
155  // we should never get 'unassigned' here
156  assert(!full_template_args.has_unassigned());
157 
158  // do we have args?
159  if(full_template_args.arguments().empty())
160  {
161  error().source_location=source_location;
162  error() << "'" << template_symbol.base_name
163  << "' is a template; thus, expected template arguments" << eom;
164  throw 0;
165  }
166 
167  // produce new symbol name
168  std::string suffix=template_suffix(full_template_args);
169 
170  cpp_scopet *template_scope=
171  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
172 
174  template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
175 
176  irep_idt identifier = id2string(template_scope->get_parent().prefix) +
177  "tag-" + id2string(template_symbol.base_name) +
178  id2string(suffix);
179 
180  // already there?
181  symbol_tablet::symbolst::const_iterator s_it=
182  symbol_table.symbols.find(identifier);
183  if(s_it!=symbol_table.symbols.end())
184  return s_it->second;
185 
186  // Create as incomplete struct, but mark as
187  // "template_class_instance", to be elaborated later.
188  symbolt new_symbol;
189  new_symbol.name=identifier;
190  new_symbol.pretty_name=template_symbol.pretty_name;
191  new_symbol.location=template_symbol.location;
192  new_symbol.type = struct_typet();
193  to_struct_type(new_symbol.type).make_incomplete();
194  new_symbol.type.set(ID_tag, template_symbol.type.find(ID_tag));
195  if(template_symbol.type.get_bool(ID_C_class))
196  new_symbol.type.set(ID_C_class, true);
197  new_symbol.type.set(ID_template_class_instance, true);
198  new_symbol.type.add_source_location()=template_symbol.location;
199  new_symbol.type.set(
200  ID_specialization_template_args, specialization_template_args);
201  new_symbol.type.set(ID_full_template_args, full_template_args);
202  new_symbol.type.set(ID_identifier, template_symbol.name);
203  new_symbol.mode=template_symbol.mode;
204  new_symbol.base_name=template_symbol.base_name;
205  new_symbol.is_type=true;
206 
207  symbolt *s_ptr;
208  symbol_table.move(new_symbol, s_ptr);
209 
210  // put into template scope
211  cpp_idt &id=cpp_scopes.put_into_scope(*s_ptr, *template_scope);
212 
214  id.is_scope=true;
215  id.prefix = template_scope->get_parent().prefix +
216  id2string(s_ptr->base_name) + id2string(suffix) + "::";
217  id.class_identifier=s_ptr->name;
218  id.id_class=cpp_idt::id_classt::CLASS;
219 
220  return *s_ptr;
221 }
222 
225  const typet &type)
226 {
227  if(type.id() != ID_struct_tag)
228  return;
229 
230  const symbolt &symbol = lookup(to_struct_tag_type(type));
231 
232  // Make a copy, as instantiate will destroy the symbol type!
233  const typet t_type=symbol.type;
234 
235  if(t_type.id() == ID_struct && t_type.get_bool(ID_template_class_instance))
236  {
238  type.source_location(),
239  lookup(t_type.get(ID_identifier)),
240  static_cast<const cpp_template_args_tct &>(
241  t_type.find(ID_specialization_template_args)),
242  static_cast<const cpp_template_args_tct &>(
243  t_type.find(ID_full_template_args)));
244  }
245 }
246 
251 #define MAX_DEPTH 50
252 
254  const source_locationt &source_location,
255  const symbolt &template_symbol,
256  const cpp_template_args_tct &specialization_template_args,
257  const cpp_template_args_tct &full_template_args,
258  const typet &specialization)
259 {
260 #ifdef DEBUG
261  std::cout << "instantiate_template: " << template_symbol.name << '\n';
262 #endif
263 
264  if(instantiation_stack.size()==MAX_DEPTH)
265  {
266  error().source_location=source_location;
267  error() << "reached maximum template recursion depth ("
268  << MAX_DEPTH << ")" << eom;
269  throw 0;
270  }
271 
273  instantiation_stack.back().source_location=source_location;
274  instantiation_stack.back().identifier=template_symbol.name;
275  instantiation_stack.back().full_template_args=full_template_args;
276 
277 #ifdef DEBUG
278  std::cout << "L: " << source_location << '\n';
279  std::cout << "I: " << template_symbol.name << '\n';
280 #endif
281 
283 
284  bool specialization_given=specialization.is_not_nil();
285 
286  // we should never get 'unassigned' here
287  assert(!specialization_template_args.has_unassigned());
288  assert(!full_template_args.has_unassigned());
289 
290 #ifdef DEBUG
291  std::cout << "A: <";
292  forall_expr(it, specialization_template_args.arguments())
293  {
294  if(it!=specialization_template_args.arguments().begin())
295  std::cout << ", ";
296  if(it->id()==ID_type)
297  std::cout << to_string(it->type());
298  else
299  std::cout << to_string(*it);
300  }
301  std::cout << ">\n\n";
302 #endif
303 
304  // do we have arguments?
305  if(full_template_args.arguments().empty())
306  {
307  error().source_location=source_location;
308  error() << "'" << template_symbol.base_name
309  << "' is a template; thus, expected template arguments" << eom;
310  throw 0;
311  }
312 
313  // produce new symbol name
314  std::string suffix=template_suffix(full_template_args);
315 
316  // we need the template scope to see the template parameters
317  cpp_scopet *template_scope=
318  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
319 
320  if(template_scope==nullptr)
321  {
322  error().source_location=source_location;
323  error() << "identifier: " << template_symbol.name << '\n'
324  << "template instantiation error: scope not found" << eom;
325  throw 0;
326  }
327 
328  // produce new declaration
329  cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
330 
331  // The new one is not a template any longer, but we remember the
332  // template type that was used.
333  template_typet template_type=new_decl.template_type();
334  new_decl.remove(ID_is_template);
335  new_decl.remove(ID_template_type);
336  new_decl.set(ID_C_template, template_symbol.name);
337  new_decl.set(ID_C_template_arguments, specialization_template_args);
338 
339  // save old scope
340  cpp_save_scopet saved_scope(cpp_scopes);
341 
342  // mapping from template parameters to values/types
343  template_map.build(template_type, specialization_template_args);
344 
345  // enter the template scope
346  cpp_scopes.go_to(*template_scope);
347 
348  // Is it a template method?
349  // It's in the scope of a class, and not a class itself.
350  bool is_template_method=
352  new_decl.type().id()!=ID_struct;
353 
354  irep_idt class_name;
355 
356  if(is_template_method)
358 
359  // sub-scope for fixing the prefix
360  cpp_scopet &sub_scope = sub_scope_for_instantiation(*template_scope, suffix);
361 
362  // let's see if we have the instance already
363  {
364  cpp_scopet::id_sett id_set =
365  sub_scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
366 
367  if(id_set.size()==1)
368  {
369  // It has already been instantiated!
370  const cpp_idt &cpp_id = **id_set.begin();
371 
372  assert(cpp_id.id_class == cpp_idt::id_classt::CLASS ||
374 
375  const symbolt &symb=lookup(cpp_id.identifier);
376 
377  // continue if the type is incomplete only
378  if(cpp_id.id_class==cpp_idt::id_classt::CLASS &&
379  symb.type.id()==ID_struct)
380  return symb;
381  else if(symb.value.is_not_nil())
382  return symb;
383  }
384 
385  cpp_scopes.go_to(sub_scope);
386  }
387 
388  // store the information that the template has
389  // been instantiated using these arguments
390  {
391  // need non-const handle on template symbol
392  symbolt &s = symbol_table.get_writeable_ref(template_symbol.name);
393  irept &instantiated_with = s.value.add(ID_instantiated_with);
394  instantiated_with.get_sub().push_back(specialization_template_args);
395  }
396 
397  #ifdef DEBUG
398  std::cout << "CLASS MAP:\n";
399  template_map.print(std::cout);
400  #endif
401 
402  // fix the type
403  {
404  typet declaration_type=new_decl.type();
405 
406  // specialization?
407  if(specialization_given)
408  {
409  if(declaration_type.id()==ID_struct)
410  {
411  declaration_type=specialization;
412  declaration_type.add_source_location()=source_location;
413  }
414  else
415  {
416  irept tmp=specialization;
417  new_decl.declarators()[0].swap(tmp);
418  }
419  }
420 
421  template_map.apply(declaration_type);
422  new_decl.type().swap(declaration_type);
423  }
424 
425  if(new_decl.type().id()==ID_struct)
426  {
427  // a class template
429 
430  // also instantiate all the template methods
431  const exprt &template_methods = static_cast<const exprt &>(
432  template_symbol.value.find(ID_template_methods));
433 
434  for(auto &tm : template_methods.operands())
435  {
436  saved_scope.restore();
437 
438  cpp_declarationt method_decl=
439  static_cast<const cpp_declarationt &>(
440  static_cast<const irept &>(tm));
441 
442  // copy the type of the template method
443  template_typet method_type=
444  method_decl.template_type();
445 
446  // do template parameters
447  // this also sets up the template scope of the method
448  cpp_scopet &method_scope=
449  typecheck_template_parameters(method_type);
450 
451  cpp_scopes.go_to(method_scope);
452 
453  // mapping from template arguments to values/types
454  template_map.build(method_type, specialization_template_args);
455 #ifdef DEBUG
456  std::cout << "METHOD MAP:\n";
457  template_map.print(std::cout);
458 #endif
459 
460  method_decl.remove(ID_template_type);
461  method_decl.remove(ID_is_template);
462 
463  convert(method_decl);
464  }
465 
466  const irep_idt& new_symb_id = new_decl.type().get(ID_identifier);
467  symbolt &new_symb = symbol_table.get_writeable_ref(new_symb_id);
468 
469  // add template arguments to type in order to retrieve template map when
470  // typechecking function body
471  new_symb.type.set(ID_C_template, template_type);
472  new_symb.type.set(ID_C_template_arguments, specialization_template_args);
473 
474 #ifdef DEBUG
475  std::cout << "instance symbol: " << new_symb.name << "\n\n";
476  std::cout << "template type: " << template_type.pretty() << "\n\n";
477 #endif
478 
479  return new_symb;
480  }
481 
482  if(is_template_method)
483  {
484  symbolt &symb = symbol_table.get_writeable_ref(class_name);
485 
486  assert(new_decl.declarators().size() == 1);
487 
488  if(new_decl.member_spec().is_virtual())
489  {
491  error() << "invalid use of `virtual' in template declaration"
492  << eom;
493  throw 0;
494  }
495 
496  if(new_decl.is_typedef())
497  {
499  error() << "template declaration for typedef" << eom;
500  throw 0;
501  }
502 
503  if(new_decl.storage_spec().is_extern() ||
504  new_decl.storage_spec().is_auto() ||
505  new_decl.storage_spec().is_register() ||
506  new_decl.storage_spec().is_mutable())
507  {
509  error() << "invalid storage class specified for template field"
510  << eom;
511  throw 0;
512  }
513 
514  bool is_static=new_decl.storage_spec().is_static();
515  irep_idt access = new_decl.get(ID_C_access);
516 
517  assert(!access.empty());
518  assert(symb.type.id()==ID_struct);
519 
521  symb,
522  new_decl,
523  new_decl.declarators()[0],
525  access,
526  is_static,
527  false,
528  false);
529 
530  return lookup(to_struct_type(symb.type).components().back().get_name());
531  }
532 
533  // not a class template, not a class template method,
534  // it must be a function template!
535 
536  assert(new_decl.declarators().size()==1);
537 
539 
540  const symbolt &symb=
541  lookup(new_decl.declarators()[0].get(ID_identifier));
542 
543  return symb;
544 }
cpp_typecheckt::convert
void convert(cpp_linkage_spect &)
Definition: cpp_typecheck_linkage_spec.cpp:14
cpp_scopet::new_scope
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:192
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_typecheckt::convert_non_template_declaration
void convert_non_template_declaration(cpp_declarationt &declaration)
Definition: cpp_typecheck_declaration.cpp:95
cpp_declarationt::storage_spec
const cpp_storage_spect & storage_spec() const
Definition: cpp_declaration.h:74
cpp_scopet::get_parent
cpp_scopet & get_parent() const
Definition: cpp_scope.h:88
cpp_typecheckt::sub_scope_for_instantiation
cpp_scopet & sub_scope_for_instantiation(cpp_scopet &template_scope, const std::string &suffix)
Set up a scope as subscope of the template scope.
Definition: cpp_instantiate_template.cpp:116
cpp_idt::is_class
bool is_class() const
Definition: cpp_id.h:53
cpp_declarationt::is_typedef
bool is_typedef() const
Definition: cpp_declaration.h:135
cpp_scopet
Definition: cpp_scope.h:21
cpp_typecheckt::elaborate_class_template
void elaborate_class_template(const typet &type)
elaborate class template instances
Definition: cpp_instantiate_template.cpp:224
arith_tools.h
cpp_idt::id_classt::CLASS
@ CLASS
cpp_scopet::id_sett
std::set< cpp_idt * > id_sett
Definition: cpp_scope.h:28
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
cpp_save_scopet
Definition: cpp_scopes.h:129
cpp_scopest::id_map
id_mapt id_map
Definition: cpp_scopes.h:69
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
cpp_typecheckt::template_suffix
std::string template_suffix(const cpp_template_args_tct &template_args)
Definition: cpp_instantiate_template.cpp:26
cpp_scopet::lookup
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
cpp_scopet::add_using_scope
void add_using_scope(cpp_scopet &other)
Definition: cpp_scope.h:109
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
cpp_typecheckt::show_instantiation_stack
void show_instantiation_stack(std::ostream &)
Definition: cpp_instantiate_template.cpp:93
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:148
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_typecheckt::typecheck_template_parameters
cpp_scopet & typecheck_template_parameters(template_typet &type)
Definition: cpp_typecheck_template.cpp:708
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
cpp_idt::identifier
irep_idt identifier
Definition: cpp_id.h:78
cpp_type2name.h
C++ Language Module.
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
exprt
Base class for all expressions.
Definition: expr.h:53
cpp_storage_spect::is_extern
bool is_extern() const
Definition: cpp_storage_spec.h:38
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_typecheckt::class_template_symbol
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
Definition: cpp_instantiate_template.cpp:149
nullptr_exceptiont
Definition: base_exceptions.h:30
cpp_typecheckt::instantiation_stack
instantiation_stackt instantiation_stack
Definition: cpp_typecheck.h:182
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
cpp_scopet::SCOPE_ONLY
@ SCOPE_ONLY
Definition: cpp_scope.h:30
struct_union_typet::make_incomplete
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:186
messaget::eom
static eomt eom
Definition: message.h:297
cpp_typecheckt::instantiation_levelt
Definition: cpp_typecheck.h:187
cpp_idt::suffix
std::string suffix
Definition: cpp_id.h:85
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
cpp_template_args_tct
Definition: cpp_template_args.h:65
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
cpp_storage_spect::is_static
bool is_static() const
Definition: cpp_storage_spec.h:37
cpp_idt
Definition: cpp_id.h:29
template_mapt::apply
void apply(exprt &dest) const
Definition: template_map.cpp:70
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
cpp_declarationt::member_spec
const cpp_member_spect & member_spec() const
Definition: cpp_declaration.h:86
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3552
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
base_exceptions.h
Generic exception types primarily designed for use with invariants.
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
cpp_member_spect::is_virtual
bool is_virtual() const
Definition: cpp_member_spec.h:23
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_idt::id_classt::SYMBOL
@ SYMBOL
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
cpp_typecheckt::typecheck_compound_declarator
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
Definition: cpp_typecheck_compound_type.cpp:287
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
cpp_template_args_baset::arguments
argumentst & arguments()
Definition: cpp_template_args.h:31
cpp_saved_template_mapt
Definition: template_map.h:69
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
template_mapt::print
void print(std::ostream &out) const
Definition: template_map.cpp:133
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
cpp_storage_spect::is_mutable
bool is_mutable() const
Definition: cpp_storage_spec.h:41
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
irept::swap
void swap(irept &irep)
Definition: irep.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
cpp_declarationt
Definition: cpp_declaration.h:24
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
cpp_storage_spect::is_auto
bool is_auto() const
Definition: cpp_storage_spec.h:39
dstringt::empty
bool empty() const
Definition: dstring.h:88
cpp_idt::id_classt::TEMPLATE_SCOPE
@ TEMPLATE_SCOPE
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
cpp_typecheck.h
C++ Language Type Checking.
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
cpp_storage_spect::is_register
bool is_register() const
Definition: cpp_storage_spec.h:40
source_locationt
Definition: source_location.h:20
simplify_expr.h
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
cpp_typecheckt::instantiate_template
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
Definition: cpp_instantiate_template.cpp:253
cpp_save_scopet::restore
void restore()
Definition: cpp_scopes.h:142
cpp_type2name
std::string cpp_type2name(const typet &type)
Definition: cpp_type2name.cpp:97
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:51
irept::get_sub
subt & get_sub()
Definition: irep.h:477
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:408
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:85
cpp_template_args_tct::has_unassigned
bool has_unassigned() const
Definition: cpp_template_args.h:67
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
template_typet
Definition: cpp_template_type.h:19
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:84
cpp_template_args_baset::argumentst
exprt::operandst argumentst
Definition: cpp_template_args.h:29
exprt::operands
operandst & operands()
Definition: expr.h:95
template_mapt::build
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
Definition: template_map.cpp:142
MAX_DEPTH
#define MAX_DEPTH
Definition: cpp_instantiate_template.cpp:251
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
cpp_typecheckt::template_map
template_mapt template_map
Definition: cpp_typecheck.h:228
cpp_idt::is_template_scope
bool is_template_scope() const
Definition: cpp_id.h:73
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_declarationt::template_type
template_typet & template_type()
Definition: cpp_declaration.h:98
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106