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