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 }
cpp_typecheckt::convert_function
void convert_function(symbolt &symbol)
Definition: cpp_typecheck_function.cpp:82
cpp_typecheckt::typecheck_method_bodies
void typecheck_method_bodies()
Definition: cpp_typecheck_method_bodies.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:55
cpp_typecheckt::instantiation_stack
instantiation_stackt instantiation_stack
Definition: cpp_typecheck.h:177
cpp_typecheckt::method_bodyt::instantiation_stack
instantiation_stackt instantiation_stack
Definition: cpp_typecheck.h:334
cpp_typecheckt::instantiation_stackt
std::list< instantiationt > instantiation_stackt
Definition: cpp_typecheck.h:176
template_mapt::swap
void swap(template_mapt &template_map)
Definition: template_map.h:37
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
cpp_typecheckt::method_bodyt::template_map
template_mapt template_map
Definition: cpp_typecheck.h:333
cpp_typecheckt::add_method_body
void add_method_body(symbolt *_method_symbol)
Definition: cpp_typecheck_method_bodies.cpp:51
cpp_typecheckt::methods_seen
std::set< irep_idt > methods_seen
Definition: cpp_typecheck.h:338
cpp_typecheckt::method_bodyt
Definition: cpp_typecheck.h:319
irept::id
const irep_idt & id() const
Definition: irep.h:396
cpp_typecheck.h
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:65
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt
Symbol table entry.
Definition: symbol.h:27
cpp_typecheckt::method_bodies
method_bodiest method_bodies
Definition: cpp_typecheck.h:339
cpp_typecheckt::method_bodyt::method_symbol
symbolt * method_symbol
Definition: cpp_typecheck.h:332
cpp_typecheckt::template_map
template_mapt template_map
Definition: cpp_typecheck.h:223
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40