33std::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;
75std::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);
237std::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)
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
const source_locationt & source_location() const
The Boolean constant false.
A collection of goto functions.
void compute_loop_numbers()
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst::const_iterator const_targett
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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,...
bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2) const
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,...
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,...
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,...
void forward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
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.
#define Forall_goto_program_instructions(it, program)
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.
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.
Remove calls to functions without a body.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void remove_unreachable(goto_programt &goto_program)
remove unreachable code