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-07/main.c

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

regression/cbmc/String_Abstraction17/strcpy-no-decl.c

@@ -1,4 +1,5 @@
-void *malloc(unsigned);
+#include <stdlib.h>
+// string.h intentionally omitted
 
 char *make_str()
 {

regression/cbmc/String_Abstraction17/test.desc

@@ -1,11 +1,13 @@
 CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
-Condition: strlen type inconsistency
-^EXIT=(127|134)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-While this test currently passes when omitting --validate-goto-model, we should
-expect a report of type inconsistencies as no forward declarations are present.
+The linker is able to fix up type inconsistencies of the missing function
+declarations, but the absence of a declaration of strlen results in not picking
+up the library model. Consequently the assumption does not work as intended, and
+verification fails. Adding #include <string.h> makes verification pass as
+expected.

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

@@ -98,7 +98,8 @@ std::string get_cprover_library_text(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
@@ -107,7 +108,7 @@ void cprover_c_library_factory(
   std::string library_text =
     get_cprover_library_text(functions, symbol_table, false);
 
-  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

@@ -41,6 +41,7 @@ void add_library(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   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_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &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_table_baset;
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   message_handlert &);