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,
28  bool include_forward_reachability)
29  {
30  cfg(goto_functions);
31  is_threadedt is_threaded(goto_functions);
32  fixedpoint_to_assertions(is_threaded, criterion);
33  if(include_forward_reachability)
35  slice(goto_functions);
36  }
37 
38 protected:
40  {
42  {
43  }
44 
47  };
48 
51 
52  typedef std::stack<cfgt::entryt> queuet;
53 
58  {
61 
70 
73  {
74  }
75  };
76 
78  const is_threadedt &is_threaded,
80 
82  const is_threadedt &is_threaded,
84 
85  void slice(goto_functionst &goto_functions);
86 
87 private:
88  std::vector<cfgt::node_indext>
90 };
91 
92 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Over-approximate Concurrency for Threaded Goto Programs.
Control Flow Graph.
search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known)
Goto Programs with Functions.
cfgt::node_indext node_index
CFG node to mark reachable.
std::stack< cfgt::entryt > queuet
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
bool caller_is_known
If true, this function&#39;s caller is known and has already been queued to mark reachable, so there is no need to queue anything when walking out of the function, whether forwards (via END_FUNCTION) or backwards (via a callsite).
std::vector< cfgt::node_indext > get_sources(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent executi...
void fixedpoint_from_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
cfg_baset< slicer_entryt > cfgt
void fixedpoint_to_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform backwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
void operator()(goto_functionst &goto_functions, slicing_criteriont &criterion, bool include_forward_reachability)
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...