CBMC
replace_calls.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace calls
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H
14 #define CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H
15 
16 #include <util/irep.h>
17 
18 #include <list>
19 #include <map>
20 
21 class goto_functionst;
22 class goto_modelt;
23 class goto_programt;
24 class namespacet;
25 
27 {
28 public:
29  typedef std::list<std::string> replacement_listt;
30  typedef std::map<irep_idt, irep_idt> replacement_mapt;
31 
32  void operator()(
33  goto_modelt &goto_model,
34  const replacement_listt &replacement_list) const;
35 
36  void operator()(
37  goto_modelt &goto_model,
38  const replacement_mapt &replacement_map) const;
39 
40 protected:
41  void operator()(
42  goto_programt &goto_program,
43  const goto_functionst &goto_functions,
44  const namespacet &ns,
45  const replacement_mapt &replacement_map) const;
46 
48  parse_replacement_list(const replacement_listt &replacement_list) const;
49 
51  const replacement_mapt &replacement_map,
52  const goto_functionst &goto_functions,
53  const namespacet &ns) const;
54 };
55 
56 #define OPT_REPLACE_CALLS "(replace-calls):"
57 
58 #define HELP_REPLACE_CALLS \
59  " --replace-calls f:g replace calls to f with calls to g\n"
60 
61 #endif // CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H
replace_callst::replacement_listt
std::list< std::string > replacement_listt
Definition: replace_calls.h:29
goto_modelt
Definition: goto_model.h:25
replace_callst::check_replacement_map
void check_replacement_map(const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const
Definition: replace_calls.cpp:140
replace_callst::parse_replacement_list
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
Definition: replace_calls.cpp:115
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
replace_callst::replacement_mapt
std::map< irep_idt, irep_idt > replacement_mapt
Definition: replace_calls.h:30
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
replace_callst::operator()
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
Definition: replace_calls.cpp:29
replace_callst
Definition: replace_calls.h:26
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
irep.h