Benchmark Test Tasks
All test tasks are available for web browsing and for download via the following GIT repository (for Test-Comp 2020 visit the tag 'testcomp20'): https://github.com/sosy-lab/sv-benchmarks/tree/testcomp20/
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.
1. Cover Errors (Finding Bugs)
This category consists of the following sub-categories.
ReachSafety-Arrays
Contains tasks for which treatment of arrays is necessary in order to determine reachability.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-BitVectors
Contains tasks for which treatment of bit-operations is necessary.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
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 tasks consist of the programs that match
ntdrivers-simplified/*.yml ssh-simplified/*.yml locks/*.yml ntdrivers/*.yml ssh/*.yml
with the specification
COVER( init(main()), FQL(COVER EDGES(@CALL(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-ECA
Contains programs that represent event-condition-action systems.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Floats
Contains tasks for checking programs with floating-point arithmetics.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Heap
Contains tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Loops
Contains tasks for which loop analysis is necessary.
The test 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 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
with the specification
COVER( init(main()), FQL(COVER EDGES(@CALL(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Recursive
Contains tasks for which recursive analysis is necessary.
The test 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
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 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(__VERIFIER_error))) )
and the following parameter:
Architecture: 32 bit
2. Cover Branches (Code Coverage)
This category consists of the following sub-categories.
ReachSafety-Arrays
Contains tasks for which treatment of arrays is necessary in order to determine reachability.
The test 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)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-BitVectors
Contains tasks for which treatment of bit-operations is necessary.
The test 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)) )
and the following parameter:
Architecture: 32 bit
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 tasks consist of the programs that match
ntdrivers-simplified/*.yml ssh-simplified/*.yml locks/*.yml ntdrivers/*.yml ssh/*.yml
with the specification
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-ECA
Contains programs that represent event-condition-action systems.
The test 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)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Floats
Contains tasks for checking programs with floating-point arithmetics.
The test 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)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Heap
Contains tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.
The test 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)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Loops
Contains tasks for which loop analysis is necessary.
The test 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 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
with the specification
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Recursive
Contains tasks for which recursive analysis is necessary.
The test 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)) )
and the following parameter:
Architecture: 32 bit
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 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)) )
and the following parameter:
Architecture: 32 bit
SoftwareSystems-BusyBox-MemSafety
Contains problems from the software system BusyBox.
The test tasks consist of the programs that match
busybox-1.22.0/*.yml
with the specification
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
and the following parameter:
Architecture: 64 bit
SoftwareSystems-DeviceDriversLinux64-ReachSafety
Contains problems that require the analysis of pointer aliases and function pointers.
The test 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)) )
and the following parameter:
Architecture: 64 bit
SoftwareSystems-SQLite-MemSafety
Contains problems from the software SQLite
The test tasks consist of the programs that match
sqlite/*.yml
with the specification
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
and the following parameter:
Architecture: 64 bit
Termination-MainHeap
Contains programs for which termination should be decided.
The test tasks consist of the programs that match
termination-libowfat/*.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)) )
and the following parameter:
Architecture: 64 bit