Project

General

Profile

Actions

Feature #7627

open

SV-COMP compilation issues for clang compiler

Added by Vadim Mutilin over 7 years ago. Updated over 7 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Start date:
10/25/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

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

fix_clang_errors.sh (1.8 KB) fix_clang_errors.sh Vadim Mutilin, 11/18/2016 04:48 PM
Actions #1

Updated by Evgeny Novikov over 7 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.

Actions #2

Updated by Vadim Mutilin over 7 years ago

magic script

Actions

Also available in: Atom PDF