diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index fc849ff1b09..9f7a7dba5aa 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -17,7 +17,29 @@ To be documented. To be documented. -## Documentation +## Running tests ## + +### Regression tests ### + +The regression tests are contained in the `regression/` folder. +They are grouped into directories for each of the tools/modules. +Each of these contains multiple directories, each of which contains +input files and one or more`.desc` files that describe what command +to run, what output is expected and so on. There is a Perl script, +`test.pl` that is used to invoke the tests as: + + ../test.pl -c PATH_TO_CBMC + +The `–help` option gives instructions for use and the +format of the description files. + +To be documented further. + +### Unit tests ### + +To be documented. + +## Documentation ## Apart from the (user-orientated) CBMC user manual and this document, most of the rest of the documentation is inline in the code as `doxygen` and diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md index 9835af8a1c7..59e0b2aa43e 100644 --- a/doc/architectural/folder-walkthrough.md +++ b/doc/architectural/folder-walkthrough.md @@ -75,14 +75,12 @@ into the `doc/html` directory when running `doxygen` from `src`. ## `regression/` ## -The `regression/` directory contains the test suites. -They are grouped into directories for each of the tools/modules. -Each of these contains a directory per test case, containing a C or C++ -file that triggers the bug and a `.desc` file that describes -the tests, expected output and so on. There is a Perl script, -`test.pl` that is used to invoke the tests as: +The `regression/` directory contains the regression test suites. See +\ref compilation-and-development for information on how to run and +develop regression tests. - ../test.pl -c PATH_TO_CBMC +## `unit/` ## -The `–help` option gives instructions for use and the -format of the description files. +The `unit/` directory contains the unit test suites. See +\ref compilation-and-development for information on how to run and +develop unit tests.