CBMC
Loading...
Searching...
No Matches
remove_unreachable.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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
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 {
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
57 goto_program.update();
58}
59
64{
65 for(auto &gf_entry : goto_functions.function_map)
66 remove_unreachable(gf_entry.second.body);
67}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
instructionst::iterator targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Goto Programs with Functions.
#define Forall_goto_program_instructions(it, program)
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Program Transformation.