Skip to content

Adjust bench defs to sv-benchmarks updates

Closes !123 (closed) because the changes by @Po-Chun-Chien are included here.

Adjust to this change: sosy-lab/benchmarking/sv-benchmarks@6a611de3

Because the set files are unmerged now, we can keep the old categories as-is. There was never a decision to merge any categories in Test-Comp, so I keep the old categories.

In addition, add new categories that now also have coverage-* tasks.

We can not include two task directories because of the way sv-benchmark sets are currently structured: sv-benchmarks/c/memsafety-ext3 is only included in NoOverflows-Main.set and MemSafety-Other.set, and sv-benchmarks/c/pthread-memsafety is only included in MemSafety-Other.set. But the two set files also contain lots of other tasks from other categories, for example loop/ (full list below). If we included these two sets this would either create a messed-up categories that includes a subset of tasks from many other categories, or we would have to exclude a lot of directories manually.

To avoid this, the easiest solution is to just not include these two directories from Test-Comp for now. The two directories only contain 6 tasks, in total.

❱ cat MemSafety-Other.set
# Contains tasks for checking memory safety of programs.
loops/*.yml
loop-acceleration/*.yml
ntdrivers/*.yml
ntdrivers-simplified/*.yml
locks/*.yml
memsafety-ext3/*.yml
pthread-memsafety/*.yml
memsafety-bftpd/*.yml
termination-crafted/4BitCounterPointer.yml
termination-crafted/SyntaxSupportPointer*.yml
ldv-regression/*.yml
loop-industry-pattern/aiob_4*.yml
recursive-with-pointer/*.yml
❱ cat NoOverflows-Main.set
# Contains tasks for checking if variables of type signed integers overflow.
recursive/*.yml
recursive-simple/*.yml
bitvector/*.yml
psyco/*.yml
loop-zilu/*.yml
signedintegeroverflow-regression/*.yml
unsignedintegeroverflow-sas23/*.yml
termination-crafted/*.yml
termination-crafted-lit/*.yml
termination-numeric/*.yml
array-cav19/*.yml
array-crafted/*.yml
array-examples/*.yml
array-fpi/*.yml
array-industry-pattern/*.yml
array-lopstr16/*.yml
array-memsafety/*.yml
array-memsafety-realloc/*.yml
array-multidimensional/*.yml
array-tiling/*.yml
aws-c-common/*.yml
ddv-machzwd/*.yml
float-benchs/*.yml
heap-data/*.yml
ldv-commit-tester/*.yml
ldv-consumption/*.yml
ldv-linux-3.0/*.yml
ldv-linux-3.12-rc1/*.yml
ldv-linux-3.16-rc1/*.yml
ldv-linux-4.0-rc1-mav/*.yml
ldv-memsafety/*.yml
ldv-regression/*.yml
ldv-sets/*.yml
ldv-validator-v0.6/*.yml
ldv-validator-v0.8/*.yml
list-ext-properties/*.yml
list-ext3-properties/*.yml
list-simple/*.yml
loop-acceleration/*.yml
loop-industry-pattern/*.yml
loop-invgen/*.yml
loop-lit/*.yml
loop-new/*.yml
loop-simple/*.yml
loops/*.yml
loops-crafted-1/*.yml
memsafety/*.yml
memsafety-bftpd/*.yml
memsafety-ext2/*.yml
memsafety-ext3/*.yml
ntdrivers/*.yml
ntdrivers-simplified/*.yml
openssl/*.yml
openssl-simplified/*.yml
recursive-with-pointer/*.yml
reducercommutativity/*.yml
seq-mthreaded/*.yml
seq-mthreaded-reduced/*.yml
seq-pthread/*.yml
systemc/*.yml
termination-15/*.yml
termination-bwb/*.yml
termination-dietlibc/*.yml
termination-memory-alloca/*.yml
termination-memory-linkedlists/*.yml
termination-nla/*.yml
termination-recursive-malloc/*.yml
termination-restricted-15/*.yml
verifythis/*.yml
xcsp/*.yml
Edited by Thomas Lemberger

Merge request reports