CBMC
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 class message_handlert;
19 
21 {
22 protected:
24  const goto_programt::const_targett target,
25  const goto_functionst &goto_functions);
26 
28  goto_programt &dest,
30  const exprt &lhs,
31  const exprt::operandst &arguments);
32 
33 public:
34  void operator()(
35  goto_programt &goto_program,
36  const goto_functionst &goto_functions,
38 
39  void operator()(goto_functionst &goto_functions, message_handlert &);
40 };
41 
42 #define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)"
43 
44 #define HELP_REMOVE_CALLS_NO_BODY \
45  " {y--remove-calls-no-body} \t remove calls to functions without a body\n"
46 
47 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single 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.
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions, message_handlert &)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
Concrete Goto Program.