diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 1672308593a..56cf0ec9025 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -28,11 +28,62 @@ void link_to_library( void(const std::set &, symbol_tablet &, message_handlert &)> &library) { - link_to_library( - goto_model.symbol_table, - goto_model.goto_functions, - message_handler, - 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_model.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_model.goto_functions.function_map.find(id); + + if( + f_it != goto_model.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, goto_model.symbol_table, message_handler); + + // convert to CFG + for(const auto &id : missing_functions) + { + if( + goto_model.symbol_table.symbols.find(id) != + goto_model.symbol_table.symbols.end()) + { + goto_convert( + id, + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); + } + + added_functions.insert(id); + } + } } /// Complete missing function definitions using the \p library. diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h index 495c43de244..4d2222fa5e4 100644 --- a/src/goto-programs/link_to_library.h +++ b/src/goto-programs/link_to_library.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include class goto_functionst; @@ -22,6 +23,7 @@ class goto_modelt; class message_handlert; class symbol_tablet; +DEPRECATED("Use link_to_library(goto_model, ...) instead") void link_to_library( symbol_tablet &, goto_functionst &,