Running Dafny's test suite

Update: This page describes testing with the lit tool. The project is moving to testing with an xUnit system, which is described here. The lit-based testing mechanism may be disabled in the future.

---

We use the LLVM integrated tester (lit) to test Dafny.

Dafny's test suite is located in the Test directory.

We provide a global lit configuration in the main test directory: Test/lit.site.cfg. We additionally provide local test configurations within some of the Test/* directories, such as for example Test/comp/lit.local.cfg.

lit is additionally instrumented in the headers of the test files. Each *.dfy file within the test suite provides information on how to call Dafny on itself, which is then combined with the global and local configurations. The test's output is then compared to the corresponding *.dfy.expect file via diff.

lit stores temporary outputs in an Output directory adjacent to the particular test file in the directory structure. If you encounter unexpected issues, you can get additional output by running lit in verbose mode (lit --verbose).

lit, by default, runs tests in parallel. For performance measurements, run lit with the -j 1 option.

Cygwin

Known Issue: When running lit on Cygwin, with Cygwin's Python installation, Dafny/Boogie seem to be confused about the correct path separator: they try to interpret files passed to it with absolute path (starting with /) as command line flags. A workaround is to run lit from a Windows shell using Windows' Python installation: e.g. it works for me running lit from the Anaconda prompt after installing lit there: conda install -c conda-forge lit. Please let us know if you know a better solution.