Merge pull request #4303 from tautschnig/deprecate-link_to_library

Deprecate link_to_library(goto_functions, symbol_table, ...) [blocks: #4296]

Author: tautschnig

src/goto-programs/link_to_library.cpp

@@ -28,11 +28,62 @@ void link_to_library(
     void(const std::set<irep_idt> &, 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<irep_idt> added_functions;
+
+  while(true)
+  {
+    std::unordered_set<irep_idt> called_functions =
+      compute_called_functions(goto_model.goto_functions);
+
+    // eliminate those for which we already have a body
+
+    std::set<irep_idt> 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.

src/goto-programs/link_to_library.h

@@ -15,13 +15,15 @@ Author: Daniel Kroening, [email protected]
 #include <functional>
 #include <set>
 
+#include <util/deprecate.h>
 #include <util/irep.h>
 
 class goto_functionst;
 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 &,