35 std::vector<reachability_slicert::cfgt::node_indext>
40 std::vector<cfgt::node_indext> sources;
43 if(criterion(e_it.first) || is_threaded(e_it.first))
44 sources.push_back(e_it.second);
56 return it1->function == it2->function && it1 == it2;
65 std::vector<reachability_slicert::cfgt::node_indext>
67 std::vector<cfgt::node_indext>
stack)
69 std::vector<cfgt::node_indext> return_sites;
76 if(node.reaches_assertion)
78 node.reaches_assertion =
true;
80 for(
const auto &edge : node.in)
82 const auto &pred_node =
cfg[edge.first];
84 if(pred_node.PC->is_end_function())
88 return_sites.push_back(edge.first);
91 std::prev(node.PC)->is_function_call(),
92 "all function return edges should point to the successor of a "
93 "FUNCTION_CALL instruction");
99 stack.push_back(edge.first);
117 std::vector<cfgt::node_indext>
stack)
119 while(!
stack.empty())
124 if(node.reaches_assertion)
126 node.reaches_assertion =
true;
128 for(
const auto &edge : node.in)
130 const auto &pred_node =
cfg[edge.first];
132 if(pred_node.PC->is_end_function())
137 stack.push_back(edge.first);
140 std::prev(node.PC)->is_function_call(),
141 "all function return edges should point to the successor of a "
142 "FUNCTION_CALL instruction");
146 else if(pred_node.PC->is_function_call())
153 stack.push_back(edge.first);
169 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
173 std::vector<cfgt::node_indext> return_sites =
189 const cfgt::nodet &call_node,
190 std::vector<cfgt::node_indext> &callsite_successor_stack,
191 std::vector<cfgt::node_indext> &callee_head_stack)
195 INVARIANT(call_node.out.size() == 1,
"Call sites should have one successor");
196 const auto successor_index = call_node.out.begin()->first;
198 auto callsite_successor_pc = std::next(call_node.PC);
200 auto successor_pc =
cfg[successor_index].PC;
204 callee_head_stack.push_back(successor_index);
207 while(!successor_pc->is_end_function())
211 callsite_successor_stack.push_back(
cfg.
entry_map[callsite_successor_pc]);
216 callsite_successor_stack.push_back(successor_index);
226 std::vector<reachability_slicert::cfgt::node_indext>
228 std::vector<cfgt::node_indext>
stack)
230 std::vector<cfgt::node_indext> called_function_heads;
232 while(!
stack.empty())
237 if(node.reachable_from_assertion)
239 node.reachable_from_assertion =
true;
241 if(node.PC->is_function_call())
250 for(
const auto &edge : node.out)
251 stack.push_back(edge.first);
255 return called_function_heads;
266 std::vector<cfgt::node_indext>
stack)
268 while(!
stack.empty())
273 if(node.reachable_from_assertion)
275 node.reachable_from_assertion =
true;
277 if(node.PC->is_function_call())
282 else if(node.PC->is_end_function())
291 for(
const auto &edge : node.out)
292 stack.push_back(edge.first);
307 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
311 std::vector<cfgt::node_indext> return_sites =
326 if(f_it->second.body_available())
332 !e.reaches_assertion && !e.reachable_from_assertion &&
333 !i_it->is_end_function())
353 const bool include_forward_reachability)
369 const std::list<std::string> &properties,
370 const bool include_forward_reachability)
384 const std::list<std::string> &functions_list)
386 for(
const auto &
function : functions_list)
416 const std::list<std::string> &properties)