diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 56cf0ec9025..2274cfd2473 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -85,69 +85,3 @@ void link_to_library( } } } - -/// Complete missing function definitions using the \p library. -/// \param symbol_table: symbol table that may contain symbols with missing -/// function bodies -/// \param goto_functions: goto functions that may contain function calls with -/// missing function bodies -/// \param message_handler: message handler to report library processing -/// problems -/// \param library: generator function that produces function definitions for a -/// given set of symbol names that have no body. -void link_to_library( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, - message_handlert &message_handler, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> - &library) -{ - // this needs a fixedpoint, as library functions - // may depend on other library functions - - std::set added_functions; - - while(true) - { - std::unordered_set called_functions = - compute_called_functions(goto_functions); - - // eliminate those for which we already have a body - - std::set missing_functions; - - for(const auto &id : called_functions) - { - goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.find(id); - - if(f_it!=goto_functions.function_map.end() && - f_it->second.body_available()) - { - // it's overridden! - } - else if(added_functions.find(id)!=added_functions.end()) - { - // already added - } - else - missing_functions.insert(id); - } - - // done? - if(missing_functions.empty()) - break; - - library(missing_functions, symbol_table, message_handler); - - // convert to CFG - for(const auto &id : missing_functions) - { - if(symbol_table.symbols.find(id)!=symbol_table.symbols.end()) - goto_convert(id, symbol_table, goto_functions, message_handler); - - added_functions.insert(id); - } - } -} diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h index 14c43a1b745..ac772a05cae 100644 --- a/src/goto-programs/link_to_library.h +++ b/src/goto-programs/link_to_library.h @@ -18,19 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class goto_functionst; class goto_modelt; class message_handlert; class symbol_tablet; -DEPRECATED(SINCE(2019, 2, 28, "Use link_to_library(goto_model, ...) instead")) -void link_to_library( - symbol_tablet &, - goto_functionst &, - message_handlert &, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> &); - void link_to_library( goto_modelt &, message_handlert &,