Skip to content

Commit e49c751

Browse files
committed
Improve ansi-c library syntax check and run via travis
1 parent 6d68345 commit e49c751

File tree

2 files changed

+7
-4
lines changed

2 files changed

+7
-4
lines changed

.travis.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff 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" &&

src/ansi-c/Makefile

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -94,14 +94,15 @@ else
9494
endif
9595
library_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 ; \

0 commit comments

Comments
 (0)