Test-Comp 2023 - 5th International Competition on Software Testing

Benchmark Test Tasks

All test tasks are available for web browsing and for download via the following GIT repository (for Test-Comp 2023 visit the tag 'testcomp23'): https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks

This edition of the competition on software testing is based on the following categories of test tasks. The test tasks are taken from the most diverse and publicly available repository of tasks, which were collected and contributed by the community on software verification.

For illustration, a structured overview shows the categories.

The authorative definition of the category structure is maintained in the repository for the benchmark definitions (https://gitlab.com/sosy-lab/test-comp/bench-defs).

1. Cover Errors (Finding Bugs)

This category consists of the following sub-categories.

c/ReachSafety-Arrays

Contains tasks for which treatment of arrays is necessary in order to determine reachability.

The test-generation tasks consist of the programs that match

array-examples/*.yml
array-industry-pattern/*.yml
reducercommutativity/*.yml
array-tiling/*.yml
array-programs/*.yml
array-crafted/*.yml
array-multidimensional/*.yml
array-patterns/*.yml
array-cav19/*.yml
array-lopstr16/*.yml
array-fpi/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-BitVectors

Contains tasks for which treatment of bit-operations is necessary.

The test-generation tasks consist of the programs that match

bitvector/*.yml
bitvector-regression/*.yml
bitvector-loops/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-ControlFlow

Contains programs for which the correctness depends mostly on the control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency.

The test-generation tasks consist of the programs that match

ntdrivers-simplified/*.yml
openssl-simplified/*.yml
locks/*.yml
ntdrivers/*.yml
openssl/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-ECA

Contains programs that represent event-condition-action systems.

The test-generation tasks consist of the programs that match

eca-rers2012/*.yml
eca-rers2018/*.yml
psyco/*.yml
eca-programs/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Floats

Contains tasks for checking programs with floating-point arithmetics.

The test-generation tasks consist of the programs that match

floats-cdfpl/*.yml
floats-cbmc-regression/*.yml
float-benchs/*.yml
floats-esbmc-regression/*.yml
float-newlib/*.yml
loop-floats-scientific-comp/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Heap

Contains tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.

The test-generation tasks consist of the programs that match

heap-manipulation/*.yml
list-properties/*.yml
ldv-regression/*.yml
ddv-machzwd/*.yml
forester-heap/*.yml
list-ext-properties/*.yml
list-ext2-properties/*.yml
ldv-sets/*.yml
list-simple/*.yml
heap-data/*.yml
list-ext3-properties/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Loops

Contains tasks for which loop analysis is necessary.

The test-generation tasks consist of the programs that match

loops/*.yml
loop-acceleration/*.yml
loop-crafted/*.yml
loop-invgen/*.yml
loop-lit/*.yml
loop-new/*.yml
loop-industry-pattern/*.yml
loops-crafted-1/*.yml
loop-invariants/*.yml
loop-simple/*.yml
loop-zilu/*.yml
verifythis/duplets.yml
verifythis/elimination_max.yml
verifythis/lcp.yml
verifythis/prefixsum_iter.yml
verifythis/tree_del_iter.yml
verifythis/tree_del_iter_incorrect.yml
nla-digbench/*.yml
nla-digbench-scaling/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-ProductLines

Contains programs that represents 'products' and 'product simulators' that are derived using different configurations of product lines.

The test-generation tasks consist of the programs that match

product-lines/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Recursive

Contains tasks for which recursive analysis is necessary.

The test-generation tasks consist of the programs that match

recursive/*.yml
recursive-simple/*.yml
recursive-with-pointer/*.yml
verifythis/prefixsum_rec.yml
verifythis/tree_del_rec.yml
verifythis/tree_del_rec_incorrect.yml
verifythis/tree_max.yml
verifythis/tree_max_incorrect.yml
verifythis/elimination_max_rec.yml
verifythis/elimination_max_rec_onepoint.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Sequentialized

Contains sequentialized concurrent programs that were derived from SystemC programs. The programs were transformed to pure C programs by incorporating the scheduler into the C code.

The test-generation tasks consist of the programs that match

systemc/*.yml
seq-mthreaded/*.yml
seq-mthreaded-reduced/*.yml
seq-pthread/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-XCSP

Contains tasks from the XCSP_to_C tool benchmark set.

The test-generation tasks consist of the programs that match

xcsp/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/ReachSafety-Hardware

Contain tasks converted by Btor2C from word-level hardware-model-checking benchmarks Tasks converted by Btor2C with eager-modulo hardware-verification-array/btor2c-eagerMod.*.yml hardware-verification-bv/btor2c-eagerMod.*.yml Tasks converted by Btor2C with lazy-modulo

The test-generation tasks consist of the programs that match


hardware-verification-array/btor2c-lazyMod.*.yml
hardware-verification-bv/btor2c-lazyMod.*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/SoftwareSystems-BusyBox-MemSafety

Contains problems from the software system BusyBox.

The test-generation tasks consist of the programs that match

busybox-1.22.0/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

c/SoftwareSystems-DeviceDriversLinux64-ReachSafety

Contains problems that require the analysis of pointer aliases and function pointers.

The test-generation tasks consist of the programs that match

ldv-linux-3.0/*.yml
ldv-linux-3.4-simple/*.yml
ldv-linux-3.7.3/*.yml
ldv-commit-tester/*.yml
ldv-consumption/*.yml
ldv-linux-3.12-rc1/*.yml
ldv-linux-3.16-rc1/*.yml
ldv-validator-v0.6/*.yml
ldv-validator-v0.8/*.yml
ldv-linux-4.2-rc1/*.yml
ldv-linux-3.14/*.yml
ldv-challenges/*.yml
ldv-linux-4.0-rc1-mav/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )

2. Cover Branches (Code Coverage)

This category consists of the following sub-categories.

c/ReachSafety-Arrays

Contains tasks for which treatment of arrays is necessary in order to determine reachability.

The test-generation tasks consist of the programs that match

array-examples/*.yml
array-industry-pattern/*.yml
reducercommutativity/*.yml
array-tiling/*.yml
array-programs/*.yml
array-crafted/*.yml
array-multidimensional/*.yml
array-patterns/*.yml
array-cav19/*.yml
array-lopstr16/*.yml
array-fpi/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-BitVectors

Contains tasks for which treatment of bit-operations is necessary.

The test-generation tasks consist of the programs that match

bitvector/*.yml
bitvector-regression/*.yml
bitvector-loops/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-ControlFlow

Contains programs for which the correctness depends mostly on the control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency.

The test-generation tasks consist of the programs that match

ntdrivers-simplified/*.yml
openssl-simplified/*.yml
locks/*.yml
ntdrivers/*.yml
openssl/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-ECA

Contains programs that represent event-condition-action systems.

The test-generation tasks consist of the programs that match

eca-rers2012/*.yml
eca-rers2018/*.yml
psyco/*.yml
eca-programs/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Floats

Contains tasks for checking programs with floating-point arithmetics.

The test-generation tasks consist of the programs that match

floats-cdfpl/*.yml
floats-cbmc-regression/*.yml
float-benchs/*.yml
floats-esbmc-regression/*.yml
float-newlib/*.yml
loop-floats-scientific-comp/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Heap

Contains tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.

The test-generation tasks consist of the programs that match

heap-manipulation/*.yml
list-properties/*.yml
ldv-regression/*.yml
ddv-machzwd/*.yml
forester-heap/*.yml
list-ext-properties/*.yml
list-ext2-properties/*.yml
ldv-sets/*.yml
list-simple/*.yml
heap-data/*.yml
list-ext3-properties/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Loops

Contains tasks for which loop analysis is necessary.

The test-generation tasks consist of the programs that match

loops/*.yml
loop-acceleration/*.yml
loop-crafted/*.yml
loop-invgen/*.yml
loop-lit/*.yml
loop-new/*.yml
loop-industry-pattern/*.yml
loops-crafted-1/*.yml
loop-invariants/*.yml
loop-simple/*.yml
loop-zilu/*.yml
verifythis/duplets.yml
verifythis/elimination_max.yml
verifythis/lcp.yml
verifythis/prefixsum_iter.yml
verifythis/tree_del_iter.yml
verifythis/tree_del_iter_incorrect.yml
nla-digbench/*.yml
nla-digbench-scaling/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-ProductLines

Contains programs that represents 'products' and 'product simulators' that are derived using different configurations of product lines.

The test-generation tasks consist of the programs that match

product-lines/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Recursive

Contains tasks for which recursive analysis is necessary.

The test-generation tasks consist of the programs that match

recursive/*.yml
recursive-simple/*.yml
recursive-with-pointer/*.yml
verifythis/prefixsum_rec.yml
verifythis/tree_del_rec.yml
verifythis/tree_del_rec_incorrect.yml
verifythis/tree_max.yml
verifythis/tree_max_incorrect.yml
verifythis/elimination_max_rec.yml
verifythis/elimination_max_rec_onepoint.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Sequentialized

Contains sequentialized concurrent programs that were derived from SystemC programs. The programs were transformed to pure C programs by incorporating the scheduler into the C code.

The test-generation tasks consist of the programs that match

systemc/*.yml
seq-mthreaded/*.yml
seq-mthreaded-reduced/*.yml
seq-pthread/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-XCSP

Contains tasks from the XCSP_to_C tool benchmark set.

The test-generation tasks consist of the programs that match

xcsp/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/ReachSafety-Combinations

Contains programs combined from other sv-benchmark tasks through loose coupling

The test-generation tasks consist of the programs that match

combinations/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/SoftwareSystems-BusyBox-MemSafety

Contains problems from the software system BusyBox.

The test-generation tasks consist of the programs that match

busybox-1.22.0/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/SoftwareSystems-DeviceDriversLinux64-ReachSafety

Contains problems that require the analysis of pointer aliases and function pointers.

The test-generation tasks consist of the programs that match

ldv-linux-3.0/*.yml
ldv-linux-3.4-simple/*.yml
ldv-linux-3.7.3/*.yml
ldv-commit-tester/*.yml
ldv-consumption/*.yml
ldv-linux-3.12-rc1/*.yml
ldv-linux-3.16-rc1/*.yml
ldv-validator-v0.6/*.yml
ldv-validator-v0.8/*.yml
ldv-linux-4.2-rc1/*.yml
ldv-linux-3.14/*.yml
ldv-challenges/*.yml
ldv-linux-4.0-rc1-mav/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/SoftwareSystems-SQLite-MemSafety

Contains problems from the software SQLite

The test-generation tasks consist of the programs that match

sqlite/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

c/Termination-MainHeap

Contains programs for which termination should be decided.

The test-generation tasks consist of the programs that match

termination-dietlibc/*.yml
termination-memory-alloca/*.yml
termination-memory-linkedlists/*.yml
termination-15/*.yml
termination-recursive-malloc/*.yml

with the specification:

COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )

	FASE 2023
5th Competition on Software Testing (Test-Comp 2023)