From 312ca1d16a36043828dc2feac77851a6fe6152f5 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 10 Aug 2018 11:12:04 +0100 Subject: [PATCH 1/2] 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. --- .../compilation-and-development.md | 24 ++++++++++++++++++- doc/architectural/folder-walkthrough.md | 16 ++++++------- 2 files changed, 30 insertions(+), 10 deletions(-) diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index fc849ff1b09..65b11a06d4e 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 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: + + ../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. From ef53b65ef7030d9f207a6f34916a10290a19e571 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 10 Aug 2018 14:43:12 +0100 Subject: [PATCH 2/2] Update description of regression test framework --- doc/architectural/compilation-and-development.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index 65b11a06d4e..9f7a7dba5aa 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -23,9 +23,9 @@ To be documented. The regression tests are contained in the `regression/` folder. 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, +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