cprover
Loading...
Searching...
No Matches
remove_calls_no_body.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove calls to functions without a body
4
5Author: 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
17class goto_functionst;
18
20{
21protected:
24 const goto_functionst &goto_functions);
25
27 goto_programt &dest,
29 const exprt &lhs,
30 const exprt::operandst &arguments);
31
32public:
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
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
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)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
Concrete Goto Program.