CBMC
compute_called_functions.h
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 #ifndef CPROVER_GOTO_PROGRAMS_COMPUTE_CALLED_FUNCTIONS_H
13 #define CPROVER_GOTO_PROGRAMS_COMPUTE_CALLED_FUNCTIONS_H
14 
15 #include <unordered_set>
16 
17 #include <util/irep.h>
18 
19 class exprt;
20 class goto_functionst;
21 class goto_programt;
22 class goto_modelt;
23 
24 // compute the set of functions whose address is taken
25 
26 void compute_address_taken_functions(
27  const exprt &,
28  std::unordered_set<irep_idt> &);
29 
30 void compute_address_taken_functions(
31  const goto_programt &,
32  std::unordered_set<irep_idt> &);
33 
34 void compute_address_taken_functions(
35  const goto_functionst &,
36  std::unordered_set<irep_idt> &);
37 
38 // computes the functions that are (potentially) called
39 std::unordered_set<irep_idt> compute_called_functions(const goto_functionst &);
40 std::unordered_set<irep_idt> compute_called_functions(const goto_modelt &);
41 
42 #endif // CPROVER_GOTO_PROGRAMS_COMPUTE_CALLED_FUNCTIONS_H
exprt
Base class for all expressions.
Definition: expr.h:56
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
compute_called_functions
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &)
computes the functions that are (potentially) called
Definition: compute_called_functions.cpp:88
compute_address_taken_functions
void compute_address_taken_functions(const exprt &, std::unordered_set< irep_idt > &)
get all functions whose address is taken
Definition: compute_called_functions.cpp:20