#sel4test

Library for creating and running tests for seL4.

#Setup

See the build instructions page for instructions for installing required Host dependencies and how to checkout, build and run the tests in seL4test (this project).

#Usage

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.

#Unit tests

To define a small unit test in a library outside of sel4test or in sel4test-driver:

1. Declare libsel4test as a dependency for your library and include <sel4test/test.h>. You may also find the functions in <sel4test/testutil.h> handy.
2. 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 here.
3. Add your library as dependency to libsel4testsupport. Add a call to any function in your test file to testreporter.c in dummy_func(). If you have multiple test files, then you need to call one function for each test file.

For an example, take a look at libsel4serialserver/src/test.c in sel4_libs.

#Assumptions

Currently unit tests are assumed to be running sequentially, standalone (i.e. not multi-threaded). Some tests rely on being the highest priority running thread in the system.

#Other tests

To define a larger test in sel4test-tests:

1. Place your test in apps/sel4test-tests/src/tests.
2. Include <../helpers.h>.
3. 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 here.

For an example, take a look at trivial.c in sel4test.