Check cbmc-library regressions for completeness

This will make sure that newly added library functions are also covered by
tests.

Author: tautschnig

src/ansi-c/library_check.sh

@@ -17,3 +17,53 @@ for f in "$@"; do
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"
 done
+
+# 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:
+sed -i '/^__CPROVER_jsa_synthesise$/d' __functions
+sed -i '/^java::java.io.InputStream.read:()I$/d' __functions
+
+# Some functions are implicitly covered by running on different operating
+# systems:
+sed -i '/^_fopen$/d' __functions # fopen, macOS
+sed -i '/^_pipe$/d' __functions # pipe, macOS
+sed -i '/^_time32$/d' __functions # time, Windows
+sed -i '/^_time64$/d' __functions # time, Windows
+
+# Some functions are covered by existing tests:
+sed -i '/^__builtin_clzl$/d' __functions # __builtin_clz-01
+sed -i '/^__builtin_clzll$/d' __functions # __builtin_clz-01
+sed -i '/^__builtin_ffsl$/d' __functions # __builtin_ffs-01
+sed -i '/^__builtin_ffsll$/d' __functions # __builtin_ffs-01
+sed -i '/^__lzcnt$/d' __functions # __builtin_clz-01
+sed -i '/^__lzcnt16$/d' __functions # __builtin_clz-01
+sed -i '/^__lzcnt64$/d' __functions # __builtin_clz-01
+sed -i '/^fclose_cleanup$/d' __functions # fopen
+
+# Some functions are covered by tests in other folders:
+sed -i '/^__builtin_sadd_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_saddl_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_saddll_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_smul_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_smull_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_smulll_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_ssub_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+sed -i '/^__builtin_ssubl_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+sed -i '/^__builtin_ssubll_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+sed -i '/^__builtin_uadd_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_uaddl_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_uaddll_overflow$/d' __functions # cbmc/gcc_builtin_add_overflow
+sed -i '/^__builtin_umul_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_umull_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_umulll_overflow$/d' __functions # cbmc/gcc_builtin_mul_overflow
+sed -i '/^__builtin_usub_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+sed -i '/^__builtin_usubl_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+sed -i '/^__builtin_usubll_overflow$/d' __functions # cbmc/gcc_builtin_sub_overflow
+
+ls ../../regression/cbmc-library/ | grep -- - | cut -f1 -d- | sort -u > __tests
+diff -u __tests __functions
+ec="${?}"
+rm __functions __tests
+exit "${ec}"