cprover
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 
18 void remove_unreachable(goto_programt &goto_program)
19 {
20  std::set<goto_programt::targett> reachable;
21  std::stack<goto_programt::targett> working;
22 
23  working.push(goto_program.instructions.begin());
24 
25  while(!working.empty())
26  {
27  goto_programt::targett t=working.top();
28  working.pop();
29 
30  if(reachable.find(t)==reachable.end() &&
31  t!=goto_program.instructions.end())
32  {
33  reachable.insert(t);
34 
35  for(const auto &succ : goto_program.get_successors(t))
36  working.push(succ);
37  }
38  }
39 
40  // make all unreachable code a skip
41  // unless it's an 'end_function'
42 
43  Forall_goto_program_instructions(it, goto_program)
44  {
45  if(reachable.find(it)==reachable.end() &&
46  !it->is_end_function())
47  it->make_skip();
48  }
49 }
50 
55 void remove_unreachable(goto_functionst &goto_functions)
56 {
57  Forall_goto_functions(f_it, goto_functions)
58  remove_unreachable(f_it->second.body);
59 }
instructionst instructions
The list of instructions in the goto program.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
std::list< Target > get_successors(Target target) const
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
#define Forall_goto_functions(it, functions)
Program Transformation.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73