CBMC
cpp_typecheck_method_bodies.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 #ifdef DEBUG
13 #include <iostream>
14 #endif
15 
16 #include "cpp_typecheck.h"
17 
19 {
20  instantiation_stackt old_instantiation_stack;
21  old_instantiation_stack.swap(instantiation_stack);
22 
23  while(!method_bodies.empty())
24  {
25  // Dangerous not to take a copy here. We'll have to make sure that
26  // convert is never called with the same symbol twice.
27  method_bodyt &method_body = *method_bodies.begin();
28  symbolt &method_symbol = *method_body.method_symbol;
29 
30  template_map.swap(method_body.template_map);
31  instantiation_stack.swap(method_body.instantiation_stack);
32 
33  method_bodies.erase(method_bodies.begin());
34 
35  exprt &body=method_symbol.value;
36  if(body.id() == ID_cpp_not_typechecked)
37  continue;
38 
39 #ifdef DEBUG
40  std::cout << "convert_method_body: " << method_symbol.name << '\n';
41  std::cout << " is_not_nil: " << body.is_not_nil() << '\n';
42  std::cout << " !is_zero: " << (!body.is_zero()) << '\n';
43 #endif
44  if(body.is_not_nil() && !body.is_zero())
45  convert_function(method_symbol);
46  }
47 
48  old_instantiation_stack.swap(instantiation_stack);
49 }
50 
52 {
53 #ifdef DEBUG
54  std::cout << "add_method_body: " << _method_symbol->name << '\n';
55 #endif
56  // Converting a method body might add method bodies for methods that we have
57  // already analyzed. Adding the same method more than once causes duplicated
58  // symbol prefixes, therefore we have to keep track.
59  if(methods_seen.insert(_method_symbol->name).second)
60  {
61  method_bodies.push_back(
63  }
64 #ifdef DEBUG
65  else
66  std::cout << " already exists\n";
67 #endif
68 }
std::set< irep_idt > methods_seen
instantiation_stackt instantiation_stack
template_mapt template_map
void convert_function(symbolt &symbol)
std::list< instantiationt > instantiation_stackt
void add_method_body(symbolt *_method_symbol)
method_bodiest method_bodies
Base class for all expressions.
Definition: expr.h:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
void swap(template_mapt &template_map)
Definition: template_map.h:37
C++ Language Type Checking.
instantiation_stackt instantiation_stack