diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-10-05 16:14:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-05 16:14:10 -0700 |
| commit | 88fb54a554f1a374a380b1808d355f096437d1c0 (patch) | |
| tree | 70e3a56c22fa5afaee520b3422f64d506506cf5d /INSTALL.md | |
| parent | e65308fa102d7121a981c9e6bc5b1414b28f9b28 (diff) | |
cmake: Add warning when unit testing is disabled due to assertions being disabled. (#5204)
This further fixes the testing instructions for API tests (formerly known as system tests)
in INSTALL.md.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/INSTALL.md b/INSTALL.md index 7143dfc0e..b3308726b 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -229,8 +229,8 @@ We have 4 categories of tests: (label: **example**) - **regression tests** (5 levels) in directory `test/regress` (label: **regressN** with N the regression level) -- **system tests** in directory `test/system` - (label: **system**) +- **api tests** in directory `test/api` + (label: **api**) - **unit tests** in directory `test/unit` (label: **unit**) @@ -238,26 +238,29 @@ We have 4 categories of tests: The system tests are not built by default. - make systemtests # build and run all system tests - make <system_test> # build test/system/<system_test>.<ext> - ctest system/<system_test> # run test/system/<system_test>.<ext> + make apitests # build and run all system tests + make <api_test> # build test/system/<system_test>.<ext> + ctest api/<api_test> # run test/system/<system_test>.<ext> All system test binaries are built into `<build_dir>/bin/test/system`. -We use prefix `system/` + `<system_test>` (for `<system_test>` in `test/system`) +We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`) as test target name. - make ouroborous # build test/system/ouroborous.cpp + make ouroborous # build test/api/ouroborous.cpp ctest -R ouroborous # run all tests that match '*ouroborous*' - # > runs system/ouroborous + # > runs api/ouroborous ctest -R ouroborous$ # run all tests that match '*ouroborous' - # > runs system/ouroborous - ctest -R system/ouroborous$ # run all tests that match '*system/ouroborous' - # > runs system/ouroborous + # > runs api/ouroborous + ctest -R api/ouroborous$ # run all tests that match '*api/ouroborous' + # > runs api/ouroborous ### Testing Unit Tests The unit tests are not built by default. +Note that CVC4 can only be configured with unit tests in non-static builds with +assertions enabled. + make units # build and run all unit tests make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext> ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext> |