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
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
if
(method_symbol.
name
==ID_main)
36
add_argc_argv
(method_symbol);
37
38
exprt
&body=method_symbol.
value
;
39
if
(body.
id
() == 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
54
void
cpp_typecheckt::add_method_body
(
symbolt
*_method_symbol)
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(
70
method_bodyt
(_method_symbol,
template_map
,
instantiation_stack
));
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
}
c_typecheck_baset::add_argc_argv
void add_argc_argv(const symbolt &main_symbol)
Definition:
c_typecheck_argc_argv.cpp:16
cpp_typecheckt::convert_function
void convert_function(symbolt &symbol)
Definition:
cpp_typecheck_function.cpp:84
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:54
cpp_typecheckt::instantiation_stack
instantiation_stackt instantiation_stack
Definition:
cpp_typecheck.h:184
cpp_typecheckt::method_bodyt::instantiation_stack
instantiation_stackt instantiation_stack
Definition:
cpp_typecheck.h:338
cpp_typecheckt::instantiation_stackt
std::list< instantiationt > instantiation_stackt
Definition:
cpp_typecheck.h:183
template_mapt::swap
void swap(template_mapt &template_map)
Definition:
template_map.h:35
irept::is_not_nil
bool is_not_nil() const
Definition:
irep.h:173
cpp_typecheckt::method_bodyt::template_map
template_mapt template_map
Definition:
cpp_typecheck.h:337
cpp_typecheckt::add_method_body
void add_method_body(symbolt *_method_symbol)
Definition:
cpp_typecheck_method_bodies.cpp:54
cpp_typecheckt::methods_seen
std::set< irep_idt > methods_seen
Definition:
cpp_typecheck.h:342
cpp_typecheckt::method_bodyt
Definition:
cpp_typecheck.h:323
irept::id
const irep_idt & id() const
Definition:
irep.h:259
cpp_typecheck.h
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition:
expr.cpp:130
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:343
cpp_typecheckt::method_bodyt::method_symbol
symbolt * method_symbol
Definition:
cpp_typecheck.h:336
cpp_typecheckt::template_map
template_mapt template_map
Definition:
cpp_typecheck.h:230
symbolt::name
irep_idt name
The unique identifier.
Definition:
symbol.h:40
cpp
cpp_typecheck_method_bodies.cpp
Generated by
1.8.16