Use the linker when adding library functions

This enables type checking of missing functions vs library-provided functions,
and also enables type sanitisation as done by the linker.

Author: tautschnig

src/ansi-c/cprover_library.cpp

@@ -76,7 +76,8 @@ std::string get_cprover_library_text(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_tablet &symbol_table,
+  const symbol_tablet &symbol_table,
+  symbol_tablet &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
@@ -86,7 +87,7 @@ void cprover_c_library_factory(
 
   library_text=get_cprover_library_text(functions, symbol_table);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }
 
 void add_library(

src/ansi-c/cprover_library.h

@@ -34,6 +34,7 @@ void add_library(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_tablet &,
   symbol_tablet &,
   message_handlert &);
 

src/cpp/cprover_library.cpp

@@ -37,7 +37,8 @@ static std::string get_cprover_library_text(
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_tablet &symbol_table,
+  const symbol_tablet &symbol_table,
+  symbol_tablet &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE)
@@ -46,5 +47,5 @@ void cprover_cpp_library_factory(
   const std::string library_text =
     get_cprover_library_text(functions, symbol_table);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }

src/cpp/cprover_library.h

@@ -18,6 +18,7 @@ class symbol_tablet;
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_tablet &,
   symbol_tablet &,
   message_handlert &);
 

src/goto-programs/link_goto_model.cpp

@@ -97,6 +97,7 @@ static bool link_functions(
 
         in_dest_symbol_table.body.swap(src_func.body);
         in_dest_symbol_table.type=src_func.type;
+        in_dest_symbol_table.parameter_identifiers = src_func.parameter_identifiers;
       }
       else if(src_func.body.instructions.empty() ||
               src_ns.lookup(src_it->first).is_weak)

src/goto-programs/link_to_library.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "compute_called_functions.h"
 #include "goto_convert_functions.h"
+#include "link_goto_model.h"
 
 /// Complete missing function definitions using the \p library.
 /// \param goto_model: goto model that may contain function calls and symbols
@@ -25,7 +26,7 @@ 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 &)>
+    void(const std::set<irep_idt> &, const symbol_tablet &, symbol_tablet &, message_handlert &)>
     &library)
 {
   // this needs a fixedpoint, as library functions
@@ -65,23 +66,26 @@ void link_to_library(
     if(missing_functions.empty())
       break;
 
-    library(missing_functions, goto_model.symbol_table, message_handler);
+    goto_modelt library_model;
+    library(missing_functions, goto_model.symbol_table, library_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())
+        library_model.symbol_table.symbols.find(id) !=
+        library_model.symbol_table.symbols.end())
       {
         goto_convert(
           id,
-          goto_model.symbol_table,
-          goto_model.goto_functions,
+          library_model.symbol_table,
+          library_model.goto_functions,
           message_handler);
       }
 
       added_functions.insert(id);
     }
+
+    link_goto_model(goto_model, library_model, message_handler);
   }
 }

src/goto-programs/link_to_library.h

@@ -27,6 +27,6 @@ void link_to_library(
   goto_modelt &,
   message_handlert &,
   const std::function<
-    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)> &);
+    void(const std::set<irep_idt> &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &);
 
 #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H