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.

Co-authored-by: Peter Schrammel <[email protected]>

Author: tautschnig

regression/cbmc-library/__errno_location-01/main.c

@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <errno.h>
 
-int main()
+int main(int arc, char *argv[])
 {
-  __errno_location();
-  assert(0);
+  // errno expands to use of __errno_location() with glibc
+  assert(errno == 0);
   return 0;
 }

regression/cbmc-library/__errno_location-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc-library/memcpy-06/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 
 function 'memcpy' is not declared
-parameter "memcpy::dst" type mismatch
-^EXIT=6$
+Linking library function 'memcpy' failed
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-library/memcpy-07/main.c

@@ -1,4 +1,5 @@
 // #include <string.h> intentionally omitted
+void *memcpy();
 
 struct c
 {

regression/cbmc/String_Abstraction17/test.desc

@@ -1,7 +1,7 @@
 CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
-Condition: strlen type inconsistency
+^Condition: fct_type.parameters\(\).size\(\) == parameter_identifiers.size\(\)$
 ^EXIT=(127|134)$
 ^SIGNAL=0$
 --

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c

@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 // This file is highly reduced from some open source projects.
 // The following four lines are adapted from the openssl library
 // Full repository here:

src/ansi-c/cprover_library.cpp

@@ -94,7 +94,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)
@@ -104,7 +105,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

@@ -36,6 +36,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 &);