From 00183866ac8d1fec6c001af6933a847d9dfd5396 Mon Sep 17 00:00:00 2001
From: Reini Urban <reini.urban@gmail.com>
Date: Thu, 21 Dec 2023 08:46:43 +0100
Subject: [PATCH] library-check: fixup missing __builtin_ffs check

---
 src/ansi-c/library/math.c   | 7 +++++++
 src/ansi-c/library_check.sh | 9 +++++----
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index d707997972c..a1040989b73 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -317,6 +317,13 @@ long double __builtin_huge_vall(void)
 #pragma CPROVER check pop
 }
 
+/* FUNCTION: __builtin_ffs */
+
+//int __builtin_ffs(float f)
+//{
+//  return simplify_exprt::simplify_ffs(f);
+//}
+
 /* FUNCTION: _dsign */
 
 int _dsign(double d)
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 9d973341585..c97301bb745 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -22,7 +22,7 @@ for f in "$@"; do
     [ "${ec}" -eq 0 ] || exit "${ec}"
 done
 
-# Make sure all internal library functions have tests exercising them:
+echo Make sure all internal library functions have tests exercising them
 grep '^/\* FUNCTION:' ../*/library/* | cut -f3 -d" " | sort -u > __functions
 
 # Some functions are not expected to have tests:
@@ -81,7 +81,7 @@ perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.d
 
 # Some functions are covered by tests in other folders:
 perl -p -i -e 's/^__spawned_thread\n//' __functions # any pthread_create tests
-perl -p -i -e 's/^__builtin_ffsl?l?\n//' __functions # cbmc/__builtin_ffs-01
+#perl -p -i -e 's/^__builtin_ffsl?l?\n//' __functions # cbmc/__builtin_ffs-01
 perl -p -i -e 's/^__builtin_[su]addl?l?_overflow\n//' __functions # cbmc/gcc_builtin_add_overflow
 perl -p -i -e 's/^__builtin_[su]mull?l?_overflow\n//' __functions # cbmc/gcc_builtin_mul_overflow
 perl -p -i -e 's/^__builtin_[su]subl?l?_overflow\n//' __functions # cbmc/gcc_builtin_sub_overflow
@@ -101,13 +101,14 @@ perl -p -i -e 's/^_mm_setr_epi(16|32)\n//' __functions # cbmc/SIMD1
 perl -p -i -e 's/^_mm_setr_pi16\n//' __functions # cbmc/SIMD1
 perl -p -i -e 's/^_mm_subs_ep[iu]16\n//' __functions # cbmc/SIMD1
 
-ls ../../regression/cbmc-library/ | grep -- - | cut -f1 -d- | sort -u > __tests
+ls ../../regression/cbmc-library/ | grep -- -0 | cut -f1 -d- | sort -u > __tests
 diff -u __tests __functions
 ec="${?}"
-rm __functions __tests
 if [ $ec != 0 ]; then
   echo "Tests and library functions don't match."
   echo "Lines prefixed with - are tests not matching any library function."
   echo "Lines prefixed with + are functions lacking a test."
+else
+  rm __functions __tests
 fi
 exit "${ec}"