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
18
void
cpp_typecheckt::typecheck_method_bodies
()
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
51
void
cpp_typecheckt::add_method_body
(
symbolt
*_method_symbol)
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(
62
method_bodyt
(_method_symbol,
template_map
,
instantiation_stack
));
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
src
cpp
cpp_typecheck_method_bodies.cpp
Generated by
1.8.17