Library functions may require converting additional inline functions

Library functions may make use of (inline) functions defined in header
files. One such case is `copysignf`, which uses `signbit`, which in turn
is inlined on macOS. When these functions hadn't been seen before
linking the library, then converting just the `library_model` symbol
table would be insufficient for it would not include functions outside
our own model library. Fall back to the `goto_model` symbol table for
those cases.

This was originally reported via Kani in
model-checking/kani#1993.

Author: tautschnig

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

@@ -1,9 +1,13 @@
-#include <assert.h>
-#include <math.h>
+// Use a forward declaration instead of including math.h to demonstrate a bugfix
+// in library linking.
+float copysignf(float, float);
 
 int main()
 {
-  copysignf();
-  assert(0);
+  float x;
+  float y;
+  float result = copysignf(x, y);
+  __CPROVER_assert(
+    __CPROVER_signf(result) == __CPROVER_signf(y), "signs match");
   return 0;
 }

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

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

src/goto-programs/link_to_library.cpp

@@ -47,6 +47,19 @@ static std::pair<optionalt<replace_symbolt::expr_mapt>, bool> add_one_function(
       library_model.goto_functions,
       message_handler);
   }
+  // We might need a function that's outside our own library, but brought in via
+  // some header file included by the library. Those functions already exist in
+  // goto_model.symbol_table, but haven't been converted just yet.
+  else if(
+    goto_model.symbol_table.symbols.find(missing_function) !=
+    goto_model.symbol_table.symbols.end())
+  {
+    goto_convert(
+      missing_function,
+      goto_model.symbol_table,
+      library_model.goto_functions,
+      message_handler);
+  }
 
   // check whether additional initialization may be required
   bool init_required = false;