Skip to content

Commit edbd1fd

Browse files
committed
Check cbmc-library regressions for completeness
This will make sure that newly added library functions are also covered by tests.
1 parent cb9f69a commit edbd1fd

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

src/ansi-c/library_check.sh

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,10 @@ for f in "$@"; do
1717
rm __libcheck.s __libcheck.i __libcheck.c
1818
[ "${ec}" -eq 0 ] || exit "${ec}"
1919
done
20+
21+
grep '^/\* FUNCTION:' ../*/library/* | cut -f3 -d" " | sort -u > __functions
22+
ls ../../regression/cbmc-library/ | grep -- - | cut -f1 -d- | sort -u > __tests
23+
diff -u __tests __functions
24+
ec="${?}"
25+
rm __functions __tests
26+
exit "${ec}"

0 commit comments

Comments
 (0)