29 for(cfgt::entry_mapt::iterator
33 if(criterion(e_it->first) ||
34 is_threaded(e_it->first))
35 queue.push(e_it->second);
43 if(node.reaches_assertion)
46 node.reaches_assertion=
true;
48 for(cfgt::edgest::const_iterator
53 queue.push(p_it->first);
64 if(f_it->second.body_available())
69 if(!e.reaches_assertion &&
70 !i_it->is_end_function())
92 const std::list<std::string> &properties)
void fixedpoint_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
std::stack< cfgt::entryt > queuet
void slice(goto_functionst &goto_functions)
The boolean constant false.
void reachability_slicer(goto_functionst &goto_functions)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)