cprover
Loading...
Searching...
No Matches
reachability_slicer_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Program Slicing
4
5Author: 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
19
21
23{
24public:
26 goto_functionst &goto_functions,
29 {
30 cfg(goto_functions);
31 for(const auto &gf_entry : goto_functions.function_map)
32 {
34 cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
35 }
36
37 is_threadedt is_threaded(goto_functions);
41 slice(goto_functions);
42 }
43
44protected:
55
56 bool is_same_target(
59
62
63 typedef std::stack<cfgt::entryt> queuet;
64
87
89 const is_threadedt &is_threaded,
91
93 const is_threadedt &is_threaded,
95
96 void slice(goto_functionst &goto_functions);
97
98private:
99 std::vector<cfgt::node_indext>
100 backward_outwards_walk_from(std::vector<cfgt::node_indext>);
101
102 void backward_inwards_walk_from(std::vector<cfgt::node_indext>);
103
104 std::vector<cfgt::node_indext>
105 forward_outwards_walk_from(std::vector<cfgt::node_indext>);
106
107 void forward_inwards_walk_from(std::vector<cfgt::node_indext>);
108
110 const cfgt::nodet &call_node,
111 std::vector<cfgt::node_indext> &callsite_successor_stack,
112 std::vector<cfgt::node_indext> &callee_head_stack);
113
114 std::vector<cfgt::node_indext> get_sources(
115 const is_threadedt &is_threaded,
117};
118
119#endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Control Flow Graph.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
base_grapht::nodet nodet
Definition cfg.h:92
entry_mapt entry_map
Definition cfg.h:152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
A collection of goto functions.
function_mapt function_map
instructionst::const_iterator const_targett
nodet::node_indext node_indext
Definition graph.h:173
cfg_baset< slicer_entryt > cfgt
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability)
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 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.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
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.