CBMC
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 
17 class goto_functionst;
18 class message_handlert;
19 class slicing_criteriont;
20 
22 {
23 public:
24  void operator()(
25  goto_functionst &goto_functions,
26  const slicing_criteriont &criterion,
27  bool include_forward_reachability,
29 
30 protected:
32  {
34  {
35  }
36 
40  };
41 
42  bool is_same_target(
45 
48 
49  typedef std::stack<cfgt::entryt> queuet;
50 
55  {
58 
67 
70  {
71  }
72  };
73 
75  const is_threadedt &is_threaded,
76  const slicing_criteriont &criterion);
77 
79  const is_threadedt &is_threaded,
80  const slicing_criteriont &criterion);
81 
82  void slice(goto_functionst &goto_functions);
83 
84 private:
85  std::vector<cfgt::node_indext>
86  backward_outwards_walk_from(std::vector<cfgt::node_indext>);
87 
88  void backward_inwards_walk_from(std::vector<cfgt::node_indext>);
89 
90  std::vector<cfgt::node_indext>
91  forward_outwards_walk_from(std::vector<cfgt::node_indext>);
92 
93  void forward_inwards_walk_from(std::vector<cfgt::node_indext>);
94 
96  const cfgt::nodet &call_node,
97  std::vector<cfgt::node_indext> &callsite_successor_stack,
98  std::vector<cfgt::node_indext> &callee_head_stack);
99 
100  std::vector<cfgt::node_indext> get_sources(
101  const is_threadedt &is_threaded,
102  const slicing_criteriont &criterion);
103 };
104 
105 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
base_grapht::nodet nodet
Definition: cfg.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:615
cfg_baset< slicer_entryt > cfgt
std::vector< cfgt::node_indext > backward_outwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program,...
bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2) const
std::vector< cfgt::node_indext > forward_outwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
std::stack< cfgt::entryt > queuet
void backward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program,...
std::vector< cfgt::node_indext > get_sources(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent executi...
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability, message_handlert &)
void fixedpoint_to_assertions(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Perform backward depth-first search of the control-flow graph of the goto program,...
void fixedpoint_from_assertions(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Perform forwards depth-first search of the control-flow graph of the goto program,...
void forward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
void forward_walk_call_instruction(const cfgt::nodet &call_node, std::vector< cfgt::node_indext > &callsite_successor_stack, std::vector< cfgt::node_indext > &callee_head_stack)
Process a call instruction during a forwards reachability walk.
Concrete Goto Program.
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...
bool caller_is_known
If true, this function's caller is known and has already been queued to mark reachable,...
search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known)
cfgt::node_indext node_index
CFG node to mark reachable.