36 std::vector<reachability_slicert::cfgt::node_indext>
41 std::vector<cfgt::node_indext> sources;
45 criterion(
cfg[e_it.second].function_id, e_it.first) ||
46 is_threaded(e_it.first))
47 sources.push_back(e_it.second);
53 "no slicing criterion found",
55 "provide at least one property using --property <property>"};
69 return node1.function_id == node2.function_id && it1 == it2;
78 std::vector<reachability_slicert::cfgt::node_indext>
80 std::vector<cfgt::node_indext> stack)
82 std::vector<cfgt::node_indext> return_sites;
86 auto &node =
cfg[stack.back()];
89 if(node.reaches_assertion)
91 node.reaches_assertion =
true;
93 for(
const auto &edge : node.in)
95 const auto &pred_node =
cfg[edge.first];
97 if(pred_node.PC->is_end_function())
101 return_sites.push_back(edge.first);
104 std::prev(node.PC)->is_function_call(),
105 "all function return edges should point to the successor of a "
106 "FUNCTION_CALL instruction");
112 stack.push_back(edge.first);
130 std::vector<cfgt::node_indext> stack)
132 while(!stack.empty())
134 auto &node =
cfg[stack.back()];
137 if(node.reaches_assertion)
139 node.reaches_assertion =
true;
141 for(
const auto &edge : node.in)
143 const auto &pred_node =
cfg[edge.first];
145 if(pred_node.PC->is_end_function())
150 stack.push_back(edge.first);
153 std::prev(node.PC)->is_function_call(),
154 "all function return edges should point to the successor of a "
155 "FUNCTION_CALL instruction");
159 else if(pred_node.PC->is_function_call())
166 stack.push_back(edge.first);
182 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
186 std::vector<cfgt::node_indext> return_sites =
202 const cfgt::nodet &call_node,
203 std::vector<cfgt::node_indext> &callsite_successor_stack,
204 std::vector<cfgt::node_indext> &callee_head_stack)
208 INVARIANT(call_node.out.size() == 1,
"Call sites should have one successor");
209 const auto successor_index = call_node.out.begin()->first;
211 auto callsite_successor_pc = std::next(call_node.PC);
213 auto successor_pc =
cfg[successor_index].PC;
217 callee_head_stack.push_back(successor_index);
220 while(!successor_pc->is_end_function())
224 callsite_successor_stack.push_back(
230 callsite_successor_stack.push_back(successor_index);
240 std::vector<reachability_slicert::cfgt::node_indext>
242 std::vector<cfgt::node_indext> stack)
244 std::vector<cfgt::node_indext> called_function_heads;
246 while(!stack.empty())
248 auto &node =
cfg[stack.back()];
251 if(node.reachable_from_assertion)
253 node.reachable_from_assertion =
true;
255 if(node.PC->is_function_call())
264 for(
const auto &edge : node.out)
265 stack.push_back(edge.first);
269 return called_function_heads;
280 std::vector<cfgt::node_indext> stack)
282 while(!stack.empty())
284 auto &node =
cfg[stack.back()];
287 if(node.reachable_from_assertion)
289 node.reachable_from_assertion =
true;
291 if(node.PC->is_function_call())
296 else if(node.PC->is_end_function())
305 for(
const auto &edge : node.out)
306 stack.push_back(edge.first);
321 std::vector<cfgt::node_indext> sources =
get_sources(is_threaded, criterion);
325 std::vector<cfgt::node_indext> return_sites =
340 if(f_it->second.body_available())
346 !e.reaches_assertion && !e.reachable_from_assertion &&
347 !i_it->is_end_function())
370 const bool include_forward_reachability)
386 const std::list<std::string> &properties,
387 const bool include_forward_reachability)
401 const std::list<std::string> &functions_list)
403 for(
const auto &
function : functions_list)
433 const std::list<std::string> &properties)