File tree Expand file tree Collapse file tree 2 files changed +7
-4
lines changed Expand file tree Collapse file tree 2 files changed +7
-4
lines changed Original file line number Diff line number Diff line change @@ -158,6 +158,8 @@ install:
158158 - ccache --max-size=1G
159159 - COMMAND="make -C src minisat2-download" &&
160160 eval ${PRE_COMMAND} ${COMMAND}
161+ - COMMAND="make -C src/ansi-c library_check" &&
162+ eval ${PRE_COMMAND} ${COMMAND}
161163 - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
162164 eval ${PRE_COMMAND} ${COMMAND}
163165 - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
Original file line number Diff line number Diff line change 9494endif
9595library_check : library/* .c
9696 for f in $( filter-out $( platform_unavail) , $^) ; do \
97+ echo " Checking $$ f" ; \
9798 cp $$ f __libcheck.c ; \
98- sed -i ' s/__builtin_[^v]/s& /' __libcheck.c ; \
99- sed -i ' s/__sync_/s& /' __libcheck.c ; \
100- sed -i ' s/__noop/s& /' __libcheck.c ; \
99+ perl -p -i -e ' s/( __builtin_[^v])/s$$1 /' __libcheck.c ; \
100+ perl -p -i -e ' s/( __sync_)/s$$1 /' __libcheck.c ; \
101+ perl -p -i -e ' s/( __noop)/s$$1 /' __libcheck.c ; \
101102 $(CC ) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \
102103 -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \
103104 $(CC ) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \
104- -Wno-unused-label -Wno-uninitialized ; \
105+ -Wno-unused-label ; \
105106 ec=$$? ; \
106107 $(RM ) __libcheck.s __libcheck.i __libcheck.c ; \
107108 [ $$ ec -eq 0 ] || exit $$ ec ; \
You can’t perform that action at this time.
0 commit comments