Skip to content

Commit 604e87f

Browse files
committed
Expand single regression test documentation
1 parent 916913a commit 604e87f

File tree

2 files changed

+13
-5
lines changed

2 files changed

+13
-5
lines changed

docs/developer-guide/testing.md

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,17 +16,24 @@ Regression tests can be run with various granularity:
1616

1717
* Run all (non-Apron) regression tests with: `./scripts/update_suite.rb`.
1818
* Run all Apron tests with: `dune build @runaprontest`.
19-
* Run a group of tests with: `./scripts/update_suite.rb group sanity`.
19+
* Run a group of tests (by directory, without number) with: `./scripts/update_suite.rb group sanity`.
2020

2121
Unfortunately this also runs skipped tests.
2222
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.
2323

24-
* Run a single test with: `./scripts/update_suite.rb assert`.
25-
* Run a single test with full output: `./regtest.sh 00 01`.
24+
* Run a single test (by name, without group or number) with: `./scripts/update_suite.rb assert`.
2625

27-
Additional options are also passed to Goblint.
26+
This compares Goblint output with test annotations (described below) and only outputs mismatches (i.e. test failures).
27+
It is useful for checking if the test passes (or which parts don't).
28+
Since group name is not specified, beware of same test name in multiple groups.
2829

29-
To pass additional options to Goblint with `update_suite.rb`, use the `gobopt` environment variable, e.g.:
30+
* Run a single test (by group and test number) with full output: `./regtest.sh 00 01`.
31+
32+
This _does not_ compare Goblint output with test annotations, but directly shows all Goblint output.
33+
It is useful for debugging the test.
34+
Additional command-line options are also passed to Goblint.
35+
36+
To pass additional command-line options to Goblint with `update_suite.rb`, use the `gobopt` environment variable, e.g.:
3037
```
3138
gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
3239
```

regtest.sh

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
#MacOS: needs brew install grep
33
if [ $# -lt 2 ]; then
44
echo "Usage: $0 group-nr test-nr [extra options]"
5+
echo "(Does not check test annotations.)"
56
exit 1
67
fi
78
file=(tests/regression/$1*/$2*.c)

0 commit comments

Comments
 (0)