replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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.
This commit is contained in:
Owen Jones 2018-08-10 11:12:04 +01:00
parent 98657d85cd
commit 312ca1d16a
2 changed files with 30 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
doc/architectural/compilation-and-development.md
View File

@ -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

16
doc/architectural/folder-walkthrough.md
View File

@ -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.