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 =
341 if(gf_entry.second.body_available())
347 !e.reaches_assertion && !e.reachable_from_assertion &&
348 !i_it->is_end_function())
372 const bool include_forward_reachability)
388 const std::list<std::string> &properties,
389 const bool include_forward_reachability)
403 const std::list<std::string> &functions_list)
405 for(
const auto &
function : functions_list)
435 const std::list<std::string> &properties)
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to 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