cprover
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  if(method_symbol.name==ID_main)
36  add_argc_argv(method_symbol);
37 
38  exprt &body=method_symbol.value;
39  if(body.id()=="cpp_not_typechecked")
40  continue;
41 
42 #ifdef DEBUG
43  std::cout << "convert_method_body: " << method_symbol.name << std::endl;
44  std::cout << " is_not_nil: " << body.is_not_nil() << std::endl;
45  std::cout << " !is_zero: " << (!body.is_zero()) << std::endl;
46 #endif
47  if(body.is_not_nil() && !body.is_zero())
48  convert_function(method_symbol);
49  }
50 
51  old_instantiation_stack.swap(instantiation_stack);
52 }
53 
55 {
56 #ifdef DEBUG
57  std::cout << "add_method_body: " << _method_symbol->name << std::endl;
58 #endif
59 
60  // We have to prevent the same method to be added multiple times
61  // otherwise we get duplicated symbol prefixes
62  if(methods_seen.find(_method_symbol->name) != methods_seen.end())
63  {
64 #ifdef DEBUG
65  std::cout << " already exists" << std::endl;
66 #endif
67  return;
68  }
69  method_bodies.push_back(
71 
72  // Converting a method body might add method bodies for methods
73  // that we have already analyzed. Hence, we have to keep track.
74  methods_seen.insert(_method_symbol->name);
75 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
void convert_function(symbolt &symbol)
bool is_not_nil() const
Definition: irep.h:173
instantiation_stackt instantiation_stack
exprt value
Initial value of symbol.
Definition: symbol.h:37
template_mapt template_map
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::set< irep_idt > methods_seen
void swap(template_mapt &template_map)
Definition: template_map.h:35
instantiation_stackt instantiation_stack
void add_method_body(symbolt *_method_symbol)
const irep_idt & id() const
Definition: irep.h:259
std::list< instantiationt > instantiation_stackt
C++ Language Type Checking.
method_bodiest method_bodies
Base class for all expressions.
Definition: expr.h:42
void add_argc_argv(const symbolt &main_symbol)
bool is_zero() const
Definition: expr.cpp:161