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
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
exprt
Base class for all expressions.
Definition:
expr.h:55
goto_modelt
Definition:
goto_model.h:25
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
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:24
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:72
irep.h
src
goto-programs
compute_called_functions.h
Generated by
1.8.17