CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_method_bodies.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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{
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.
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
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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)
C++ Language Type Checking.