33std::vector<reachability_slicert::cfgt::node_indext>
38 std::vector<cfgt::node_indext>
sources;
43 is_threaded(
e_it.first))
50 "no slicing criterion found",
52 "provide at least one property using --property <property>"};
75std::vector<reachability_slicert::cfgt::node_indext>
77 std::vector<cfgt::node_indext> stack)
83 auto &node =
cfg[stack.back()];
86 if(node.reaches_assertion)
88 node.reaches_assertion =
true;
90 for(
const auto &edge : node.in)
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)
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);
237std::vector<reachability_slicert::cfgt::node_indext>
239 std::vector<cfgt::node_indext> stack)
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);
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);
338 if(
gf_entry.second.body_available())
344 !e.reaches_assertion && !e.reachable_from_assertion &&
345 !
i_it->is_end_function())
385 const std::list<std::string> &properties,
432 const std::list<std::string> &properties)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.