search

goblint / bench

The benchmark suite
4 stars 5 forks source link

Combined programs use outdated headers #15

Open sim642 opened 2 years ago

sim642 commented 2 years ago

Since https://github.com/goblint/analyzer/pull/547 analyzing the combined pthread programs produces CIL merging errors, because the pthread.c stub includes a modern pthread.h, but the benchmarks have included an older version of the header. The differences are in the sizes of arrays in some structs, which have been increased over time.

vesalvojdani commented 2 years ago

I think we concluded with Simmo that merged programs are simply inadmissible as benchmarks because we probably want to use the stub approach much more widely than just this one pthread thing, but almost all our other benchmarks are also merged. It's very convenient to work with these merged programs, but it's obviously better to document how to run it on the original repository.

vesalvojdani commented 2 years ago

Somewhat more worrying is that SV-COMP also includes merged programs, no? Fortunately, the headers are in sync with what we use, for now: https://github.com/goblint/bench/blob/7c8fa961aa455df6b05969dcbb620e0d1e86f0d4/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i#L3-L6

sim642 commented 2 years ago

I'm not that worried about sv-benchmarks because they have some CI job that checks whether the preprocessed files have been correctly preprocessed: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/ad265d07a04053bfcd80626ac1d30cec2d1c254e/.gitlab-ci.yml#L111-119.