From a06ce414d9dbc00df908e482c55e40ed2001d2fc Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Mon, 12 Feb 2024 15:35:32 +0100 Subject: [PATCH] Improve test documentation Ref. None --- tests/README.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tests/README.md b/tests/README.md index 853f6a2c9..8c37c2fb0 100644 --- a/tests/README.md +++ b/tests/README.md @@ -12,6 +12,8 @@ A unit test verifies the functionality of a single Python module. The result of Integration tests verify the correct interaction between multiple modules. Complex tests comprising just a single module may also be included in this directory. +### Feature Tests (`tests/feature`) + Each subdirectory is considered as a feature test and must contain a `test.rflx` file. The following actions are performed for each feature test: - Check parsability of specification and creation of model @@ -20,6 +22,8 @@ Each subdirectory is considered as a feature test and must contain a `test.rflx` - Check executability of generated SPARK code (if `sequence` key in config is defined) - Check provabilility of generated SPARK code (if `prove` key in config is defined) +The checks are implemented in the `feature_test.py` in `tests/integration`, `tests/compilation` and `tests/verification`. + The executability and provability tests require the definition of a session called `Session`. The actions can be configured in an optional `config.yml` file: - `input`: A mapping of all readable channels to a list of messages. A message is represented by a space-separated list of bytes (decimal numerals in the range 0 to 255). @@ -37,10 +41,22 @@ End-to-end tests verify the functionality of the entire application. These tests Property-based testing based on [Hypothesis](https://hypothesis.readthedocs.io/). +### Verification Tests (`tests/verification`, `tests/property_verification`) + +All Python-based tests that require GNATprove. + +### Compilation Tests (`tests/compilation`) + +All Python-based tests that require GNAT. + ### SPARK Tests (`tests/spark`) The SPARK tests verify the correctness of the generated SPARK code. A [test suite](https://docs.adacore.com/live/wave/aunit/html/aunit_cb/aunit_cb.html) and [formal verification](https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/gnatprove.html) is used to ensure functional correctness and prove absence of runtime errors. The to be proven code is contained in `tests/spark/generated`. This code is also used by integration tests for regression testing. +### Language Tests (`tests/language`) + +Tests for the generated Langkit-based parser. + ### Tool Tests (`tests/tools`) Tool tests verify the functionality of the complementary tools in the `tools/` directory of the repository.