goblint / bench

The benchmark suite
4 stars 5 forks source link

Add ldv regression benchmarks to incremental benchmarks #35

Open jerhard opened 1 year ago

jerhard commented 1 year ago

This PR imports benchmarks that were taken from https://gitlab.com/sosy-lab/software/regression-verification-tasks/-/tree/new-svcomp-spec. Further information on these benchmarks can be found here.

The benchmarks were processed with incremental-ldv.py to generate the patch files and create the benchmark sets in index/sets/ldv/. The file index/sets/ldv/combined.yaml contains all benchmarks that are imported; the other yaml files in index/sets/ldv/ contain the benchmarks per directory.

Problems

There are some significant problems with this benchmark set. In particular:

sim642 commented 1 year ago
  • Most of the benchmarks have syntax errors that cause Goblint to be unable to parse them.

Would be useful to have a CIL issue about this parsing error.

michael-schwarz commented 1 year ago

Iirc they were actually errors (the type of the implementation not matching the one given in the prototype in the same file) etc that GCC also flags. If we want to do something here, I don't think we should patch CIL to accept invalid programs, but rather fix the benchmarks.