Skip to content

Commit 8b12064

Browse files
author
Owen Jones
committed
Add section to documentation about running tests
There was already a small amount of information about running the regression tests in the folder walkthrough, which I've moved to the new Running Tests section. The folder walkthrough now links to that section. Also added the `unit/` folder to the folder walkthrough.
1 parent 98657d8 commit 8b12064

File tree

2 files changed

+28
-10
lines changed

2 files changed

+28
-10
lines changed

doc/architectural/compilation-and-development.md

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,29 @@ To be documented.
1717

1818
To be documented.
1919

20-
## Documentation
20+
## Running tests ##
21+
22+
### Regression tests ###
23+
24+
The regression tests are contained in the `regression/` folder.
25+
They are grouped into directories for each of the tools/modules.
26+
Each of these contains a directory per test case, containing a C or C++
27+
file that triggers the bug and a `.desc` file that describes
28+
the tests, expected output and so on. There is a Perl script,
29+
`test.pl` that is used to invoke the tests as:
30+
31+
../test.pl -c PATH_TO_CBMC
32+
33+
The `–help` option gives instructions for use and the
34+
format of the description files.
35+
36+
To be documented further.
37+
38+
### Unit tests ###
39+
40+
To be documented.
41+
42+
## Documentation ##
2143

2244
Apart from the (user-orientated) CBMC user manual and this document, most
2345
of the rest of the documentation is inline in the code as `doxygen` and

doc/architectural/folder-walkthrough.md

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -75,14 +75,10 @@ into the `doc/html` directory when running `doxygen` from `src`.
7575

7676
## `regression/` ##
7777

78-
The `regression/` directory contains the test suites.
79-
They are grouped into directories for each of the tools/modules.
80-
Each of these contains a directory per test case, containing a C or C++
81-
file that triggers the bug and a `.desc` file that describes
82-
the tests, expected output and so on. There is a Perl script,
83-
`test.pl` that is used to invoke the tests as:
78+
The `regression/` directory contains the regression test suites. How to run the
79+
regression tests is documented in \ref compilation-and-development
8480

85-
../test.pl -c PATH_TO_CBMC
81+
## `unit/` ##
8682

87-
The `–help` option gives instructions for use and the
88-
format of the description files.
83+
The `unit/` directory contains the unit test suites. How to run the unit
84+
tests is documented in \ref compilation-and-development.

0 commit comments

Comments
 (0)