cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
compute_called_functions.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Query Called Functions
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
compute_called_functions.h
"
13
14
#include <
util/pointer_expr.h
>
15
#include <
util/std_expr.h
>
16
17
#include "
goto_model.h
"
18
20
void
compute_address_taken_functions
(
21
const
exprt
&src,
22
std::unordered_set<irep_idt> &
address_taken
)
23
{
24
for
(
const
auto
&op : src.
operands
())
25
compute_address_taken_functions
(op,
address_taken
);
26
27
if
(src.
id
() == ID_address_of)
28
{
29
const
address_of_exprt
&address =
to_address_of_expr
(src);
30
31
if
(
32
address.
type
().
id
() == ID_pointer &&
33
to_pointer_type
(address.
type
()).base_type().id() == ID_code)
34
{
35
const
exprt
&target = address.
object
();
36
if
(target.
id
() == ID_symbol)
37
address_taken
.insert(
to_symbol_expr
(target).get_identifier());
38
}
39
}
40
}
41
43
void
compute_functions
(
44
const
exprt
&src,
45
std::unordered_set<irep_idt> &
address_taken
)
46
{
47
for
(
const
auto
&op : src.
operands
())
48
compute_functions
(op,
address_taken
);
49
50
if
(src.
type
().
id
()==ID_code &&
51
src.
id
()==ID_symbol)
52
address_taken
.insert(
to_symbol_expr
(src).get_identifier());
53
}
54
56
void
compute_address_taken_functions
(
57
const
goto_programt
&goto_program,
58
std::unordered_set<irep_idt> &
address_taken
)
59
{
60
for
(
const
auto
&i : goto_program.
instructions
)
61
{
62
i.apply([&
address_taken
](
const
exprt
&expr) {
63
compute_address_taken_functions
(expr,
address_taken
);
64
});
65
}
66
}
67
69
void
compute_address_taken_functions
(
70
const
goto_functionst
&goto_functions,
71
std::unordered_set<irep_idt> &
address_taken
)
72
{
73
for
(
const
auto
&gf_entry : goto_functions.
function_map
)
74
compute_address_taken_functions
(gf_entry.second.body,
address_taken
);
75
}
76
78
std::unordered_set<irep_idt>
79
compute_address_taken_functions
(
const
goto_functionst
&goto_functions)
80
{
81
std::unordered_set<irep_idt>
address_taken
;
82
compute_address_taken_functions
(goto_functions,
address_taken
);
83
return
address_taken
;
84
}
85
87
std::unordered_set<irep_idt>
88
compute_called_functions
(
const
goto_functionst
&goto_functions)
89
{
90
std::unordered_set<irep_idt> working_queue;
91
std::unordered_set<irep_idt> functions;
92
93
// start from entry point
94
working_queue.insert(goto_functions.
entry_point
());
95
96
while
(!working_queue.empty())
97
{
98
irep_idt
id
=*working_queue.begin();
99
working_queue.erase(working_queue.begin());
100
101
if
(!functions.insert(
id
).second)
102
continue
;
103
104
const
goto_functionst::function_mapt::const_iterator f_it=
105
goto_functions.
function_map
.find(
id
);
106
107
if
(f_it==goto_functions.
function_map
.end())
108
continue
;
109
110
const
goto_programt
&program=
111
f_it->second.body;
112
113
compute_address_taken_functions
(program, working_queue);
114
115
for
(
const
auto
&instruction : program.
instructions
)
116
{
117
if
(instruction.is_function_call())
118
{
119
compute_functions
(instruction.call_function(), working_queue);
120
}
121
}
122
}
123
124
return
functions;
125
}
126
128
std::unordered_set<irep_idt>
129
compute_called_functions
(
const
goto_modelt
&goto_model)
130
{
131
return
compute_called_functions
(goto_model.
goto_functions
);
132
}
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition
address_taken.cpp:51
address_of_exprt
Operator to return the address of an object.
Definition
pointer_expr.h:540
address_of_exprt::object
exprt & object()
Definition
pointer_expr.h:549
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
exprt::operands
operandst & operands()
Definition
expr.h:95
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_functionst::function_map
function_mapt function_map
Definition
goto_functions.h:29
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition
goto_functions.h:97
goto_modelt
Definition
goto_model.h:27
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition
goto_model.h:34
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition
goto_program.h:621
irept::id
const irep_idt & id() const
Definition
irep.h:388
compute_functions
void compute_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions in the expression
Definition
compute_called_functions.cpp:43
compute_address_taken_functions
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
Definition
compute_called_functions.cpp:20
compute_called_functions
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Definition
compute_called_functions.cpp:88
compute_called_functions.h
Query Called Functions.
goto_model.h
Symbol Table + CFG.
pointer_expr.h
API to expression classes for Pointers.
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition
pointer_expr.h:577
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition
pointer_expr.h:93
std_expr.h
API to expression classes.
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition
std_expr.h:211
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-programs
compute_called_functions.cpp
Generated by
1.17.0