32 std::vector<reachability_slicert::cfgt::node_indext>
37 std::vector<cfgt::node_indext> sources;
40 if(
criterion(e_it.first) || is_threaded(e_it.first))
41 sources.push_back(e_it.second);
53 return it1->function == it2->function && it1 == it2;
66 std::vector<search_stack_entryt>
stack;
68 for(
const auto source : sources)
69 stack.emplace_back(source,
false);
73 auto &node =
cfg[
stack.back().node_index];
74 const auto caller_is_known =
stack.back().caller_is_known;
77 if(node.reaches_assertion)
79 node.reaches_assertion =
true;
81 for(
const auto &edge : node.in)
83 const auto &pred_node =
cfg[edge.first];
85 if(pred_node.PC->is_end_function())
90 std::prev(node.PC)->is_function_call(),
91 "all function return edges should point to the successor of a " 92 "FUNCTION_CALL instruction");
93 stack.emplace_back(edge.first,
true);
97 else if(pred_node.PC->is_function_call())
101 if(!caller_is_known ||
is_same_target(std::next(pred_node.PC), node.PC))
102 stack.emplace_back(edge.first, caller_is_known);
106 stack.emplace_back(edge.first, caller_is_known);
122 std::vector<search_stack_entryt>
stack;
124 for(
const auto source : sources)
125 stack.emplace_back(source,
false);
127 while(!
stack.empty())
129 auto &node =
cfg[
stack.back().node_index];
130 const auto caller_is_known =
stack.back().caller_is_known;
133 if(node.reachable_from_assertion)
135 node.reachable_from_assertion =
true;
137 if(node.PC->is_function_call())
141 INVARIANT(node.out.size() == 1,
"Call sites should have one successor");
142 const auto successor_index = node.out.begin()->first;
146 const auto &callee_head_node =
cfg[successor_index];
147 auto callee_it = callee_head_node.PC;
150 stack.emplace_back(successor_index,
true);
153 while(!callee_it->is_end_function())
165 stack.emplace_back(successor_index, caller_is_known);
168 else if(node.PC->is_end_function() && caller_is_known)
178 for(
const auto &edge : node.out)
179 stack.emplace_back(edge.first, caller_is_known);
192 if(f_it->second.body_available())
198 !e.reaches_assertion && !e.reachable_from_assertion &&
199 !i_it->is_end_function())
219 const bool include_forward_reachability)
235 const std::list<std::string> &properties,
236 const bool include_forward_reachability)
259 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...
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
#define INVARIANT(CONDITION, REASON)
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...
The boolean constant false.
std::vector< cfgt::node_indext > get_sources(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent executi...
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)
void fixedpoint_from_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
goto_programt coverage_criteriont criterion
static bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2)
void fixedpoint_to_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform backwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
#define Forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.