Skip to content

Commit 04886f5

Browse files
committed
C library check: silence warnings about GNU-style line markers
Clang 15 complains about GNU-style line markers (`# <number>` instead of `#line <number>`), which we don't need to do anything about. Fixes: #7525
1 parent 77e7bfe commit 04886f5

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/ansi-c/library_check.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ for f in "$@"; do
1414
perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
1515
$CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
1616
$CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
17-
-o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
17+
-o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas \
18+
-Wno-gnu-line-marker -Wno-unknown-warning-option
1819
ec="${?}"
1920
rm __libcheck.s __libcheck.i __libcheck.c
2021
[ "${ec}" -eq 0 ] || exit "${ec}"

0 commit comments

Comments
 (0)