Fix and refactor library_check target

src/ansi-c/CMakeLists.txt

@@ -39,7 +39,7 @@ file(GLOB library_check_sources "library/*.c")
 list(REMOVE_ITEM library_check_sources ${platform_unavail})
 
 add_custom_target(library_check
-    ${CMAKE_CURRENT_SOURCE_DIR}/check_library.sh ${library_check_sources}
+    ${CMAKE_CURRENT_SOURCE_DIR}/library_check.sh ${library_check_sources}
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
 
@@ -93,3 +93,5 @@ add_library(ansi-c
 generic_includes(ansi-c)
 
 target_link_libraries(ansi-c util linking goto-programs assembler)
+
+add_dependencies(ansi-c library_check)

src/ansi-c/Makefile

@@ -92,20 +92,7 @@ else
   platform_unavail = library/java.io.c library/threads.c
 endif
 library_check: library/*.c
-	for f in $(filter-out $(platform_unavail), $^) ; do \
-		echo "Checking $$f" ; \
-		cp $$f __libcheck.c ; \
-		perl -p -i -e 's/(__builtin_[^v])/s$$1/' __libcheck.c ; \
-		perl -p -i -e 's/(__sync_)/s$$1/' __libcheck.c ; \
-		perl -p -i -e 's/(__noop)/s$$1/' __libcheck.c ; \
-		$(CC) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \
-			-D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \
-		$(CC) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \
-			-Wno-unused-label ; \
-		ec=$$? ; \
-		$(RM) __libcheck.s __libcheck.i __libcheck.c ; \
-		[ $$ec -eq 0 ] || exit $$ec ; \
-	done
+	./library_check.sh $(filter-out $(platform_unavail), $^)
 	touch $@
 
 cprover_library.inc: library/converter$(EXEEXT) library/*.c

src/ansi-c/check_library.sh → src/ansi-c/library_check.sh

@@ -1,14 +1,14 @@
 #!/usr/bin/env bash
 
-for var in "$@"; do
-    cp "${var}" __libcheck.c
-    sed -i 's/__builtin_[^v]/s&/' __libcheck.c
-    sed -i 's/__sync_/s&/' __libcheck.c
-    sed -i 's/__noop/s&/' __libcheck.c
+for f in "$@"; do
+    echo "Checking ${f}"
+    cp "${f}" __libcheck.c
+    perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
+    perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
+    perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
     cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
-    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label -Wno-uninitialized
-
-    ec="$?"
+    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
+    ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"
 done