-
Notifications
You must be signed in to change notification settings - Fork 254
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.
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.
The tests are in the projects DafnyLanguageServer.Test
and DafnyPipeline.Test
. You can either run them through most IDEs or on the command line:
- IDE: For example, in Visual Studio you can open the Test Explorer view: This view allows you to run (and debug) the whole test suite using the Play button or individual tests by right-clicking them.
- Command line: You can also execute the tests through the command line:
dotnet test .\Source\DafnyLanguageServer.Test\DafnyLanguageServer.Test.csproj
It's important to note that you may have to place z3 in the build directory of the tests. That's DafnyLanguageServer.Test/bin/Debug/net6.0
and DafnyLanguageServer.Test/bin/Release/net6.0
, depending on your build settings. Alternatively, you can ensure that z3/bin
's directory is accessible from the PATH
environment variable.
We are working towards being able to effectively measure the code coverage of the regression test suite: switching to the xUnit-based LIT test runner was a helpful first step, but we still need to be able to execute multiple test cases with the same .NET process, and/or merge coverage results in CI.
It is fairly straightforward to measure what code is hit when handling a particular set of Dafny files, however. The steps here are the most flexible since they can be used on arbitrary inputs and not just regression test cases, but it's likely possible to get an easier and smoother workflow working within an IDE for test cases - edits welcome!
- (one time only) Install the
coverlet
andreportgenerator
.NET tools.
dotnet tool install --global coverlet.console
dotnet tool install --global dotnet-reportgenerator-globaltool
-
cd
to the directory containing the Dafny DLLs (either an unzipped release or theBinaries
directory of a git clone). -
Invoke the Dafny CLI using the coverlet tool, which will store the raw coverage data to the given file path.
coverlet . --target "dotnet" --targetargs "Dafny.dll <dafny CLI arguments>" -f cobertura -o /path/to/output/coverage.cobertura.xml
- Run the
reportgenerator
tool to create a HTML report from the raw data.
reportgenerator -reports:/path/to/output/coverage.cobertura.xml -targetdir:/path/to/report/directory -reporttypes:HTML
- Navigate to
/path/to/report/directory/index.html
in a browser and enjoy!