Allow skipping runs for which <requiredfiles> does not match

[PhilippWendler]

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]

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.

[dbeyer]

• 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?

[leventeBajczi]

I would like to express my support for this feature request, it would save a lot of time and unnecessary computations for purposes similar to witness validation at SV-COMP. I will try to prepare a PR soon with the proposed modification, and then we can continue discussing what makes sense for this, there.