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)
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
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,...
void compute_loop_numbers()
Remove calls to functions without a body.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
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
const edgest & out(node_indext n) const
instructionst::const_iterator const_targett
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.
The Boolean constant false.
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.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
static bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2)
#define Forall_goto_program_instructions(it, program)
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,...
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,...
goto_functionst goto_functions
GOTO functions.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.