CBMC
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 }
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:614
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.