cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
remove_unreachable.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Program Transformation
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
remove_unreachable.h
"
13
14
#include <set>
15
#include <stack>
16
17
#include "
goto_functions.h
"
18
20
void
remove_unreachable
(
goto_programt
&goto_program)
21
{
22
std::set<goto_programt::targett, goto_programt::target_less_than> reachable;
23
std::stack<goto_programt::targett> working;
24
25
working.push(goto_program.
instructions
.begin());
26
27
while
(!working.empty())
28
{
29
goto_programt::targett
t=working.top();
30
working.pop();
31
32
if
(reachable.find(t)==reachable.end() &&
33
t!=goto_program.
instructions
.end())
34
{
35
reachable.insert(t);
36
37
for
(
const
auto
&succ : goto_program.
get_successors
(t))
38
working.push(succ);
39
}
40
}
41
42
// make all unreachable code a skip
43
// unless it's an 'end_function'
44
bool
did_something =
false
;
45
46
Forall_goto_program_instructions
(it, goto_program)
47
{
48
if
(reachable.find(it)==reachable.end() &&
49
!it->is_end_function())
50
{
51
it->turn_into_skip();
52
did_something =
true
;
53
}
54
}
55
56
if
(did_something)
57
goto_program.
update
();
58
}
59
63
void
remove_unreachable
(
goto_functionst
&goto_functions)
64
{
65
for
(
auto
&gf_entry : goto_functions.
function_map
)
66
remove_unreachable
(gf_entry.second.body);
67
}
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_functionst::function_map
function_mapt function_map
Definition
goto_functions.h:29
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition
goto_program.h:621
goto_programt::update
void update()
Update all indices.
Definition
goto_program.cpp:619
goto_programt::targett
instructionst::iterator targett
Definition
goto_program.h:613
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition
goto_program.h:1125
goto_functions.h
Goto Programs with Functions.
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition
goto_program.h:1233
remove_unreachable
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Definition
remove_unreachable.cpp:20
remove_unreachable.h
Program Transformation.
goto-programs
remove_unreachable.cpp
Generated by
1.17.0