Improve how the test suite is set up and executed

[viper-admin]

Created by @mschwerhoff on 2019-03-23 22:14
Last updated on 2019-07-28 12:30

The Viper test suite is currently executed as follows: the test runner (instances of viper.silver.testing.SilSuite, see e.g. silicon/src/test/scala/SiliconTests.scala) is a single ScalaTest test suite, whose single ScalaTest test searches for Viper test files (*.sil, *.vpr) in certain directories and dynamically adds further ScalaTest tests, one per found file. From ScalaTest's point of view, what is executed is thus a single test suite with lots of (dynamically created) tests.

This has several disadvantages, e.g. during backend development:

1. Sbt's testQuick feature, which re-runs only those tests that previously failed, doesn't properly work because it works on the granularity of ScalaTest test suites rather than tests, and the former fails if any of its tests fail.

2. Individual tests can be run via Sbt's testOnly feature, by passing which tags tests to run must have to ScalaTests, e.g. testOnly -- -n functions.vpr. This works because our test runner creates several tags (filename, full path - maybe others) per test. However, tags do not support wildcards, which would be handy, e.g. to run all tests that contain "quantified" in their path name. Wildcards are supported by ScalaTests -z option, which can be specified, e.g. as testOnly -- -z *quantified*, but that only seems to work for statically created tests.

[viper-admin]

@mschwerhoff commented on 2019-07-28 12:30

See also #284