Merge pull request #7475 from tautschnig/bugfixes/library-inline

Library functions may require converting additional inline functions

Author: kroening

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

@@ -1,9 +1,14 @@
 #include <assert.h>
 #include <math.h>
 
+int __signbitd(double);
+int __signbitf(float);
+
 int main()
 {
-  __signbitd();
-  assert(0);
+  float f;
+  double df = (double)f;
+  __CPROVER_assert(
+    isnan(f) || __signbitd(df) == __signbitf(f), "cast preserves sign");
   return 0;
 }

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

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

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/ansi-c/compiler_headers/gcc_builtin_headers_math.h

@@ -339,7 +339,7 @@ long double __builtin_scalblnl(long double, long);
 double __builtin_scalbn(double, int);
 float __builtin_scalbnf(float, int);
 long double __builtin_scalbnl(long double, int);
-int __builtin_signbit(double);
+int __builtin_signbit(); // this is type-generic
 int __builtin_signbitf(float);
 int __builtin_signbitl(long double);
 double __builtin_significand(double);

src/ansi-c/library/math.c

@@ -2400,7 +2400,7 @@ float fabsf (float d);
 
 float copysignf(float x, float y)
 {
-  float abs = fabs(x);
+  float abs = fabsf(x);
   return (signbit(y)) ? -abs : abs;
 }
 

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;