cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
20
class
remove_calls_no_bodyt
21
{
22
protected
:
23
bool
is_opaque_function_call
(
24
const
goto_programt::const_targett
target,
25
const
goto_functionst
&goto_functions);
26
27
void
remove_call_no_body
(
28
goto_programt
&dest,
29
goto_programt::targett
target,
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,
37
message_handlert
&);
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
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::operandst
std::vector< exprt > operandst
Definition
expr.h:59
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
goto_programt::targett
instructionst::iterator targett
Definition
goto_program.h:613
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition
goto_program.h:614
message_handlert
Definition
message.h:27
remove_calls_no_bodyt
Definition
remove_calls_no_body.h:21
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:25
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:66
remove_calls_no_bodyt::operator()
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...
Definition
remove_calls_no_body.cpp:99
goto_program.h
Concrete Goto Program.
goto-programs
remove_calls_no_body.h
Generated by
1.17.0