cprover
remove_calls_no_body.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove calls to functions without a body
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
13 #define CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
14 
15 #include "goto_program.h"
16 
17 class goto_functionst;
18 
20 {
21 protected:
23  const goto_programt::const_targett target,
24  const goto_functionst &goto_functions);
25 
27  goto_programt &dest,
29  const exprt &lhs,
30  const exprt::operandst &arguments);
31 
32 public:
33  void operator()(
34  goto_programt &goto_program,
35  const goto_functionst &goto_functions);
36 
37  void operator()(goto_functionst &goto_functions);
38 };
39 
40 #define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)"
41 
42 #define HELP_REMOVE_CALLS_NO_BODY \
43  " --remove-calls-no-body remove calls to functions without a body\n"
44 
45 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
exprt
Base class for all expressions.
Definition: expr.h:53
remove_calls_no_bodyt::remove_call_no_body
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
Definition: remove_calls_no_body.cpp:23
remove_calls_no_bodyt::operator()
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
Definition: remove_calls_no_body.cpp:99
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
goto_program.h
Concrete Goto Program.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
remove_calls_no_bodyt
Definition: remove_calls_no_body.h:20
remove_calls_no_bodyt::is_opaque_function_call
bool is_opaque_function_call(const goto_programt::const_targett target, const goto_functionst &goto_functions)
Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call.
Definition: remove_calls_no_body.cpp:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579