Skip to content

Change pattern syntax to match result files to Python syntax

The results of the competitions are not reproducible with BenchExec, because the benchmark definitions used in SV-COMP and Test-Comp use the pattern language of VerifierCloud, not the (more common) pattern language of BenchExec (and Python and Bash).

The following instructions to reproduce competition results do not work with BenchExec: https://gitlab.com/sosy-lab/sv-comp/bench-defs#executing-a-benchmark-for-a-particular-tool All witness files are missing after the benchmark execution.

The reason is that the benchmark definition files of the competitions use the pattern in the VerifierCloud format. Example: https://gitlab.com/sosy-lab/sv-comp/bench-defs/-/blob/main/benchmark-defs/cpachecker.xml#L7

BenchExec would expect **/*.graphml instead of **.graphml in order to work properly.

Two use cases for competitions:

VerifierCloud (Java) BenchExec (Python)
**.graphml **/*.graphml
**test-suite/* **/test-suite

Here hereby request to change the pattern language in VerifierCloud to the one used be BenchExec.

Description of the patterns that BenchExec supports and that I want: https://github.com/sosy-lab/benchexec/blob/main/doc/container.md#retrieving-result-files

A solution was described by @PhilippWendler and was also discussed in the following issue: #251

The change leads to a simplification and more robust VerifierCloud code: #251 (comment 254956468)

Edited by Dirk Beyer
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information