``regression`` benchmarks contain GCC compiler built-ins which Clang cannot handle

[sosy-lab]

``regression`` benchmarks contain GCC compiler built-ins which Clang cannot handle

[tautschnig]

If travis-ci/travis-ci#2877 got fixed, we could have separate configurations for SV-COMP (with SET_FILES being set) vs. all benchmarks.

That should address @PhilippWendler's concerns voiced on the SV-COMP mailing list.

Best,
Michael

[delcypher]

@tautschnig
We can do this already if we want. If you take a look at .travis.yml in the root of the repository you will see these lines

  - C_COMPILER=gcc-4.8 SYNTAX_ONLY=1 WARNINGS_AS_ERRORS=0 VERBOSE=0 SUPPRESS_WARNINGS=1 REPORT_CC_FILE=2
  - C_COMPILER=clang-3.7 CLANG_BUILD_HACK=1 SYNTAX_ONLY=1 WARNINGS_AS_ERRORS=0 VERBOSE=0 SUPPRESS_WARNINGS=1 REPORT_CC_FILE=2

Each line sets a build configuration (i.e. we test two different configurations) with different environment variables. Currently we build with gcc-4.8 and clang-3.7. CLANG_BUILD_HACK is only there to prevent Clang trying to build the regression benchmarks mentioned in this issue.

We could easily add another configuration that only builds certain set files.
However I think that all benchmarks that exist in the repository should be compilable, otherwise they are useless. I'd rather we just ask the author of the benchmarks to fix them and if that fails just delete the benchmarks.

[tautschnig]

While I agree that in medium term we should have compilable files only in the repository, that's just not doable on the spot. So I was hoping we could have multiple "Build (not) passing" indicators in README.md, one for the SV-COMP sub-set and another for all benchmarks.

[delcypher]

So I was hoping we could have multiple "Build (not) passing" indicators in README.md, one for the SV-COMP sub-set and another for all benchmarks.

I see to my knowledge TravisCI cannot do this right now.

[mutilin]

As far as I understood it is fixed

[PhilippWendler]

I don't know. In the last relevant commit to this directory (edc4741), @delcypher claimed that the problem persists.

[delcypher]

@mutilin @PhilippWendler No this is still broken

Try

cd c c/regression
make clean
CC=clang make

I get output like this

clang building regression/drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3238:20: warning: variable 'var_group1' is uninitialized when used here [-Wuninitialized]
    mt2266_release(var_group1);
                   ^~~~~~~~~~
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3219:34: note: initialize the variable 'var_group1' to silence this warning
  struct dvb_frontend *var_group1 ;
                                 ^
                                  = 0
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3262:36: warning: variable 'var_mt2266_get_bandwidth_6_p1' is uninitialized when used here [-Wuninitialized]
  mt2266_get_bandwidth(var_group1, var_mt2266_get_bandwidth_6_p1);
                                   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3222:37: note: initialize the variable 'var_mt2266_get_bandwidth_6_p1' to silence this warning
  u32 *var_mt2266_get_bandwidth_6_p1 ;
                                    ^
                                     = 0
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3258:36: warning: variable 'var_mt2266_get_frequency_5_p1' is uninitialized when used here [-Wuninitialized]
  mt2266_get_frequency(var_group1, var_mt2266_get_frequency_5_p1);
                                   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3221:37: note: initialize the variable 'var_mt2266_get_frequency_5_p1' to silence this warning
  u32 *var_mt2266_get_frequency_5_p1 ;
                                    ^
                                     = 0
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3254:33: warning: variable 'var_group2' is uninitialized when used here [-Wuninitialized]
  mt2266_set_params(var_group1, var_group2);
                                ^~~~~~~~~~
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3220:45: note: initialize the variable 'var_group2' to silence this warning
  struct dvb_frontend_parameters *var_group2 ;
                                            ^
                                             = 0
drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.i:3475:6: error: definition of builtin function '__builtin_expect'
long __builtin_expect(long exp , long c ) 
     ^
4 warnings and 1 error generated.
make: *** [..//Makefile.rules:229: /home/dan/dev/sv-benchmarks/c/bin/regression/drivers--media--common--tuners--mt2266.ko_000.b094516.39_7a.cil_true-unreach-call.oi] Error 1

The only reason that TravisCI doesn't currently fail is because I put in a hack to prevent the regression directory being traversed when building with clang.

You can see this at

sv-benchmarks/c/Makefile

Line 70 in dfe81a3

ifeq ($(CC_IS_CLANG)$(CLANG_BUILD_HACK),11)

[mutilin]

fixed in #189