29 std::set<irep_idt> used_functions;
30 std::list<goto_functionst::function_mapt::iterator> unused_functions;
34 for(goto_functionst::function_mapt::iterator it=
39 if(used_functions.find(it->first)==used_functions.end())
40 unused_functions.push_back(it);
45 if(!unused_functions.empty())
48 <<
"Dropping " << unused_functions.size() <<
" of " <<
53 for(
const auto &f : unused_functions)
60 std::set<irep_idt> &seen)
62 std::pair<std::set<irep_idt>::const_iterator,
bool> res =
69 goto_functionst::function_mapt::const_iterator f_it =
74 for(
const auto &instruction : f_it->second.body.instructions)
76 if(instruction.is_function_call())
78 const auto &
function = instruction.call_function();
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
goto_functionst goto_functions
GOTO functions.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & statistics() const
const irep_idt & get_identifier() const
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
void find_used_functions(const irep_idt &start, goto_functionst &functions, std::set< irep_idt > &seen)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.