Regression tests are small programs that can be used to quickly verify that existing functionality hasn't been broken.
They can be found in
Options that should be passed to Goblint when executing a regression test are specified in the test file using a single line comment starting with
Regression tests can be run with various granularity:
- Run all tests with:
Run a group of tests with:
./scripts/update_suite.rb group sanity.
Unfortunately this also runs skipped tests. This is a bug that is used as a feature in the tests with Apron, as not all CI jobs have the Apron library installed.
Run a single test with:
Run a single test with full output:
./regtest.sh 00 01.
Additional options are also passed to Goblint.
To pass additional options to Goblint with
update_suite.rb, use the
gobopt environment variable, e.g.:
gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
Regression tests use single-line comments (with
//) as annotations.
A comment on the first line can contain the following:
|The following command line parameters are added to Goblint for this test.|
||The test is skipped (except when run with
||Marshaling and unmarshaling of results is not tested on this program.|
End of line¶
Comments at the end of other lines indicate the behavior on that line:
|Annotation||Expected Goblint result||Concrete semantics||Checks|
|Assertion succeeds||Assertion always succeeds||Precision|
||Assertion fails||Assertion always fails||Precision|
||Assertion is unknown||Assertion may both
succeed or fail
||Assertion is unknown||—||Intended imprecision|
|Assertion is unknown
|Assertion always succeeds||Precision improvement|
||No race warning||No data race||Precision|
||Race warning||Data race is possible||Soundness|
||Race warning||—||Intended imprecision|
||No deadlock warning||No deadlock||Precision|
||Deadlock warning||Deadlock is possible||Soundness|
Other useful constructs are the following:
|Code with annotation||Comment|
||Checks that the line is reachable according
to Goblint results (soundness).
||Checks that the line is unreachable (precision).|
Cram-style tests are also used to verify that existing functionality hasn't been broken. They check the complete standard output of running the Goblint binary with specified command-line arguments. Unlike regular regression tests, cram tests are not limited to testing annotations in C code. They can be used to test arbitrary output from Goblint, such as program transformations.
Cram tests are located next to regression tests in
Cram tests are run as part of a complete test run:
This might take a while though. Pass the test directory to
dune to run only cram tests in a that directory:
dune runtest tests/regression/runs all cram tests.
dune runtest tests/regression/00-sanityruns all cram tests in
To run a single cram test, pass the file name without the
.t extension and with a leading
dune build @01-assertruns only
Create new cram tests in a subdirectory of
tests/regression with the extension
.t. The basic syntax of a cram test is as follows:
Anything not indented by two spaces is a comment. $ goblint <options...> file.c # This command gets run in a shell. <This is the expected output of running the command.>
dune file in the subdirectory must declare dependencies on other files, e.g. C files for goblint.
For example, to declare a dependency on all C and JSON files in the directory, use the
deps stanza with
(cram (deps (glob_files *.c) (glob_files *.json)))
The Dune documentation on file tests contains more details.
When Goblint's output is intentionally changed by code changes, cram tests will fail. After checking that the changes to Goblint's output shown in failing cram tests are as expected, you must update those tests. Dune can automatically update cram test files, i.e. promote the changes.
First, run the offending test as above. Once the new output is correct:
dune promotepromotes the changes for all files.
dune promote <path...>promotes the changes for the specified files and directories.
The incremental tests are regression tests that are first run with the option
incremental.save and then again
incrementally (activating the option
incremental.load) with some changes to the program or refinements in the
configuration. The respective
asserts and expected results are checked in both runs.
The incremental tests can be run with
./scripts/update_suite.rb -i. With
./scripts/update_suite.rb -c the
incremental tests are run using the more fine-grained cfg-based change detection.
An incremental test case consists of three files with the same file name: the
.c file with the initial program, a
.json file for the initial configuration and a
.patch file with the changes for the incremental run. Asserts and
expected results are encoded in the program as for other regression tests.
The patch file can contain changes to multiple files. This allows for modifications of code, asserts or expected results in the program file as well as refinements in the configuration for the incremental run. A suitable patch can be created with:
git diff --no-prefix relative/path/to/test.c relative/path/to/test.json > relative/path/to/test.patch
The comparison input and the metadata in the patch headers are not necessary and can be removed.
The unit tests can be run with
dune runtest unittest.
--watch for automatic rebuilding and retesting.
Property-based testing (a la QuickCheck) is used to test some domains (
Lattice.S implementations) for their lattice properties.
On integer domains the integer operations are also tested for being a valid abstraction of sets of integers.
Domain tests are now run as part of unit tests.
To test a domain, you need to do the following:
- Add the domain to
- Install bisect_ppx with
opam install bisect_ppx.
make coverageto build Goblint with bisect_ppx instrumentation.
- Run tests (this will now generate
.coveragefiles in various directories).
- Generate coverage report with
bisect-ppx-report html --coverage-path=..
- After that the generated
.coveragefiles can be removed with
find . -type f -name '*.coverage' -delete.
- The HTML report can be found in the