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,...
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,...
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,...
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,...
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,...
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,...
void backward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program,...
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability)