Feature #7627
openSV-COMP compilation issues for clang compiler
0%
Description
For compilation with clang there are a number of issues before the verification benchmarks generated by Klever can be accepted.
1. __builtin_va_start has diffrent signature in clang
linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-net-wireless-b43legacy-b43legacy_unknown-unreach-call.cil.c:8586:47: error: too few arguments to function call, expected at least 2, have 1 __builtin_va_start((__va_list_tag *)(& args)); ^
workaround:
replace __builtin_va_start by ldv__builtin_va_start
2. __builtin_va_end has diffrent signature in clang
linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-net-wireless-b43legacy-b43legacy_unknown-unreach-call.cil.c:8600:20: warning: incompatible pointer types passing '__va_list_tag *' (aka 'struct __va_list_tag *') to parameter of type '__va_list_tag *' (aka 'struct __va_list_tag *') [-Wincompatible-pointer-types] __builtin_va_end((__va_list_tag *)(& args)); ^~~~~~~~~~~~~~~~~~~~~~~~~
workaround:
replace __builtin_va_end by ldv__builtin_va_end
3. __builtin_trap should not be defined in clang
linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-dvb-core-dvb-core_unknown-unreach-call.cil.c:27928:6: error: definition of builtin function '__builtin_trap' void __builtin_trap(void) ^
workaround:
replace __builtin_trap by ldv__builtin_trap
4. __builtin_expect should not be defined in clang
linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-dvb-core-dvb-core_unknown-unreach-call.cil.c:27920:6: error: definition of builtin function '__builtin_expect' long __builtin_expect(long exp , long c ) ^
workaround:
replace __builtin_expect by ldv__builtin_expect
5. __builtin_bswap32 and __builtin_bswap64 have diffrent signatures in clang
linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-pci-bt8xx-bttv_unknown-unreach-call.cil.c:24700:5: error: conflicting types for '__builtin_bswap32' int __builtin_bswap32(int ) ; ^
workaround:
delete declarations of __builtin_bswap32 and __builtin_bswap64
6. __builtin_unreachable has diffrent signature in clang
workaround:
delete declaration __builtin_unreachable
7. entry function should have signature 'int main' instead of 'void main'
workaround:
rename 'void main' to 'int main' and add return value
Files
Updated by Evgeny Novikov about 8 years ago
- Project changed from Klever to C Instrumentation Framework
Everything except the last item doesn't belong to Klever but to CIF C-backend. For the last item I suggest to open another issue.
Updated by Vadim Mutilin about 8 years ago
- File fix_clang_errors.sh fix_clang_errors.sh added
magic script