58 std::set<irep_idt> added_functions;
62 std::unordered_set<irep_idt> called_functions =
67 std::set<irep_idt> missing_functions;
69 for(
const auto &
id : called_functions)
71 goto_functionst::function_mapt::const_iterator
75 f_it->second.body_available())
79 else if(added_functions.find(
id)!=added_functions.end())
84 missing_functions.insert(
id);
88 if(missing_functions.empty())
91 library(missing_functions, symbol_table, message_handler);
94 for(
const auto &
id : missing_functions)
97 goto_convert(
id, symbol_table, goto_functions, message_handler);
99 added_functions.insert(
id);
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
A collection of goto functions.
Goto Programs with Functions.
goto_functionst goto_functions
GOTO functions.