Skip to content

Add (empty) section about running tests to documentation #2709

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Aug 11, 2018
Merged

Add (empty) section about running tests to documentation #2709

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
312ca1d
Add section to documentation about running tests
Aug 10, 2018
ef53b65
Update description of regression test framework
Aug 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 23 additions & 1 deletion doc/architectural/compilation-and-development.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 7 additions & 9 deletions doc/architectural/folder-walkthrough.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.