12 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H 13 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H 28 bool include_forward_reachability)
33 if(include_forward_reachability)
35 slice(goto_functions);
52 typedef std::stack<cfgt::entryt>
queuet;
88 std::vector<cfgt::node_indext>
93 std::vector<cfgt::node_indext>
100 std::vector<cfgt::node_indext> &callsite_successor_stack,
101 std::vector<cfgt::node_indext> &callee_head_stack);
108 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Over-approximate Concurrency for Threaded Goto Programs.
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, starting from a given set of nodes.
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.
bool reachable_from_assertion
std::stack< cfgt::entryt > queuet
void forward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.
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, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
cfg_base_nodet< slicer_entryt, goto_programt::const_targett > nodet
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
A collection of goto functions.
bool caller_is_known
If true, this function'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).
nodet::node_indext node_indext
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.
cfg_baset< slicer_entryt > cfgt
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, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...
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, starting from a given set of nodes.
void backward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability)