File tree Expand file tree Collapse file tree 2 files changed +30
-10
lines changed
Expand file tree Collapse file tree 2 files changed +30
-10
lines changed Original file line number Diff line number Diff line change @@ -17,7 +17,29 @@ To be documented.
1717
1818To 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 multiple directories, each of which contains
27+ input files and one or more` .desc ` files that describe what command
28+ to run, what output is expected 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
2244Apart from the (user-orientated) CBMC user manual and this document, most
2345of the rest of the documentation is inline in the code as ` doxygen ` and
Original file line number Diff line number Diff line change @@ -75,14 +75,12 @@ 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. See
79+ \ref compilation-and-development for information on how to run and
80+ develop regression tests.
8481
85- ../test.pl -c PATH_TO_CBMC
82+ ## ` unit/ ` ##
8683
87- The ` –help ` option gives instructions for use and the
88- format of the description files.
84+ The ` unit/ ` directory contains the unit test suites. See
85+ \ref compilation-and-development for information on how to run and
86+ develop unit tests.
You can’t perform that action at this time.
0 commit comments