NameDateSize

..25-Jul-20198

.licenseignoreH A D25-Jul-201937

apps/H25-Jul-20194

CMakeLists.txtH A D10-Jun-20201.3 KiB

docs/H22-Jul-20203

domain_schedule.cH A D25-Jul-20192 KiB

easy-settings.cmakeH A D22-Sep-20191.7 KiB

libsel4testsupport/H25-Jul-20195

LICENSE_BSD2.txtH A D25-Jul-20191.4 KiB

README.mdH A D15-Nov-20192.7 KiB

settings.cmakeH A D06-Oct-20204.1 KiB

README.md

1<!--
2 Copyright 2017, Data61
3 Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 ABN 41 687 119 230.
5
6 This software may be distributed and modified according to the terms of
7 the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 See "LICENSE_BSD2.txt" for details.
9
10 @TAG(DATA61_BSD)
11-->
12
13# sel4test
14
15Library for creating and running tests for seL4.
16
17## Setup
18
19See the [Getting Started](https://docs.sel4.systems/GettingStarted.html) page for instructions for installing required Host dependencies and how to checkout, build and run the tests in seL4test (this project).
20
21## Usage
22
23*Small unit tests* can be defined anywhere, such as libraries outside of `sel4test` or in `sel4test-driver`. *Larger tests* that do things like creating processes need to be declared inside `sel4test-tests`.
24
25### Unit tests
26To define a small unit test in a library outside of `sel4test` or in `sel4test-driver`:
271. Declare `libsel4test` as a dependency for your library and include `<sel4test/test.h>`. You may also find the functions in `<sel4test/testutil.h>` handy.
282. Write your tests. Then, for each test you want to run, call one of the macros that define a test, such as the `DEFINE_TEST` macro. They are declared
29[here](https://github.com/seL4/seL4_libs/blob/master/libsel4test/include/sel4test/test.h#L88).
303. Add your library as dependency to
31[`libsel4testsupport`](https://github.com/seL4/sel4test/blob/master/libsel4testsupport).
32Add a call to any function in your test file to `testreporter.c` in [`dummy_func()`](https://github.com/seL4/sel4test/blob/master/libsel4testsupport/src/testreporter.c#L35). If you have multiple test files, then you need to call one function for each test file.
33
34For an example, take a look at [`libsel4serialserver/src/test.c`](https://github.com/seL4/seL4_libs/blob/master/libsel4serialserver/src/test.c) in `sel4_libs`.
35
36### Assumptions
37Currently unit tests are assumed to be running sequentially, standalone (i.e. not multi-threaded).
38Some tests rely on being the highest priority running thread in the system.
39
40### Other tests
41To define a larger test in `sel4test-tests`:
421. Place your test in `apps/sel4test-tests/src/tests`.
432. Include `<../helpers.h>`.
443. Write your tests. Then, for each test you want to run, call one of the macros that define a test,
45    such as the `DEFINE_TEST` macro. They are declared [here](https://github.com/seL4/seL4_libs/blob/master/libsel4test/include/sel4test/test.h#L88).
46
47For an example, take a look at [`trivial.c`](https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/trivial.c) in `sel4test`.
48
49# License
50The files in this repository are release under standard open source licenses. Please see individual file headers and the `LICENSE_BSD2`.txt file for details.
51