File tree Expand file tree Collapse file tree 3 files changed +12
-23
lines changed
Expand file tree Collapse file tree 3 files changed +12
-23
lines changed Original file line number Diff line number Diff line change @@ -39,7 +39,7 @@ file(GLOB library_check_sources "library/*.c")
3939list (REMOVE_ITEM library_check_sources ${platform_unavail} )
4040
4141add_custom_target (library_check
42- ${CMAKE_CURRENT_SOURCE_DIR} /check_library .sh ${library_check_sources}
42+ ${CMAKE_CURRENT_SOURCE_DIR} /library_check .sh ${library_check_sources}
4343 WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
4444)
4545
@@ -93,3 +93,5 @@ add_library(ansi-c
9393generic_includes(ansi-c)
9494
9595target_link_libraries (ansi-c util linking goto-programs assembler)
96+
97+ add_dependencies (ansi-c library_check)
Original file line number Diff line number Diff line change 9292 platform_unavail = library/java.io.c library/threads.c
9393endif
9494library_check : library/* .c
95- for f in $( filter-out $( platform_unavail) , $^) ; do \
96- echo " Checking $$ f" ; \
97- cp $$ f __libcheck.c ; \
98- perl -p -i -e ' s/(__builtin_[^v])/s$$1/' __libcheck.c ; \
99- perl -p -i -e ' s/(__sync_)/s$$1/' __libcheck.c ; \
100- perl -p -i -e ' s/(__noop)/s$$1/' __libcheck.c ; \
101- $(CC ) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \
102- -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \
103- $(CC ) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \
104- -Wno-unused-label ; \
105- ec=$$? ; \
106- $(RM ) __libcheck.s __libcheck.i __libcheck.c ; \
107- [ $$ ec -eq 0 ] || exit $$ ec ; \
108- done
95+ ./library_check.sh $(filter-out $(platform_unavail ) , $^ )
10996 touch $@
11097
11198cprover_library.inc : library/converter$(EXEEXT ) library/* .c
Original file line number Diff line number Diff line change 11#! /usr/bin/env bash
22
3- for var in " $@ " ; do
4- cp " ${var} " __libcheck.c
5- sed -i ' s/__builtin_[^v]/s&/' __libcheck.c
6- sed -i ' s/__sync_/s&/' __libcheck.c
7- sed -i ' s/__noop/s&/' __libcheck.c
3+ for f in " $@ " ; do
4+ echo " Checking ${f} "
5+ cp " ${f} " __libcheck.c
6+ perl -p -i -e ' s/(__builtin_[^v])/s$1/' __libcheck.c
7+ perl -p -i -e ' s/(__sync_)/s$1/' __libcheck.c
8+ perl -p -i -e ' s/(__noop)/s$1/' __libcheck.c
89 cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
9- cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label -Wno-uninitialized
10-
11- ec=" $? "
10+ cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
11+ ec=" ${?} "
1212 rm __libcheck.s __libcheck.i __libcheck.c
1313 [ " ${ec} " -eq 0 ] || exit " ${ec} "
1414done
You can’t perform that action at this time.
0 commit comments