cprover
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 
13 
14 #include <util/std_expr.h>
15 
18  const exprt &src,
19  std::unordered_set<irep_idt> &address_taken)
20 {
21  forall_operands(it, src)
22  compute_address_taken_functions(*it, address_taken);
23 
24  if(src.id()==ID_address_of &&
25  src.type().id()==ID_pointer &&
26  src.type().subtype().id()==ID_code)
27  {
28  assert(src.operands().size()==1);
29  const exprt &op=src.op0();
30  if(op.id()==ID_symbol)
31  address_taken.insert(to_symbol_expr(op).get_identifier());
32  }
33 }
34 
37  const exprt &src,
38  std::unordered_set<irep_idt> &address_taken)
39 {
40  forall_operands(it, src)
41  compute_functions(*it, address_taken);
42 
43  if(src.type().id()==ID_code &&
44  src.id()==ID_symbol)
45  address_taken.insert(to_symbol_expr(src).get_identifier());
46 }
47 
51  std::unordered_set<irep_idt> &address_taken)
52 {
54  {
55  compute_address_taken_functions(it->guard, address_taken);
56  compute_address_taken_functions(it->code, address_taken);
57  }
58 }
59 
62  const goto_functionst &goto_functions,
63  std::unordered_set<irep_idt> &address_taken)
64 {
65  forall_goto_functions(it, goto_functions)
66  compute_address_taken_functions(it->second.body, address_taken);
67 }
68 
70 std::unordered_set<irep_idt>
72 {
73  std::unordered_set<irep_idt> address_taken;
74  compute_address_taken_functions(goto_functions, address_taken);
75  return address_taken;
76 }
77 
79 std::unordered_set<irep_idt>
81 {
82  std::unordered_set<irep_idt> working_queue;
83  std::unordered_set<irep_idt> functions;
84 
85  // start from entry point
86  working_queue.insert(goto_functions.entry_point());
87 
88  while(!working_queue.empty())
89  {
90  irep_idt id=*working_queue.begin();
91  working_queue.erase(working_queue.begin());
92 
93  if(!functions.insert(id).second)
94  continue;
95 
96  const goto_functionst::function_mapt::const_iterator f_it=
97  goto_functions.function_map.find(id);
98 
99  if(f_it==goto_functions.function_map.end())
100  continue;
101 
102  const goto_programt &program=
103  f_it->second.body;
104 
105  compute_address_taken_functions(program, working_queue);
106 
107  forall_goto_program_instructions(i_it, program)
108  {
109  if(i_it->is_function_call())
110  {
112  to_code_function_call(i_it->code).function(),
113  working_queue);
114  }
115  }
116  }
117 
118  return functions;
119 }
120 
122 std::unordered_set<irep_idt>
124 {
125  return compute_called_functions(goto_model.goto_functions);
126 }
exprt & op0()
Definition: expr.h:72
void compute_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions in the expression
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
function_mapt function_map
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Query Called Functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
static irep_idt entry_point()
exprt & function()
Definition: std_code.h:878
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
const typet & subtype() const
Definition: type.h:33
#define forall_goto_functions(it, functions)
operandst & operands()
Definition: expr.h:66
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909