search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known)
cfgt::node_indext node_index
CFG node to mark reachable.
bool reachable_from_assertion
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).
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.
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.
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...