33 std::vector<reachability_slicert::cfgt::node_indext>
38 std::vector<cfgt::node_indext> sources;
42 criterion(
cfg[e_it.second].function_id, e_it.first) ||
43 is_threaded(e_it.first))
44 sources.push_back(e_it.second);
50 "no slicing criterion found",
52 "provide at least one property using --property <property>"};
66 return node1.function_id == node2.function_id && it1 == it2;
75 std::vector<reachability_slicert::cfgt::node_indext>
77 std::vector<cfgt::node_indext> stack)
79 std::vector<cfgt::node_indext> return_sites;
83 auto &node =
cfg[stack.back()];
86 if(node.reaches_assertion)
88 node.reaches_assertion =
true;
90 for(
const auto &edge : node.in)
92 const auto &pred_node =
cfg[edge.first];
94 if(pred_node.PC->is_end_function())
98 return_sites.push_back(edge.first);
101 std::prev(node.PC)->is_function_call(),
102 "all function return edges should point to the successor of a "
103 "FUNCTION_CALL instruction");
109 stack.push_back(edge.first);
127 std::vector<cfgt::node_indext> stack)
129 while(!stack.empty())
131 auto &node =
cfg[stack.back()];
134 if(node.reaches_assertion)
136 node.reaches_assertion =
true;
138 for(
const auto &edge : node.in)
140 const auto &pred_node =
cfg[edge.first];
142 if(pred_node.PC->is_end_function())
147 stack.push_back(edge.first);
150 std::prev(node.PC)->is_function_call(),
151 "all function return edges should point to the successor of a "
152 "FUNCTION_CALL instruction");
156 else if(pred_node.PC->is_function_call())
163 stack.push_back(edge.first);
179 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
183 std::vector<cfgt::node_indext> return_sites =
199 const cfgt::nodet &call_node,
200 std::vector<cfgt::node_indext> &callsite_successor_stack,
201 std::vector<cfgt::node_indext> &callee_head_stack)
205 INVARIANT(call_node.out.size() == 1,
"Call sites should have one successor");
206 const auto successor_index = call_node.out.begin()->first;
208 auto callsite_successor_pc = std::next(call_node.PC);
210 auto successor_pc =
cfg[successor_index].PC;
214 callee_head_stack.push_back(successor_index);
217 while(!successor_pc->is_end_function())
221 callsite_successor_stack.push_back(
227 callsite_successor_stack.push_back(successor_index);
237 std::vector<reachability_slicert::cfgt::node_indext>
239 std::vector<cfgt::node_indext> stack)
241 std::vector<cfgt::node_indext> called_function_heads;
243 while(!stack.empty())
245 auto &node =
cfg[stack.back()];
248 if(node.reachable_from_assertion)
250 node.reachable_from_assertion =
true;
252 if(node.PC->is_function_call())
261 for(
const auto &edge : node.out)
262 stack.push_back(edge.first);
266 return called_function_heads;
277 std::vector<cfgt::node_indext> stack)
279 while(!stack.empty())
281 auto &node =
cfg[stack.back()];
284 if(node.reachable_from_assertion)
286 node.reachable_from_assertion =
true;
288 if(node.PC->is_function_call())
293 else if(node.PC->is_end_function())
302 for(
const auto &edge : node.out)
303 stack.push_back(edge.first);
318 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
322 std::vector<cfgt::node_indext> return_sites =
338 if(gf_entry.second.body_available())
344 !e.reaches_assertion && !e.reachable_from_assertion &&
345 !i_it->is_end_function())
369 const bool include_forward_reachability)
385 const std::list<std::string> &properties,
386 const bool include_forward_reachability)
400 const std::list<std::string> &functions_list)
402 for(
const auto &
function : functions_list)
432 const std::list<std::string> &properties)