Skip to content

[DOC-127]doc/cleanup-cprover-compilation-and-development #3384

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 4 commits into from
Nov 13, 2018
Merged

[DOC-127]doc/cleanup-cprover-compilation-and-development #3384

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e3f08db
Update link
Nov 13, 2018
f1e2fa9
Update build directory expression
Nov 13, 2018
4ff15dd
Added test.pl location
Nov 13, 2018
01dd28c
Fixed typo in unit test section
Nov 13, 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
8 changes: 4 additions & 4 deletions doc/architectural/compilation-and-development.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ FreeBSD 11, MacOS X and Windows.

There is also support for compiling using CMake. Instructions are
available in
[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake-experimental)
[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake)
in the root of the CBMC repository.


Expand Down Expand Up @@ -93,7 +93,7 @@ folders.
If you have compiled using CMake then you can run the regression tests (and
the unit tests) using CTest.

Here are two example commands, to be run from the build directory:
Here are two example commands, to be run from the `build/` directory:

ctest -V -L CORE -R cpp
ctest -V -L CORE -R cpp -E cbmc-cpp
Expand All @@ -112,7 +112,7 @@ list which tests it will run without actually running them.
\subsubsection compilation-and-development-subsubsection-running-regression-tests-directly-with-test-pl Running regression tests directly with `test.pl`

It can be useful to run a single test folder in isolation. This can be done by
running `test.pl` directly. The way that `test.pl` is run varies between the
running `regression/test.pl` directly. The way that `test.pl` is run varies between the
different modules, and can be ascertained by looking at the `test` target in
the makefile. The simple case is when there isn't a file called `chain.sh`.
Then you can directly run `test.pl` on a single test folder with the
Expand Down Expand Up @@ -151,7 +151,7 @@ the end of the run to see how many tests passed, how many failed which were
expected to and how many tests failed which were not expected to.

For more information on the structure of `unit/` and how to tag tests, see
[the section on unit tests in `Compiling.md` in the root of the CBMC
[the section on unit tests in `CODING_STANDARD.md` in the root of the CBMC
repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)


Expand Down