CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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;
19
21{
22protected:
25 const goto_functionst &goto_functions);
26
28 goto_programt &dest,
30 const exprt &lhs,
31 const exprt::operandst &arguments);
32
33public:
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.
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, message_handlert &)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
Concrete Goto Program.