Add integration tests for output-file generation
Currently, we have (a) integration tests that check the correct verdict for verification and validation,
and we have (b) integration tests that check that all configurations in the config/
folder run on an empty program.
But integration tests (a) have output disabled (except for witness generation on C), and the integration tests (b) do not produce meaningful verdicts. So currently there is no test that all configurations in the config/
folder finish successfully on programs with a property violation (or on non-empty programs).
This means that errors that happen in the file export are not fully covered by our integration tests.
In addition, the current tests cover programs for C and Java (because there are special configurations for Java). But LLVM is missing from these tests.
To fix this, we should add integration tests that run each configuration in config/
on one file with a property violation and one file without a property violation. The tests should at least check that no errors occur.
These tests should cover all input languages that CPAchecker supports: C, Java, and LLVM IR.
@PhilippWendler drafted a way to implement these integration tests in !137 (comment 1908399661):
How about having one test suite that checks both the goals of
ConfigurationFileChecks.instantiate_and_run()
and working output files? I.e., enable output inConfigurationFileChecks
and attempt to run each configuration twice on a safe and unsafe program?On the other hand, using BenchExec (and thus BuildBot) for so many CPAchecker executions as integration tests might be nicer than using JUnit. For example, the resulting report is much easier to handle if it is a BenchExec table than a JUnit report. So we could also consider to replace
ConfigurationFileChecks.instantiate_and_run()
with a generator of a benchmark definition that gets then executed with BenchExec?
When these new tests exist, the integration tests added in !137 (merged) may be obsolete and it shuold be discussed whether to remove them.