cprover
reachability_slicer_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Program Slicing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
14 
16 #include <goto-programs/cfg.h>
17 
18 #include <analyses/is_threaded.h>
19 
20 class slicing_criteriont;
21 
23 {
24 public:
25  void operator()(
26  goto_functionst &goto_functions,
27  slicing_criteriont &criterion)
28  {
29  cfg(goto_functions);
30  is_threadedt is_threaded(goto_functions);
31  fixedpoint_assertions(is_threaded, criterion);
32  slice(goto_functions);
33  }
34 
35 protected:
37  {
39  {
40  }
41 
43  };
44 
46  cfgt cfg;
47 
48  typedef std::stack<cfgt::entryt> queuet;
49 
51  const is_threadedt &is_threaded,
52  slicing_criteriont &criterion);
53 
54  void slice(goto_functionst &goto_functions);
55 };
56 
57 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Over-approximate Concurrency for Threaded Goto Programs.
Control Flow Graph.
Goto Programs with Functions.
void operator()(goto_functionst &goto_functions, slicing_criteriont &criterion)
void fixedpoint_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
void slice(goto_functionst &goto_functions)
cfg_baset< slicer_entryt > cfgt