cprover
reachability_slicer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "reachability_slicer.h"
13 
14 #include <stack>
15 
18 #include <goto-programs/cfg.h>
19 
20 #include "full_slicer_class.h"
22 
24  const is_threadedt &is_threaded,
25  slicing_criteriont &criterion)
26 {
27  queuet queue;
28 
29  for(cfgt::entry_mapt::iterator
30  e_it=cfg.entry_map.begin();
31  e_it!=cfg.entry_map.end();
32  e_it++)
33  if(criterion(e_it->first) ||
34  is_threaded(e_it->first))
35  queue.push(e_it->second);
36 
37  while(!queue.empty())
38  {
39  cfgt::entryt e=queue.top();
40  cfgt::nodet &node=cfg[e];
41  queue.pop();
42 
43  if(node.reaches_assertion)
44  continue;
45 
46  node.reaches_assertion=true;
47 
48  for(cfgt::edgest::const_iterator
49  p_it=node.in.begin();
50  p_it!=node.in.end();
51  p_it++)
52  {
53  queue.push(p_it->first);
54  }
55  }
56 }
57 
59 {
60  // now replace those instructions that do not reach any assertions
61  // by assume(false)
62 
63  Forall_goto_functions(f_it, goto_functions)
64  if(f_it->second.body_available())
65  {
66  Forall_goto_program_instructions(i_it, f_it->second.body)
67  {
68  const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
69  if(!e.reaches_assertion &&
70  !i_it->is_end_function())
71  i_it->make_assumption(false_exprt());
72  }
73 
74  // replace unreachable code by skip
75  remove_unreachable(f_it->second.body);
76  }
77 
78  // remove the skips
79  remove_skip(goto_functions);
80  goto_functions.update();
81 }
82 
83 void reachability_slicer(goto_functionst &goto_functions)
84 {
87  s(goto_functions, a);
88 }
89 
91  goto_functionst &goto_functions,
92  const std::list<std::string> &properties)
93 {
95  properties_criteriont p(properties);
96  s(goto_functions, p);
97 }
Goto Program Slicing.
Control Flow Graph.
entry_mapt entry_map
Definition: cfg.h:87
void fixedpoint_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
std::size_t entryt
Definition: cfg.h:65
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
edgest in
Definition: graph.h:41
std::stack< cfgt::entryt > queuet
void slice(goto_functionst &goto_functions)
The boolean constant false.
Definition: std_expr.h:3753
void reachability_slicer(goto_functionst &goto_functions)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
#define Forall_goto_functions(it, functions)
Program Transformation.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Goto Program Slicing.
Program Transformation.