File tree 2 files changed +30
-10
lines changed
2 files changed +30
-10
lines changed Original file line number Diff line number Diff line change @@ -17,7 +17,29 @@ To be documented.
17
17
18
18
To be documented.
19
19
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 ##
21
43
22
44
Apart from the (user-orientated) CBMC user manual and this document, most
23
45
of 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`.
75
75
76
76
## ` regression/ ` ##
77
77
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.
84
81
85
- ../test.pl -c PATH_TO_CBMC
82
+ ## ` unit/ ` ##
86
83
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