benchexec icon indicating copy to clipboard operation
benchexec copied to clipboard

Allow skipping runs for which <requiredfiles> does not match

Open PhilippWendler opened this issue 3 years ago • 2 comments

In uses cases like SV-COMP, we have benchmark definitions with lots of runs, but for some of the runs a required input file does not exist, and we are not interested in executing these runs (they would just fail anyway). We can make BenchExec avoid executing these useless runs by adding an attribute like "strictly required" or so to <requiredfiles>. If this parameter was set and the pattern would not match for a specific task, BenchExec would silently skip this run instead of logging "Pattern %s in requiredfiles tag did not match any file for task %s." and keeping the run.

PhilippWendler avatar Nov 12 '21 09:11 PhilippWendler

This could be not just a binary choice, we could have possible values like fail (makes BenchExec fail if pattern does not match), warn (current behavior), ignore (avoid warning), and skip run (this proposed feature).

Naming of the attribute is still open, please comment if you have ideas.

PhilippWendler avatar Nov 12 '21 09:11 PhilippWendler

  • Regarding the name attribute, I have no particular preference. May be <requiredfiles mode="strict">.
  • How about giving a warning on log level INFO, so that the user is informed that runs were skipped, instead of doing it silently?

dbeyer avatar Dec 19 '21 09:12 dbeyer